From 708295f53feba57fa5776d5721b0455b36a4200c Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 13 May 2023 09:23:44 -0600 Subject: [PATCH] Remove the concept of an `LTuple`. --- Bookshelf/Enderton.tex | 2 +- Bookshelf/Enderton/Chapter_0.lean | 270 +---------------------------- Common.lean | 1 - Common/LTuple.lean | 1 - Common/LTuple/Basic.lean | 277 ------------------------------ 5 files changed, 2 insertions(+), 549 deletions(-) delete mode 100644 Common/LTuple.lean delete mode 100644 Common/LTuple/Basic.lean diff --git a/Bookshelf/Enderton.tex b/Bookshelf/Enderton.tex index 7b4e156..4112570 100644 --- a/Bookshelf/Enderton.tex +++ b/Bookshelf/Enderton.tex @@ -29,7 +29,7 @@ Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$. \begin{proof} - \lean{Bookshelf/Enderton/Chapter\_0}{Enderton.Chapter\_0.lemma\_0a} + TODO \end{proof} diff --git a/Bookshelf/Enderton/Chapter_0.lean b/Bookshelf/Enderton/Chapter_0.lean index 24b344c..079f2a6 100644 --- a/Bookshelf/Enderton/Chapter_0.lean +++ b/Bookshelf/Enderton/Chapter_0.lean @@ -1,5 +1,3 @@ -import Common.LTuple.Basic - /-! # Enderton.Chapter_0 Useful Facts About Sets @@ -7,272 +5,6 @@ Useful Facts About Sets namespace Enderton.Chapter_0 -/-- -The following describes a so-called "generic" tuple. Like an `LTuple`, a generic -`n`-tuple is defined recursively like so: - - `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩` - -Unlike `LTuple`, this tuple bends the syntax above further. For example, -both tuples above are equivalent to: - - `⟨⟨x₁, ..., xₘ⟩, xₘ₊₁, ..., xₙ⟩` - -for some `1 ≤ m ≤ n`. This distinction is purely syntactic, and introduced -solely to prove `lemma_0a`. In other words, `LTuple` is an always-normalized -variant of an `GTuple`. In general, prefer it over this when working within -Enderton's book. --/ -inductive GTuple : (α : Type u) → (size : Nat × Nat) → Type u where - | nil : GTuple α (0, 0) - | snoc : GTuple α (p, q) → LTuple α r → GTuple α (p + q, r) - -syntax (priority := high) "t[" term,* "]" : term - -macro_rules - | `(t[]) => `(LTuple.nil) - | `(t[$x]) => `(LTuple.snoc t[] $x) - | `(t[$xs:term,*, $x]) => `(LTuple.snoc t[$xs,*] $x) - -syntax (priority := high) "g[" term,* "]" : term - -macro_rules - | `(g[]) => `(GTuple.nil) - | `(g[$x]) => `(GTuple.snoc g[] t[$x]) - | `(g[g[$xs:term,*], $ys:term,*]) => `(GTuple.snoc g[$xs,*] t[$ys,*]) - | `(g[$x, $xs:term,*]) => `(GTuple.snoc g[] t[$x, $xs,*]) - -namespace GTuple - -open scoped LTuple - -/-! ## Normalization -/ - -/-- -Converts an `GTuple` into "normal form". --/ -def norm : GTuple α (m, n) → LTuple α (m + n) - | g[] => t[] - | snoc is ts => LTuple.concat is.norm ts - -/-- -Normalization of an empty `GTuple` yields an empty `Tuple`. --/ -theorem norm_nil_eq_nil : @norm α 0 0 nil = LTuple.nil := - rfl - -/-- -Normalization of a pseudo-empty `GTuple` yields an empty `Tuple`. --/ -theorem norm_snoc_nil_nil_eq_nil : @norm α 0 0 (snoc g[] t[]) = t[] := by - unfold norm norm - rfl - -/-- -Normalization elimates `snoc` when the `snd` component is `nil`. --/ -theorem norm_snoc_nil_elim {t : GTuple α (p, q)} - : norm (snoc t t[]) = norm t := by - cases t with - | nil => simp; unfold norm norm; rfl - | snoc tf tl => - simp - conv => lhs; unfold norm - -/-- -Normalization eliminates `snoc` when the `fst` component is `nil`. --/ -theorem norm_nil_snoc_elim {ts : LTuple α n} - : norm (snoc g[] ts) = cast (by simp) ts := by - unfold norm norm - rw [LTuple.nil_concat_self_eq_self] - -/-- -Normalization distributes across `Tuple.snoc` calls. --/ -theorem norm_snoc_snoc_norm - : norm (snoc as (LTuple.snoc bs b)) = LTuple.snoc (norm (snoc as bs)) b := by - unfold norm - rw [← LTuple.concat_snoc_snoc_concat] - -/-- -Normalizing an `GTuple` is equivalent to concatenating the normalized `fst` -component with the `snd`. --/ -theorem norm_snoc_eq_concat {t₁ : GTuple α (p, q)} {t₂ : LTuple α n} - : norm (snoc t₁ t₂) = LTuple.concat t₁.norm t₂ := by - conv => lhs; unfold norm - -/-! ## Equality -/ - -/-- -Implements Boolean equality for `GTuple α n` provided `α` has decidable -equality. --/ -instance BEq [DecidableEq α] : BEq (GTuple α n) where - beq t₁ t₂ := t₁.norm == t₂.norm - -/-! ## Basic API -/ - -/-- -Returns the number of entries in the `GTuple`. --/ -def size (_ : GTuple α n) := n - -/-- -Returns the number of entries in the "shallowest" portion of the `GTuple`. For -example, the length of `x[x[1, 2], 3, 4]` is `3`, despite its size being `4`. --/ -def length : GTuple α n → Nat - | g[] => 0 - | snoc g[] ts => ts.size - | snoc _ ts => 1 + ts.size - -/-- -Returns the first component of our `GTuple`. For example, the first component of -tuple `x[x[1, 2], 3, 4]` is `t[1, 2]`. --/ -def fst : GTuple α (m, n) → LTuple α m - | g[] => t[] - | snoc ts _ => ts.norm - -/-- -Given `GTuple α (m, n)`, the `fst` component is equal to an initial segment of -size `k` of the tuple in normal form. --/ -theorem self_fst_eq_norm_take (t : GTuple α (m, n)) : t.fst = t.norm.take m := - match t with - | g[] => by - unfold fst - rw [LTuple.self_take_zero_eq_nil] - simp - | snoc tf tl => by - unfold fst - conv => rhs; unfold norm - rw [LTuple.eq_take_concat] - simp - -/-- -If the normal form of an `GTuple` is equal to a `Tuple`, the `fst` component -must be a prefix of the `Tuple`. --/ -theorem norm_eq_fst_eq_take {t₁ : GTuple α (m, n)} {t₂ : LTuple α (m + n)} - : (t₁.norm = t₂) → (t₁.fst = t₂.take m) := by - intro h - rw [self_fst_eq_norm_take, h] - -/-- -Returns the first component of our `GTuple`. For example, the first component of -tuple `x[x[1, 2], 3, 4]` is `t[3, 4]`. --/ -def snd : GTuple α (m, n) → LTuple α n - | g[] => t[] - | snoc _ ts => ts - -end GTuple - -/-! ## Lemma 0A -/ - -section - -variable {k m n : Nat} -variable (p : 1 ≤ m) -variable (q : n + (m - 1) = m + k) - -private lemma n_eq_succ_k : n = k + 1 := by - let ⟨m', h⟩ := Nat.exists_eq_succ_of_ne_zero $ show m ≠ 0 by - intro h - have ff : 1 ≤ 0 := h ▸ p - ring_nf at ff - exact ff.elim - calc - n = n + (m - 1) - (m - 1) := by rw [Nat.add_sub_cancel] - _ = m' + 1 + k - (m' + 1 - 1) := by rw [q, h] - _ = m' + 1 + k - m' := by simp - _ = 1 + k + m' - m' := by rw [Nat.add_assoc, Nat.add_comm] - _ = 1 + k := by simp - _ = k + 1 := by rw [Nat.add_comm] - -private lemma n_pred_eq_k : n - 1 = k := by - have h : k + 1 - 1 = k + 1 - 1 := rfl - conv at h => lhs; rw [←n_eq_succ_k p q] - simp at h - exact h - -private lemma n_geq_one : 1 ≤ n := by - rw [n_eq_succ_k p q] - simp - -private lemma min_comm_succ_eq : min (m + k) (k + 1) = k + 1 := - Nat.recOn k - (by simp; exact p) - (fun k' ih => calc min (m + (k' + 1)) (k' + 1 + 1) - _ = min (m + k' + 1) (k' + 1 + 1) := by conv => rw [Nat.add_assoc] - _ = min (m + k') (k' + 1) + 1 := Nat.min_succ_succ (m + k') (k' + 1) - _ = k' + 1 + 1 := by rw [ih]) - -private lemma n_eq_min_comm_succ : n = min (m + k) (k + 1) := by - rw [min_comm_succ_eq p] - exact n_eq_succ_k p q - -private lemma n_pred_m_eq_m_k : n + (m - 1) = m + k := by - rw [←Nat.add_sub_assoc p, Nat.add_comm, Nat.add_sub_assoc (n_geq_one p q)] - conv => lhs; rw [n_pred_eq_k p q] - -private def castNorm : GTuple α (n, m - 1) → LTuple α (m + k) - | xs => cast (by rw [q]) xs.norm - -private def castFst : GTuple α (n, m - 1) → LTuple α (k + 1) - | xs => cast (by rw [n_eq_succ_k p q]) xs.fst - -private def castTake (ys : LTuple α (m + k)) := - cast (by rw [min_comm_succ_eq p]) (ys.take (k + 1)) - -/-- #### Lemma 0A - -Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Then -`x₁ = ⟨y₁, ..., yₖ₊₁⟩`. --/ -theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k)) - : (castNorm q xs = ys) → (castFst p q xs = castTake p ys) := by - intro h - suffices HEq - (cast (_ : LTuple α n = LTuple α (k + 1)) xs.fst) - (cast (_ : LTuple α (min (m + k) (k + 1)) = LTuple α (k + 1)) (LTuple.take ys (k + 1))) - from eq_of_heq this - congr - · exact n_eq_min_comm_succ p q - · rfl - · exact n_eq_min_comm_succ p q - · exact HEq.rfl - · exact Eq.recOn - (motive := fun _ h => HEq - (_ : n + (n - 1) = n + k) - (cast h (show n + (n - 1) = n + k by rw [n_pred_eq_k p q]))) - (show (n + (n - 1) = n + k) = (min (m + k) (k + 1) + (n - 1) = n + k) by - rw [n_eq_min_comm_succ p q]) - HEq.rfl - · exact n_geq_one p q - · exact n_pred_eq_k p q - · exact Eq.symm (n_eq_min_comm_succ p q) - · exact n_pred_eq_k p q - · rw [GTuple.self_fst_eq_norm_take] - unfold castNorm at h - simp at h - rw [←h, ←n_eq_succ_k p q] - have h₂ := Eq.recOn - (motive := fun x h => HEq - (LTuple.take xs.norm n) - (LTuple.take (cast (show LTuple α (n + (m - 1)) = LTuple α x by rw [h]) xs.norm) n)) - (show n + (m - 1) = m + k by rw [n_pred_m_eq_m_k p q]) - HEq.rfl - exact Eq.recOn - (motive := fun x h => HEq - (cast h (LTuple.take xs.norm n)) - (LTuple.take (cast (_ : LTuple α (n + (m - 1)) = LTuple α (m + k)) xs.norm) n)) - (show LTuple α (min (n + (m - 1)) n) = LTuple α n by simp) - h₂ - -end +-- TODO end Enderton.Chapter_0 diff --git a/Common.lean b/Common.lean index 7c935c9..1a0cb93 100644 --- a/Common.lean +++ b/Common.lean @@ -1,5 +1,4 @@ import Common.Combinator import Common.List -import Common.LTuple import Common.Real import Common.Set \ No newline at end of file diff --git a/Common/LTuple.lean b/Common/LTuple.lean deleted file mode 100644 index 8d046f3..0000000 --- a/Common/LTuple.lean +++ /dev/null @@ -1 +0,0 @@ -import Common.LTuple.Basic \ No newline at end of file diff --git a/Common/LTuple/Basic.lean b/Common/LTuple/Basic.lean deleted file mode 100644 index e6e2f46..0000000 --- a/Common/LTuple/Basic.lean +++ /dev/null @@ -1,277 +0,0 @@ -import Mathlib.Tactic.Ring - -/-! # Common.LTuple.Basic - -The following is a representation of a (possibly empty) left-biased tuple. A -left-biased `n`-tuple is defined recursively as follows: - -``` -⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩ -``` - -Note a `Tuple` exists in Lean already. This implementation differs in two -notable ways: - -1. It is left-associative. The built-in `Tuple` instance evaluates e.g. - `(x₁, x₂, x₃)` as `(x₁, (x₂, x₃))` instead of `((x₁, x₂), x₃)`. -2. Internally, the built-in `Tuple` instance is syntactic sugar for nested - `Prod` instances. Unlike this implementation, an `LTuple` is a homogeneous - collection. - -In general, prefer using `Prod` over `LTuple`. This exists primarily to solve -certain theorems outlined in [^1]. - -[^1]: Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San - Diego: Harcourt/Academic Press, 2001. --/ - -/-- -#### LTuple - -A left-biased, possibly empty, homogeneous `Tuple`-like structure.. --/ -inductive LTuple : (α : Type u) → (size : Nat) → Type u where - | nil : LTuple α 0 - | snoc : LTuple α n → α → LTuple α (n + 1) - -namespace LTuple - -/-! ## Coercions -/ - -scoped instance : CoeOut (LTuple α (min (m + n) m)) (LTuple α m) where - coe := cast (by simp) - -scoped instance : Coe (LTuple α 0) (LTuple α (min n 0)) where - coe := cast (by rw [Nat.min_zero]) - -scoped instance : Coe (LTuple α 0) (LTuple α (min 0 n)) where - coe := cast (by rw [Nat.zero_min]) - -scoped instance : Coe (LTuple α n) (LTuple α (min n n)) where - coe := cast (by simp) - -scoped instance : Coe (LTuple α n) (LTuple α (0 + n)) where - coe := cast (by simp) - -scoped instance : Coe (LTuple α (min m n + 1)) (LTuple α (min (m + 1) (n + 1))) where - coe := cast (by rw [Nat.min_succ_succ]) - -scoped instance : Coe (LTuple α m) (LTuple α (min (m + n) m)) where - coe := cast (by simp) - -/-! ### Equality -/ - -/-- -Two values `a` and `b` are equal **iff** `[a] = [b]`. --/ -theorem eq_iff_singleton : (a = b) ↔ (snoc a nil = snoc b nil) := by - apply Iff.intro - · intro h; rw [h] - · intro h; injection h - -/-- -Two lists are equal **iff** their heads and tails are equal. --/ -theorem eq_iff_snoc {t₁ t₂ : LTuple α n} - : (a = b ∧ t₁ = t₂) ↔ (snoc t₁ a = snoc t₂ b) := by - apply Iff.intro - · intro ⟨h₁, h₂ ⟩; rw [h₁, h₂] - · intro h - injection h with _ h₁ h₂ - exact And.intro h₂ h₁ - -/-- -Implements decidable equality for `Tuple α m`, provided `a` has decidable -equality. --/ -protected def hasDecEq [DecidableEq α] (t₁ t₂ : LTuple α n) - : Decidable (Eq t₁ t₂) := - match t₁, t₂ with - | nil, nil => isTrue rfl - | snoc as a, snoc bs b => - match LTuple.hasDecEq as bs with - | isFalse np => isFalse (fun h => absurd (eq_iff_snoc.mpr h).right np) - | isTrue hp => - if hq : a = b then - isTrue (eq_iff_snoc.mp $ And.intro hq hp) - else - isFalse (fun h => absurd (eq_iff_snoc.mpr h).left hq) - -instance [DecidableEq α] : DecidableEq (LTuple α n) := LTuple.hasDecEq - -/-! ## Basic API -/ - -/-- -Returns the number of entries in an `LTuple`. --/ -def size (_ : LTuple α n) : Nat := n - -/-- -Returns all but the last entry of an `LTuple`. --/ -def init : (t : LTuple α (n + 1)) → LTuple α n - | snoc vs _ => vs - -/-- -Returns the last entry of an `LTuple`. --/ -def last : LTuple α (n + 1) → α - | snoc _ v => v - -/-- -Prepends an entry to an `LTuple`. --/ -def cons : LTuple α n → α → LTuple α (n + 1) - | nil, a => snoc nil a - | snoc ts t, a => snoc (cons ts a) t - -/-! ## Concatenation -/ - -/-- -Joins two `LTuple`s together end to end. --/ -def concat : LTuple α m → LTuple α n → LTuple α (m + n) - | is, nil => is - | is, snoc ts t => snoc (concat is ts) t - -/-- -Concatenating an `LTuple` with `nil` yields the original `LTuple`. --/ -theorem self_concat_nil_eq_self (t : LTuple α m) : concat t nil = t := - match t with - | nil => rfl - | snoc _ _ => rfl - -/-- -Concatenating `nil` with an `LTuple` yields the original `LTuple`. --/ -theorem nil_concat_self_eq_self (t : LTuple α m) : concat nil t = t := by - induction t with - | nil => unfold concat; simp - | @snoc n as a ih => - unfold concat - rw [ih] - suffices HEq (snoc (cast (_ : LTuple α n = LTuple α (0 + n)) as) a) ↑(snoc as a) - from eq_of_heq this - have h₁ := Eq.recOn - (motive := fun x h => HEq - (snoc (cast (show LTuple α n = LTuple α x by rw [h]) as) a) - (snoc as a)) - (show n = 0 + n by simp) - HEq.rfl - exact Eq.recOn - (motive := fun x h => HEq - (snoc (cast (_ : LTuple α n = LTuple α (0 + n)) as) a) - (cast h (snoc as a))) - (show LTuple α (n + 1) = LTuple α (0 + (n + 1)) by simp) - h₁ - -/-- -Concatenating an `LTuple` to a nonempty `LTuple` moves `concat` calls closer to -the expression leaves. --/ -theorem concat_snoc_snoc_concat {bs : LTuple α n} - : concat as (snoc bs b) = snoc (concat as bs) b := - rfl - -/-- -`snoc` is equivalent to concatenating the `init` and `last` elements of an -`LTuple` together. --/ -theorem snoc_eq_init_concat_last (as : LTuple α m) - : snoc as a = concat as (snoc nil a) := by - cases as with - | nil => rfl - | snoc _ _ => simp; unfold concat concat; rfl - -/-! ## Initial Sequences -/ - -/-- -Takes the first `k` entries from an `LTuple` to form a new `LTuple`, or the -entire `LTuple` if `k` exceeds the size. --/ -def take (t : LTuple α n) (k : Nat) : LTuple α (min n k) := - if h : n ≤ k then - cast (by rw [min_eq_left h]) t - else - match t with - | nil => nil - | @snoc _ n' as a => cast (by rw [min_lt_succ_eq h]) (take as k) - where - min_lt_succ_eq {m : Nat} (h : ¬m + 1 ≤ k) : min m k = min (m + 1) k := by - have h' : k + 1 ≤ m + 1 := Nat.lt_of_not_le h - simp at h' - rw [min_eq_right h', min_eq_right (Nat.le_trans h' (Nat.le_succ m))] - -/-- -Taking no entries from any `LTuple` should yield an empty `LTuple`. --/ -theorem self_take_zero_eq_nil (t : LTuple α n) : take t 0 = @nil α := by - induction t with - | nil => simp; rfl - | snoc as a ih => unfold take; simp; rw [ih]; simp - -/-- -Taking any number of entries from an empty `LTuple` should yield an empty -`LTuple`. --/ -theorem nil_take_zero_eq_nil (k : Nat) : (take (@nil α) k) = @nil α := by - cases k <;> (unfold take; simp) - -/-- -Taking `n` entries from an `LTuple` of size `n` should yield the same `LTuple`. --/ -theorem self_take_size_eq_self (t : LTuple α n) : take t n = t := by - cases t with - | nil => simp; rfl - | snoc as a => unfold take; simp - -/-- -Taking `n - 1` elements from an `LTuple` of size `n` yields the same result, -regardless of the last entry's value. --/ -theorem take_subst_last {as : LTuple α n} (a₁ a₂ : α) - : take (snoc as a₁) n = take (snoc as a₂) n := by - unfold take - simp - -/-- -Taking `n` elements from an `LTuple` of size `n + 1` is the same as invoking -`init`. --/ -theorem init_eq_take_pred (t : LTuple α (n + 1)) : take t n = init t := by - cases t with - | snoc as a => - unfold init take - simp - rw [self_take_size_eq_self] - simp - -/-- -If two `LTuple`s are equal, then any initial sequences of these two `LTuple`s -are also equal. --/ -theorem eq_tuple_eq_take {t₁ t₂ : LTuple α n} - : (t₁ = t₂) → (t₁.take k = t₂.take k) := by - intro h - rw [h] - -/-- -Given an `LTuple` of size `k`, concatenating an arbitrary `LTuple` and taking -`k` elements yields the original `LTuple`. --/ -theorem eq_take_concat {t₁ : LTuple α m} {t₂ : LTuple α n} - : take (concat t₁ t₂) m = t₁ := by - induction t₂ with - | nil => - simp - rw [self_concat_nil_eq_self, self_take_size_eq_self] - | @snoc n' as a ih => - simp - rw [concat_snoc_snoc_concat] - unfold take - simp - rw [ih] - simp - -end LTuple \ No newline at end of file