Formulate Lemma0A.

bookshelf/Bookshelf.lean

@@ -1,3 +1,4 @@
 import Bookshelf.Sequence.Arithmetic
 import Bookshelf.Sequence.Geometric
 import Bookshelf.Tuple
+import Bookshelf.Vector

bookshelf/Bookshelf/Tuple.lean

@@ -0,0 +1,118 @@
+/-
+# References
+
+1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
+   Harcourt/Academic Press, 2001.
+2. Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in
+   Mathematics. Cham: Springer International Publishing, 2015.
+   https://doi.org/10.1007/978-3-319-11080-6.
+-/
+
+import Mathlib.Tactic.Ring
+
+universe u
+
+/--
+As described in [1], `n`-tuples are defined recursively as such:
+
+  `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩`
+
+We allow for empty tuples; [2] expects this functionality.
+
+For a `Tuple`-like type with opposite "endian", refer to `Vector`.
+
+TODO: It would be nice to define `⟨x⟩ = x`. It's not clear to me yet how to do
+so or whether I could leverage a simple isomorphism everywhere I would like
+this.
+-/
+inductive Tuple : (α : Type u) → (size : Nat) → Type u where
+  | nil : Tuple α 0
+  | snoc : Tuple α n → α → Tuple α (n + 1)
+
+syntax (priority := high) "t[" term,* "]" : term
+
+macro_rules
+  | `(t[]) => `(Tuple.nil)
+  | `(t[$x]) => `(Tuple.snoc t[] $x)
+  | `(t[$xs:term,*, $x]) => `(Tuple.snoc t[$xs,*] $x)
+
+namespace Tuple
+
+theorem eq_nil : @Tuple.nil α = t[] := rfl
+
+theorem eq_iff_singleton : (a = b) ↔ (t[a] = t[b]) := by
+  apply Iff.intro
+  · intro h; rw [h]
+  · intro h; injection h
+
+theorem eq_iff_snoc {t₁ t₂ : Tuple α 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₂ : Tuple α n) : Decidable (Eq t₁ t₂) :=
+  match t₁, t₂ with
+  | t[], t[] => isTrue eq_nil
+  | snoc as a, snoc bs b =>
+    match Tuple.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 (Tuple α n) := Tuple.hasDecEq
+
+/--
+Returns the number of entries of the `Tuple`.
+-/
+def size (_ : Tuple α n) : Nat := n
+
+/--
+Returns all but the last entry of the `Tuple`.
+-/
+def init : Tuple α n → 1 ≤ n → Tuple α (n - 1)
+  | snoc vs _, _ => vs
+
+/--
+Returns the last entry of the `Tuple`.
+-/
+def last : Tuple α n → 1 ≤ n → α
+  | snoc _ v, _ => v  
+
+/--
+Prepends an entry to the start of the `Tuple`.
+-/
+def cons : Tuple α n → α → Tuple α (n + 1)
+  | t[], a => t[a]
+  | snoc ts t, a => snoc (cons ts a) t
+
+/--
+Join two `Tuple`s together end to end.
+-/
+def concat : Tuple α m → Tuple α n → Tuple α (m + n)
+  | t[], ts => cast (by simp) ts
+  | is, t[] => is
+  | is, snoc ts t => snoc (concat is ts) t
+
+/--
+Take the first `k` entries from the `Tuple` to form a new `Tuple`.
+-/
+def take (t : Tuple α n) (k : Nat) (p : 1 ≤ k ∧ k ≤ n) : Tuple α k :=
+  have _ : 1 ≤ n := Nat.le_trans p.left p.right
+  match t with
+  | @snoc _ n' init last => by
+      by_cases h : k = n' + 1
+      · rw [h]; exact snoc init last
+      · exact take init k (And.intro p.left $
+          have h' : k + 1 ≤ n' + 1 := Nat.lt_of_le_of_ne p.right h
+          by simp at h'; exact h')
+
+end Tuple

bookshelf/Bookshelf/Vector.lean

