From e91628a828b1d1902d11b1535743dc0a90d8d3e3 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 26 Apr 2023 15:39:53 -0600 Subject: [PATCH] `Tuple`s already exist in Lean; nest inside Enderton section instead. --- Bookshelf.lean | 1 - Bookshelf/List/Basic.lean | 2 - MathematicalIntroductionLogic.lean | 3 +- MathematicalIntroductionLogic/Chapter0.lean | 187 +----------------- MathematicalIntroductionLogic/Tuple.lean | 2 + .../Tuple/Basic.lean | 14 +- .../Tuple/Generic.lean | 164 +++++++++++++++ 7 files changed, 189 insertions(+), 184 deletions(-) create mode 100644 MathematicalIntroductionLogic/Tuple.lean rename Bookshelf/Tuple.lean => MathematicalIntroductionLogic/Tuple/Basic.lean (92%) create mode 100644 MathematicalIntroductionLogic/Tuple/Generic.lean diff --git a/Bookshelf.lean b/Bookshelf.lean index 09cf26e..71ccb30 100644 --- a/Bookshelf.lean +++ b/Bookshelf.lean @@ -1,3 +1,2 @@ import Bookshelf.List import Bookshelf.Real -import Bookshelf.Tuple \ No newline at end of file diff --git a/Bookshelf/List/Basic.lean b/Bookshelf/List/Basic.lean index a5e1e1c..6b29285 100644 --- a/Bookshelf/List/Basic.lean +++ b/Bookshelf/List/Basic.lean @@ -1,7 +1,5 @@ import Mathlib.Data.Fintype.Basic -import Mathlib.Logic.Basic import Mathlib.Tactic.NormNum -import Mathlib.Tactic.LibrarySearch namespace List diff --git a/MathematicalIntroductionLogic.lean b/MathematicalIntroductionLogic.lean index 99394ed..6462279 100644 --- a/MathematicalIntroductionLogic.lean +++ b/MathematicalIntroductionLogic.lean @@ -1 +1,2 @@ -import MathematicalIntroductionLogic.Chapter0 \ No newline at end of file +import MathematicalIntroductionLogic.Chapter0 +import MathematicalIntroductionLogic.Tuple \ No newline at end of file diff --git a/MathematicalIntroductionLogic/Chapter0.lean b/MathematicalIntroductionLogic/Chapter0.lean index 29a1fcf..e0ec96a 100644 --- a/MathematicalIntroductionLogic/Chapter0.lean +++ b/MathematicalIntroductionLogic/Chapter0.lean @@ -4,174 +4,7 @@ Chapter 0 Useful Facts About Sets -/ -import Bookshelf.Tuple - -/-- -The following describes a so-called "generic" tuple. Like in `Bookshelf.Tuple`, -an `n`-tuple is defined recursively like so: - - `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩` - -Unlike `Bookshelf.Tuple`, a "generic" 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, but necessary to -prove certain theorems found in [1] (e.g. `lemma_0a`). - -In general, prefer `Bookshelf.Tuple`. --/ -inductive XTuple : (α : Type u) → (size : Nat × Nat) → Type u where - | nil : XTuple α (0, 0) - | snoc : XTuple α (p, q) → Tuple α r → XTuple α (p + q, r) - -syntax (priority := high) "x[" term,* "]" : term - -macro_rules - | `(x[]) => `(XTuple.nil) - | `(x[$x]) => `(XTuple.snoc x[] t[$x]) - | `(x[x[$xs:term,*], $ys:term,*]) => `(XTuple.snoc x[$xs,*] t[$ys,*]) - | `(x[$x, $xs:term,*]) => `(XTuple.snoc x[] t[$x, $xs,*]) - -namespace XTuple - -open scoped Tuple - --- ======================================== --- Normalization --- ======================================== - -/-- -Converts an `XTuple` into "normal form". --/ -def norm : XTuple α (m, n) → Tuple α (m + n) - | x[] => t[] - | snoc is ts => Tuple.concat is.norm ts - -/-- -Normalization of an empty `XTuple` yields an empty `Tuple`. --/ -theorem norm_nil_eq_nil : @norm α 0 0 nil = Tuple.nil := - rfl - -/-- -Normalization of a pseudo-empty `XTuple` yields an empty `Tuple`. --/ -theorem norm_snoc_nil_nil_eq_nil : @norm α 0 0 (snoc x[] t[]) = t[] := by - unfold norm norm - rfl - -/-- -Normalization elimates `snoc` when the `snd` component is `nil`. --/ -theorem norm_snoc_nil_elim {t : XTuple α (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 : Tuple α n} - : norm (snoc x[] ts) = cast (by simp) ts := by - unfold norm norm - rw [Tuple.nil_concat_self_eq_self] - -/-- -Normalization distributes across `Tuple.snoc` calls. --/ -theorem norm_snoc_snoc_norm - : norm (snoc as (Tuple.snoc bs b)) = Tuple.snoc (norm (snoc as bs)) b := by - unfold norm - rw [←Tuple.concat_snoc_snoc_concat] - -/-- -Normalizing an `XTuple` is equivalent to concatenating the normalized `fst` -component with the `snd`. --/ -theorem norm_snoc_eq_concat {t₁ : XTuple α (p, q)} {t₂ : Tuple α n} - : norm (snoc t₁ t₂) = Tuple.concat t₁.norm t₂ := by - conv => lhs; unfold norm - --- ======================================== --- Equality --- ======================================== - -/-- -Implements Boolean equality for `XTuple α n` provided `α` has decidable -equality. --/ -instance BEq [DecidableEq α] : BEq (XTuple α n) where - beq t₁ t₂ := t₁.norm == t₂.norm - --- ======================================== --- Basic API --- ======================================== - -/-- -Returns the number of entries in the `XTuple`. --/ -def size (_ : XTuple α n) := n - -/-- -Returns the number of entries in the "shallowest" portion of the `XTuple`. For -example, the length of `x[x[1, 2], 3, 4]` is `3`, despite its size being `4`. --/ -def length : XTuple α n → Nat - | x[] => 0 - | snoc x[] ts => ts.size - | snoc _ ts => 1 + ts.size - -/-- -Returns the first component of our `XTuple`. For example, the first component of -tuple `x[x[1, 2], 3, 4]` is `t[1, 2]`. --/ -def fst : XTuple α (m, n) → Tuple α m - | x[] => t[] - | snoc ts _ => ts.norm - -/-- -Given `XTuple α (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 : XTuple α (m, n)) : t.fst = t.norm.take m := - match t with - | x[] => by - unfold fst - rw [Tuple.self_take_zero_eq_nil] - simp - | snoc tf tl => by - unfold fst - conv => rhs; unfold norm - rw [Tuple.eq_take_concat] - simp - -/-- -If the normal form of an `XTuple` is equal to a `Tuple`, the `fst` component -must be a prefix of the `Tuple`. --/ -theorem norm_eq_fst_eq_take {t₁ : XTuple α (m, n)} {t₂ : Tuple α (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 `XTuple`. For example, the first component of -tuple `x[x[1, 2], 3, 4]` is `t[3, 4]`. --/ -def snd : XTuple α (m, n) → Tuple α n - | x[] => t[] - | snoc _ ts => ts - --- ======================================== --- Lemma 0A --- ======================================== - -section +import MathematicalIntroductionLogic.Tuple.Generic variable {k m n : Nat} variable (p : 1 ≤ m) @@ -217,10 +50,10 @@ 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 cast_norm : XTuple α (n, m - 1) → Tuple α (m + k) +private def cast_norm : GTuple α (n, m - 1) → Tuple α (m + k) | xs => cast (by rw [q]) xs.norm -private def cast_fst : XTuple α (n, m - 1) → Tuple α (k + 1) +private def cast_fst : GTuple α (n, m - 1) → Tuple α (k + 1) | xs => cast (by rw [n_eq_succ_k p q]) xs.fst private def cast_take (ys : Tuple α (m + k)) := @@ -229,14 +62,14 @@ private def cast_take (ys : Tuple α (m + k)) := /-- Lemma 0A -Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. -Then `x₁ = ⟨y₁, ..., yₖ₊₁⟩`. +Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Then +`x₁ = ⟨y₁, ..., yₖ₊₁⟩`. -/ -theorem lemma_0a (xs : XTuple α (n, m - 1)) (ys : Tuple α (m + k)) +theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : Tuple α (m + k)) : (cast_norm q xs = ys) → (cast_fst p q xs = cast_take p ys) := by intro h suffices HEq - (cast (_ : Tuple α n = Tuple α (k + 1)) (fst xs)) + (cast (_ : Tuple α n = Tuple α (k + 1)) xs.fst) (cast (_ : Tuple α (min (m + k) (k + 1)) = Tuple α (k + 1)) (Tuple.take ys (k + 1))) from eq_of_heq this congr @@ -255,7 +88,7 @@ theorem lemma_0a (xs : XTuple α (n, m - 1)) (ys : Tuple α (m + k)) · 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 [self_fst_eq_norm_take] + · rw [GTuple.self_fst_eq_norm_take] unfold cast_norm at h simp at h rw [←h, ←n_eq_succ_k p q] @@ -271,7 +104,3 @@ theorem lemma_0a (xs : XTuple α (n, m - 1)) (ys : Tuple α (m + k)) (Tuple.take (cast (_ : Tuple α (n + (m - 1)) = Tuple α (m + k)) xs.norm) n)) (show Tuple α (min (n + (m - 1)) n) = Tuple α n by simp) h₂ - -end - -end XTuple diff --git a/MathematicalIntroductionLogic/Tuple.lean b/MathematicalIntroductionLogic/Tuple.lean new file mode 100644 index 0000000..21e54af --- /dev/null +++ b/MathematicalIntroductionLogic/Tuple.lean @@ -0,0 +1,2 @@ +import MathematicalIntroductionLogic.Tuple.Basic +import MathematicalIntroductionLogic.Tuple.Generic diff --git a/Bookshelf/Tuple.lean b/MathematicalIntroductionLogic/Tuple/Basic.lean similarity index 92% rename from Bookshelf/Tuple.lean rename to MathematicalIntroductionLogic/Tuple/Basic.lean index ef18e59..84d6056 100644 --- a/Bookshelf/Tuple.lean +++ b/MathematicalIntroductionLogic/Tuple/Basic.lean @@ -1,12 +1,24 @@ import Mathlib.Tactic.Ring /-- -`n`-tuples are defined recursively as such: +A representation of a tuple. In particular, `n`-tuples are defined recursively +as follows: `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩` We allow empty tuples. For a `Tuple`-like type with opposite "endian", refer to `Mathlib.Data.Vector`. + +Keep in mind a tuple in Lean already exists but it differs in two ways: + +1. It is right associative. That is, `(x₁, x₂, x₃)` evaluates to + `(x₁, (x₂, x₃))` instead of `((x₁, x₂), x₃)`. +2. Internally a tuple is syntactic sugar for nested `Prod` instances. Inputs + types of `Prod` are not required to be the same meaning non-homogeneous + collections are allowed. + +In general, prefer using `Prod` over this `Tuple` definition. This exists solely +for proving theorems outlined in Enderton's book. -/ inductive Tuple : (α : Type u) → (size : Nat) → Type u where | nil : Tuple α 0 diff --git a/MathematicalIntroductionLogic/Tuple/Generic.lean b/MathematicalIntroductionLogic/Tuple/Generic.lean new file mode 100644 index 0000000..77fd19a --- /dev/null +++ b/MathematicalIntroductionLogic/Tuple/Generic.lean @@ -0,0 +1,164 @@ +import MathematicalIntroductionLogic.Tuple.Basic + +/-- +The following describes a so-called "generic" tuple. Like a `Tuple`, an +`n`-tuple is defined recursively like so: + + `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩` + +Unlike `Tuple`, a "generic" 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, but necessary to +prove certain theorems (e.g. `Chapter0.lemma_0a`). In other words, `Tuple` 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) → Tuple α r → GTuple α (p + q, r) + +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 Tuple + +-- ======================================== +-- Normalization +-- ======================================== + +/-- +Converts an `GTuple` into "normal form". +-/ +def norm : GTuple α (m, n) → Tuple α (m + n) + | g[] => t[] + | snoc is ts => Tuple.concat is.norm ts + +/-- +Normalization of an empty `GTuple` yields an empty `Tuple`. +-/ +theorem norm_nil_eq_nil : @norm α 0 0 nil = Tuple.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 : Tuple α n} + : norm (snoc g[] ts) = cast (by simp) ts := by + unfold norm norm + rw [Tuple.nil_concat_self_eq_self] + +/-- +Normalization distributes across `Tuple.snoc` calls. +-/ +theorem norm_snoc_snoc_norm + : norm (snoc as (Tuple.snoc bs b)) = Tuple.snoc (norm (snoc as bs)) b := by + unfold norm + rw [←Tuple.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₂ : Tuple α n} + : norm (snoc t₁ t₂) = Tuple.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) → Tuple α 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 [Tuple.self_take_zero_eq_nil] + simp + | snoc tf tl => by + unfold fst + conv => rhs; unfold norm + rw [Tuple.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₂ : Tuple α (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) → Tuple α n + | g[] => t[] + | snoc _ ts => ts + +end GTuple