`Tuple`s already exist in Lean; nest inside Enderton section instead.

Bookshelf.lean

@@ -1,3 +1,2 @@
 import Bookshelf.List
 import Bookshelf.Real
-import Bookshelf.Tuple

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
 

MathematicalIntroductionLogic.lean

@@ -1 +1,2 @@
-import MathematicalIntroductionLogic.Chapter0
+import MathematicalIntroductionLogic.Chapter0
+import MathematicalIntroductionLogic.Tuple

MathematicalIntroductionLogic/Chapter0.lean

@@ -4,174 +4,7 @@ Chapter 0
 Useful Facts About Sets
 -/
 
-import Bookshelf.Tuple
+import MathematicalIntroductionLogic.Tuple.Generic
-
-/--
-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
 
 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ₘ₊ₖ⟩`.
+Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Then
-Then `x₁ = ⟨y₁, ..., yₖ₊₁⟩`.
+`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

MathematicalIntroductionLogic/Tuple.lean

@@ -0,0 +1,2 @@
+import MathematicalIntroductionLogic.Tuple.Basic
+import MathematicalIntroductionLogic.Tuple.Generic

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

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