@@ -0,0 +1,54 @@
+import Mathlib.Tactic.Ring
+
+/--
+A list-like structure with its size encoded in the type.
+
+For a `Vector`-like type with opposite "endian", refer to `Tuple`.
+-/
+inductive Vector (α : Type u) : (size : Nat) → Type u where
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n + 1)
+
+syntax (priority := high) "v[" term,* "]" : term
+
+macro_rules
+  | `(v[]) => `(Vector.nil)
+  | `(v[$x]) => `(Vector.cons $x v[])
+  | `(v[$x, $xs:term,*]) => `(Vector.cons $x v[$xs,*])
+
+namespace Vector
+
+/--
+Returns the number of entries in the `Vector`.
+-/
+def size (_ : Vector α n) : Nat := n
+
+/--
+Returns the first entry of the `Vector`.
+-/
+def head : Vector α n → 1 ≤ n → α
+  | cons v _, _ => v
+
+/--
+Returns the last entry of the `Vector`.
+-/
+def last (v : Vector α n) : 1 ≤ n → α :=
+  fun h =>
+    match v with
+    | nil => by ring_nf at h; exact h.elim
+    | @cons _ n' v vs => if h' : n' > 0 then vs.last h' else v
+
+/--
+Returns all but the `head` of the `Vector`.
+-/
+def tail : Vector α n → 1 ≤ n → Vector α (n - 1)
+  | cons _ vs, _ => vs
+
+/--
+Appends an entry to the end of the `Vector`.
+-/
+def snoc : Vector α n → α → Vector α (n + 1)
+  | nil, a => v[a]
+  | cons v vs, a => cons v (snoc vs a)
+
+end Vector

bookshelf/lakefile.lean

@@ -4,9 +4,9 @@ open Lake DSL
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
-package «Common»
+package «Bookshelf»
 
 @[default_target]
