Add utilities around Tuples.

* Include convenience coercions.
* Example that demonstrates how heterogeneous equality works.
* Add a collection of theorems.
* Fix incorrect definitions (e.g. `take`).

bookshelf/Bookshelf/Tuple.lean

@@ -3,11 +3,9 @@
 
 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.NormCast
 import Mathlib.Tactic.Ring
 
 /--
@@ -18,10 +16,6 @@ As described in [1], `n`-tuples are defined recursively as such:
 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
@@ -36,6 +30,35 @@ macro_rules
 
 namespace Tuple
 
+/- -------------------------------------
+ - Coercions
+ - -------------------------------------/
+
+scoped instance : CoeOut (Tuple α (min (n + m) n)) (Tuple α n) where
+  coe := cast (by simp)
+
+scoped instance : Coe (Tuple α 0) (Tuple α (min n 0)) where
+  coe := cast (by rw [Nat.min_zero])
+
+scoped instance : Coe (Tuple α 0) (Tuple α (min 0 n)) where
+  coe := cast (by rw [Nat.zero_min])
+
+scoped instance : Coe (Tuple α n) (Tuple α (min n n)) where
+  coe := cast (by simp)
+
+scoped instance : Coe (Tuple α n) (Tuple α (0 + n)) where
+  coe := cast (by simp)
+
+scoped instance : Coe (Tuple α (min m n + 1)) (Tuple α (min (m + 1) (n + 1))) where
+  coe := cast (by rw [Nat.min_succ_succ])
+
+scoped instance : Coe (Tuple α n) (Tuple α (min (n + m) n)) where
+  coe := cast (by simp)
+
+/- -------------------------------------
+ - Equality
+ - -------------------------------------/
+
 theorem eq_nil : @Tuple.nil α = t[] := rfl
 
 theorem eq_iff_singleton : (a = b) ↔ (t[a] = t[b]) := by
@@ -68,6 +91,10 @@ protected def hasDecEq [DecidableEq α] (t₁ t₂ : Tuple α n) : Decidable (Eq
 
 instance [DecidableEq α] : DecidableEq (Tuple α n) := Tuple.hasDecEq
 
+/- -------------------------------------
+ - Basic API
+ - -------------------------------------/
+
 /--
 Returns the number of entries of the `Tuple`.
 -/
@@ -76,14 +103,14 @@ def size (_ : Tuple α n) : Nat := n
 /--
 Returns all but the last entry of the `Tuple`.
 -/
-def init : Tuple α n → 1 ≤ n → Tuple α (n - 1)
+def init : (t : Tuple α (n + 1)) → Tuple α n
-  | snoc vs _, _ => vs
+  | snoc vs _ => vs
 
 /--
 Returns the last entry of the `Tuple`.
 -/
-def last : Tuple α n → 1 ≤ n → α
+def last : Tuple α (n + 1) → α
-  | snoc _ v, _ => v  
+  | snoc _ v => v
 
 /--
 Prepends an entry to the start of the `Tuple`.
@@ -92,25 +119,142 @@ def cons : Tuple α n → α → Tuple α (n + 1)
   | t[], a => t[a]
   | snoc ts t, a => snoc (cons ts a) t
 
+/- -------------------------------------
+ - Concatenation
+ - -------------------------------------/
+
 /--
 Join two `Tuple`s together end to end.
 -/
 def concat : Tuple α m → Tuple α n → Tuple α (m + n)
-  | t[], ts => cast (by simp) ts
+  | t[], ts => 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`.
+Concatenating a `Tuple` with `nil` yields the original `Tuple`.
 -/
-def take (t : Tuple α n) (k : Nat) (p : 1 ≤ k ∧ k ≤ n) : Tuple α k :=
+theorem self_concat_nil_eq_self (t : Tuple α m) : concat t t[] = t :=
-  have _ : 1 ≤ n := Nat.le_trans p.left p.right
   match t with
-  | @snoc _ n' init last => by
+  | t[] => rfl
-      by_cases h : k = n' + 1
+  | snoc _ _ => rfl
-      · 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
+Concatenating `nil` with a `Tuple` yields the `Tuple`.
-          by simp at h'; exact h')
+-/
+theorem nil_concat_self_eq_self (t : Tuple α m) : concat t[] t = t :=
+  match t with
+  | t[] => rfl
+  | snoc _ _ => rfl
+
+/--
+Concatenating a `Tuple` to a nonempty `Tuple` moves `concat` calls closer to
+expression leaves.
+-/
+theorem concat_snoc_snoc_concat {bs : Tuple α n}
+  : concat as (snoc bs b) = snoc (concat as bs) b :=
+  match as with
+  | t[] => by
+    unfold concat
+    simp
+    show cast (show Tuple α (n + 1) = Tuple α (0 + (n + 1)) by simp) (snoc bs b)
+            = cast rfl (snoc (cast (show Tuple α n = Tuple α (0 + n) by simp) bs) b)
+    congr
+    all_goals simp
+    exact Eq.recOn (show Tuple α n = Tuple α (0 + n) by simp) (HEq.refl bs)
+  | snoc _ _ => rfl
+
+/--
+`snoc` is equivalent to concatenating the `init` and `last` element together.
+-/
+theorem snoc_eq_init_concat_last (as : Tuple α m) : snoc as a = concat as t[a] :=
+  Tuple.casesOn (motive := fun _ t => snoc t a = concat t t[a])
+    as
+    rfl
+    (fun is a' => by simp; unfold concat concat; rfl)
+
+/- -------------------------------------
+ - Initial sequences
+ - -------------------------------------/
+
+/--
+Take the first `k` entries from the `Tuple` to form a new `Tuple`, or the entire
+`Tuple` if `k` exceeds the number of entries.
+-/
+def take (t : Tuple α n) (k : Nat) : Tuple α (min n k) :=
+  if h : n ≤ k then
+    cast (by rw [min_eq_left h]) t
+  else
+    match t with
+    | t[] => t[]
+    | @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 `Tuple` should yield an empty one.
+-/
+theorem self_take_zero_eq_nil (t : Tuple α n) : take t 0 = @nil α :=
+  Tuple.recOn (motive := fun _ t => take t 0 = @nil α) t
+    (by simp; rfl)
+    (fun as a ih => by unfold take; simp; rw [ih]; simp)
+
+/--
+Taking any number of entries from an empty `Tuple` should yield an empty one.
+-/
+theorem nil_take_zero_eq_nil (k : Nat) : (take (@nil α) k) = @nil α := by
+  cases k <;> (unfold take; simp)
+
+/--
+Taking `n` entries from a `Tuple` of size `n` should yield the same `Tuple`.
+-/
+theorem self_take_size_eq_self (t : Tuple α n) : take t n = t :=
+  Tuple.casesOn (motive := fun x t => take t x = t) t
+    (by simp; rfl)
+    (fun as a => by unfold take; simp)
+
+/--
+Taking all but the last entry of a `Tuple` is the same result, regardless of the
+value of the last entry.
+-/
+theorem take_subst_last {as : Tuple α n} (a₁ a₂ : α)
+  : take (snoc as a₁) n = take (snoc as a₂) n := by
+  unfold take
+  simp
+
+/--
+Taking `n` elements from a tuple of size `n + 1` is the same as invoking `init`.
+-/
+theorem init_eq_take_pred (t : Tuple α (n + 1)) : take t n = init t :=
+  match t with
+  | snoc as a => by unfold init take; simp; rw [self_take_size_eq_self]; simp
+
+/--
+If two `Tuple`s are equal, then any initial sequences of those two `Tuple`s are
+also equal.
+-/
+theorem eq_tuple_eq_take {t₁ t₂ : Tuple α n}
+  : (t₁ = t₂) → (t₁.take k = t₂.take k) :=
+  fun h => by rw [h]
+
+/--
+Given a `Tuple` of size `k`, concatenating an arbitrary `Tuple` and taking `k`
+elements yields the original `Tuple`.
+-/
+theorem eq_take_concat {t₁ : Tuple α m} {t₂ : Tuple α n}
+  : take (concat t₁ t₂) m = t₁ :=
+  Tuple.recOn
+    (motive := fun x t => take (concat t₁ t) m = t₁) t₂
+    (by simp; rw [self_concat_nil_eq_self, self_take_size_eq_self])
+    (@fun n' as a ih => by
+      simp
+      rw [concat_snoc_snoc_concat]
+      unfold take
+      simp
+      rw [ih]
+      simp)
 
 end Tuple

bookshelf/Bookshelf/Vector.lean

@@ -26,23 +26,22 @@ def size (_ : Vector α n) : Nat := n
 /--
 Returns the first entry of the `Vector`.
 -/
-def head : Vector α n → 1 ≤ n → α
+def head : Vector α (n + 1) → α
-  | cons v _, _ => v
+  | cons v _ => v
 
 /--
 Returns the last entry of the `Vector`.
 -/
-def last (v : Vector α n) : 1 ≤ n → α :=
+def last : Vector α (n + 1) → α
-  fun h =>
+  | cons v vs => if _ : n = 0 then v else
-    match v with
+      match n with
-    | nil => by ring_nf at h; exact h.elim
+      | _ + 1 => vs.last
-    | @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)
+def tail : Vector α (n + 1) → Vector α n
-  | cons _ vs, _ => vs
+  | cons _ vs => vs
 
 /--
 Appends an entry to the end of the `Vector`.

mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean

@@ -43,14 +43,36 @@ 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
+  | snoc  is ts => Tuple.concat is.norm ts
 
 /--
 Casts a tuple indexed by `m` to one indexed by `n`.
 -/
-theorem cast_eq_size : (m = n) → (Tuple α m = Tuple α n) :=
+theorem lift_eq_size : (m = n) → (Tuple α m = Tuple α n) :=
   fun h => by rw [h]
 
+/--
+Normalization distributes when the `snd` component is `nil`.
+-/
+theorem distrib_norm_snoc_nil {t : XTuple α (p, q)}
+  : norm (snoc t t[]) = norm t :=
+  sorry
+
+/--
+Normalizing an `XTuple` is equivalent to concatenating the `fst` component (in
+normal form) with the second.
+-/
+theorem norm_snoc_eq_concat {t₁ : XTuple α (p, q)} {t₂ : Tuple α n}
+  : norm (snoc t₁ t₂) = t₁.norm.concat t₂ :=
+  Tuple.recOn
+    (motive := fun k t => norm (snoc t₁ t) = t₁.norm.concat t)
+    t₂
+    (calc
+      norm (snoc t₁ t[])
+          = t₁.norm := distrib_norm_snoc_nil
+        _ = t₁.norm.concat t[] := by rw [Tuple.self_concat_nil_eq_self])
+    (sorry)
+
 /--
 Implements Boolean equality for `XTuple α n` provided `α` has decidable
 equality.
@@ -76,36 +98,80 @@ def length : XTuple α n → Nat
 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
+def fst : XTuple α (m, n) → Tuple α m
-  | snoc ts _, _ => ts.norm
+  | 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))
+  : cast (by simp) (t.norm.take m) = t.fst :=
+  XTuple.casesOn
+    (motive := fun (m, n) t => cast (by simp) (t.norm.take m) = t.fst)
+    t
+    rfl
+    (@fun p q r t₁ t₂ => sorry)
+
+/--
+If the normal form of our `XTuple` is the same as another `Tuple`, the `fst`
+component must be a prefix of the second.
+-/
+theorem norm_eq_fst_eq_take {t₁ : XTuple α (m, n)} {t₂ : Tuple α (m + n)}
+  : (t₁.norm = t₂) → cast (by simp) (t₂.take m) = t₁.fst := by
+  intro h
+  sorry
+
+/--
+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
 
 section
 
 variable {k m n : Nat}
-variable (p : n + (m - 1) = m + k)
+variable (p : 1 ≤ m)
-variable (qₘ : 1 ≤ m)
+variable (q : n + (m - 1) = m + k)
 
 namespace Lemma_0a
 
-lemma aux1 : n = k + 1 :=
+lemma n_eq_succ_k : n = k + 1 :=
   let ⟨m', h⟩ := Nat.exists_eq_succ_of_ne_zero $ show m ≠ 0 by
     intro h
-    have ff : 1 ≤ 0 := h ▸ qₘ
+    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 [p, h]
+    _ = 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]
 
-lemma aux2 : 1 ≤ k + 1 ∧ k + 1 ≤ m + k := And.intro
+lemma min_comm_succ_eq : min (m + k) (k + 1) = k + 1 :=
-  (by simp)
+  Nat.recOn k
-  (calc
+    (by simp; exact p)
-    k + 1 ≤ k + m := Nat.add_le_add_left qₘ k
+    (fun k' ih => calc
-        _ = m + k := by rw [Nat.add_comm])
+      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])
+
+-- TODO: Consider using coercions and heterogeneous equality isntead of these.
+
+def cast_norm : XTuple α (n, m - 1) → Tuple α (m + k)
+  | xs => cast (lift_eq_size q) xs.norm 
+
+def cast_fst : XTuple α (n, m - 1) → Tuple α (k + 1)
+  | xs => cast (lift_eq_size (n_eq_succ_k p q)) xs.fst
+  
+def cast_init_seq (ys : Tuple α (m + k)) :=
+  cast (lift_eq_size (min_comm_succ_eq p)) (ys.take (k + 1))
 
 end Lemma_0a
 
@@ -115,9 +181,8 @@ open Lemma_0a
 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_norm q xs = ys) → (cast_fst p q xs = cast_init_seq p ys) :=
-  → (cast (cast_eq_size (aux1 p qₘ)) (xs.first qₙ) = ys.take (k + 1) (aux2 qₘ))
+  fun h => sorry
-  := sorry
 
 end