-lean_lib «Common» {
-  roots := #["Bookshelf"]
+lean_lib «Bookshelf» {
+  -- add library configuration options here
 }

bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean

@@ -1,6 +0,0 @@
-/-
-# References
-
-1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
-   Harcourt/Academic Press, 2001.
--/

common/Bookshelf/Tuple.lean

@@ -1,93 +0,0 @@
-/-
-# References
-
-1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
-   Harcourt/Academic Press, 2001.
-2. Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in
-   Mathematics. Cham: Springer International Publishing, 2015.
-   https://doi.org/10.1007/978-3-319-11080-6.
--/
-
-import Mathlib.Tactic.Ring
-
-universe u
-
-/--[1]
-An `n`-tuple is defined recursively as:
-
-  `⟨x₁, ..., xₙ₊₁⟩ = ⟨⟨x₁, ..., xₙ⟩, xₙ₊₁⟩`
-
-As [1] notes, it is useful to define `⟨x⟩ = x`. It is not clear this would be
-possible in Lean though.
-
-Though [1] does not describe a notion of an empty tuple, [2] does (though under
-the name of a "list").
---/
-inductive Tuple : (α : Type u) → Nat → Type u where
-  | nil : Tuple α 0
-  | snoc : {n : Nat} → Tuple α n → α → Tuple α (n + 1)
-
-syntax (priority := high) "⟨" term,+ "⟩" : term
-
--- Notice the ambiguity this syntax introduces. For example, pattern `⟨a, b⟩`
--- could refer to a `2`-tuple or an `n`-tuple, where `a` is an `(n-1)`-tuple.
-macro_rules
-  | `(⟨$x⟩) => `(Tuple.snoc Tuple.nil $x)
-  | `(⟨$xs:term,*, $x⟩) => `(Tuple.snoc ⟨$xs,*⟩ $x)
-
-namespace Tuple
-
-def length : Tuple α n → Nat
-  | Tuple.nil => 0
-  | Tuple.snoc init _ => length init + 1
-
-theorem nil_length_zero : length (@Tuple.nil α) = 0 :=
-  rfl
-
-theorem snoc_length_succ : length (Tuple.snoc init last) = length init + 1 :=
-  rfl
-
-theorem tuple_length {n : Nat} (t : Tuple α n) : length t = n :=
-  Tuple.recOn t nil_length_zero
-    fun _ _ ih => by
-      rw [snoc_length_succ]
-      norm_num
-      exact ih
-
-def head : {n : Nat} → Tuple α n → n ≥ 1 → α
-  | n + 1, Tuple.snoc init last, h => by
-    by_cases k : 0 = n
-    · exact last
-    · have h' : 0 ≤ n := Nat.le_of_succ_le_succ h
-      exact head init (Nat.lt_of_le_of_ne h' k)
-
-def last : Tuple α n → n ≥ 1 → α
-  | Tuple.snoc _ last, _ => last
-
-def index : {n : Nat} → Tuple α n → (k : Nat) → 1 ≤ k ∧ k ≤ n → α
-  | 0, _, m, h => by
-    have ff : 1 ≤ 0 := Nat.le_trans h.left h.right
-    ring_nf at ff
-    exact False.elim ff
-  | n + 1, Tuple.snoc init last, k, h => by
-    by_cases hₖ : k = n + 1
-    · exact last
-    · exact index init k $ And.intro
-        h.left
-        (Nat.le_of_lt_succ $ Nat.lt_of_le_of_ne h.right hₖ)
-
-/-
-
--- TODO: Prove `eq_by_index`.
--- TODO: Prove Lemma 0A [1].
-
-theorem eq_by_index (t₁ t₂ : Tuple α n)
-  : (t₁ = t₂) ↔ (∀ i : Nat, (p : 1 ≤ i ∧ i ≤ n) → index t₁ i p = index t₂ i p) := by
-  apply Iff.intro
-  · intro teq i hᵢ
-    sorry
-  · sorry
-
--/
-
-end Tuple

mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean

@@ -0,0 +1,109 @@
+/-
+# References
+
+1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
+   Harcourt/Academic Press, 2001.
+-/
+
+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
+
+/--
+Converts an `XTuple` into "normal form".
+-/
+def norm : XTuple α (m, n) → Tuple α (m + n)
+  |         x[] => t[]
+  | snoc x[] ts => cast (by simp) ts
+  | snoc  is ts => is.norm.concat ts
+
+/--
+Casts a tuple indexed by `m` to one indexed by `n`.
+-/
+theorem cast_eq_size : (m = n) → (Tuple α m = Tuple α n) :=
+  fun h => by rw [h]
+
+/--
+Implements Boolean equality for `XTuple α n` provided `α` has decidable
+equality.
+-/
+instance BEq [DecidableEq α] : BEq (XTuple α n) where
+  beq t₁ t₂ := t₁.norm == t₂.norm
+
+/--
+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 first : XTuple α (m, n) → 1 ≤ m → Tuple α m
+  | snoc ts _, _ => ts.norm
+
+section
+
+variable {k m n : Nat}
+variable (p : n + (m - 1) = m + k)
+variable (qₙ : 1 ≤ n)
+variable (qₘ : 1 ≤ m)
+
+namespace Lemma_0a
+
+lemma aux1 : n = k + 1 := sorry
+
+lemma aux2 : 1 ≤ m → 1 ≤ k + 1 ∧ k + 1 ≤ m + k := sorry
+
+end Lemma_0a
+
+open Lemma_0a
+
+/--[1]
+Assume that ⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩. Then x₁ = ⟨y₁, ..., yₖ₊₁⟩.
+-/
+theorem lemma_0a (xs : XTuple α (n, m - 1)) (ys : Tuple α (m + k))
+  : (cast (cast_eq_size p) xs.norm = ys)
+  → (cast (cast_eq_size aux1) (xs.first qₙ) = ys.take (k + 1) (aux2 qₘ))
+  := sorry
+
+end
+
+end XTuple

mathematical-introduction-logic/lake-manifest.json

@@ -0,0 +1,28 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"path": {"name": "Bookshelf", "dir": "./../bookshelf"}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "7e974fd3806866272e9f6d9e44fa04c210a21f87",
+    "name": "mathlib",
+    "inputRev?": null}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf",
+    "name": "Qq",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "ba61f7fec6174d8c7d2796457da5a8d0b0da44c6",
+    "name": "aesop",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "de7e2a79905a3f87cad1ad5bf57045206f9738c7",
+    "name": "std",
+    "inputRev?": "main"}}]}

mathematical-introduction-logic/lakefile.lean

@@ -3,6 +3,8 @@ open Lake DSL
 
 package «mathematical-introduction-logic»
 
+require Bookshelf from "../bookshelf"
+
 @[default_target]
 lean_lib «MathematicalIntroductionLogic» {
   -- add library configuration options here