Mathematical Introduction to Logic. Finish proving lemma 0A.

bookshelf/Bookshelf/Tuple.lean

@@ -34,7 +34,7 @@ namespace Tuple
  - Coercions
  - -------------------------------------/
 
-scoped instance : CoeOut (Tuple α (min (n + m) n)) (Tuple α n) where
+scoped instance : CoeOut (Tuple α (min (m + n) m)) (Tuple α m) where
   coe := cast (by simp)
 
 scoped instance : Coe (Tuple α 0) (Tuple α (min n 0)) where
@@ -52,7 +52,7 @@ scoped instance : Coe (Tuple α n) (Tuple α (0 + n)) where
 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
+scoped instance : Coe (Tuple α m) (Tuple α (min (m + n) m)) where
   coe := cast (by simp)
 
 /- -------------------------------------
@@ -127,7 +127,6 @@ def cons : Tuple α n → α → Tuple α (n + 1)
 Join two `Tuple`s together end to end.
 -/
 def concat : Tuple α m → Tuple α n → Tuple α (m + n)
-  | t[], ts => ts
   | is, t[] => is
   | is, snoc ts t => snoc (concat is ts) t
 
@@ -143,9 +142,26 @@ theorem self_concat_nil_eq_self (t : Tuple α m) : concat t t[] = t :=
 Concatenating `nil` with a `Tuple` yields the `Tuple`.
 -/
 theorem nil_concat_self_eq_self (t : Tuple α m) : concat t[] t = t :=
-  match t with
+  Tuple.recOn
-  | t[] => rfl
+    t
-  | snoc _ _ => rfl
+    (by unfold concat; simp)
+    (@fun n as a ih => by
+      unfold concat
+      rw [ih]
+      suffices HEq (snoc (cast (_ : Tuple α n = Tuple α (0 + n)) as) a) ↑(snoc as a)
+        from eq_of_heq this
+      have h₁ := Eq.recOn
+        (motive := fun x h => HEq
+          (snoc (cast (show Tuple α n = Tuple α 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 (_ : Tuple α n = Tuple α (0 + n)) as) a)
+          (cast h (snoc as a)))
+        (show Tuple α (n + 1) = Tuple α (0 + (n + 1)) by simp)
+        h₁)
 
 /--
 Concatenating a `Tuple` to a nonempty `Tuple` moves `concat` calls closer to
@@ -153,16 +169,7 @@ expression leaves.
 -/
 theorem concat_snoc_snoc_concat {bs : Tuple α n}
   : concat as (snoc bs b) = snoc (concat as bs) b :=
-  match as with
+  rfl
-  | 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.
@@ -171,7 +178,7 @@ 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)
+    (fun _ _ => by simp; unfold concat concat; rfl)
 
 /- -------------------------------------
  - Initial sequences

mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean

@@ -37,41 +37,70 @@ macro_rules
 
 namespace XTuple
 
+open scoped Tuple
+
+/- -------------------------------------
+ - Normalization
+ - -------------------------------------/
+
 /--
 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 => Tuple.concat is.norm ts
 
 /--
-Casts a tuple indexed by `m` to one indexed by `n`.
+Normalization of an empty `XTuple` yields an empty `Tuple`.
 -/
-theorem lift_eq_size : (m = n) → (Tuple α m = Tuple α n) :=
+theorem norm_nil_eq_nil : @norm α 0 0 nil = Tuple.nil :=
-  fun h => by rw [h]
+  rfl
 
 /--
-Normalization distributes when the `snd` component is `nil`.
+Normalization of a pseudo-empty `XTuple` yields an empty `Tuple`.
 -/
-theorem distrib_norm_snoc_nil {t : XTuple α (p, q)}
+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 :=
-  sorry
+  XTuple.casesOn t
+    (motive := fun _ t => norm (snoc t t[]) = norm t)
+    (by simp; unfold norm norm; rfl)
+    (fun tf tl => by
+      simp
+      conv => lhs; unfold norm)
 
 /--
-Normalizing an `XTuple` is equivalent to concatenating the `fst` component (in
+Normalization eliminates `snoc` when the `fst` component is `nil`.
-normal form) with the second.
+-/
+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₂) = t₁.norm.concat t₂ :=
+  : norm (snoc t₁ t₂) = Tuple.concat t₁.norm t₂ := by
-  Tuple.recOn
+  conv => lhs; unfold norm
-    (motive := fun k t => norm (snoc t₁ t) = t₁.norm.concat t)
+
-    t₂
+/- -------------------------------------
-    (calc
+ - Equality
-      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
@@ -80,6 +109,10 @@ 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`.
 -/
@@ -106,22 +139,22 @@ def fst : XTuple α (m, n) → Tuple α m
 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))
+theorem self_fst_eq_norm_take (t : XTuple α (m, n)) : t.fst = t.norm.take m :=
-  : cast (by simp) (t.norm.take m) = t.fst :=
+  match t with
-  XTuple.casesOn
+  | x[] => by unfold fst; rw [Tuple.self_take_zero_eq_nil]; simp
-    (motive := fun (m, n) t => cast (by simp) (t.norm.take m) = t.fst)
+  | snoc tf tl => by
-    t
+    unfold fst
-    rfl
+    conv => rhs; unfold norm
-    (@fun p q r t₁ t₂ => sorry)
+    rw [Tuple.eq_take_concat]
+    simp
 
 /--
-If the normal form of our `XTuple` is the same as another `Tuple`, the `fst`
+If the normal form of an `XTuple` is equal to a `Tuple`, the `fst` component
-component must be a prefix of the second.
+must be a prefix of the `Tuple`.
 -/
 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
+  : (t₁.norm = t₂) → (t₁.fst = t₂.take m) :=
-  intro h
+  fun h => by rw [self_fst_eq_norm_take, h]
-  sorry
 
 /--
 Returns the first component of our `XTuple`. For example, the first component of
@@ -131,6 +164,10 @@ def snd : XTuple α (m, n) → Tuple α n
   | x[] => t[]
   | snoc _ ts => ts
 
+/- -------------------------------------
+ - Lemma 0A
+ - -------------------------------------/
+
 section
 
 variable {k m n : Nat}
@@ -152,6 +189,16 @@ lemma n_eq_succ_k : n = k + 1 :=
     _ = 1 + k + m' - m' := by rw [Nat.add_assoc, Nat.add_comm]
     _ = 1 + k := by simp
     _ = k + 1 := by rw [Nat.add_comm]
+  
+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
+  
+lemma n_geq_one : 1 ≤ n := by
+  rw [n_eq_succ_k p q]
+  simp
 
 lemma min_comm_succ_eq : min (m + k) (k + 1) = k + 1 :=
   Nat.recOn k
@@ -162,16 +209,22 @@ lemma min_comm_succ_eq : min (m + k) (k + 1) = k + 1 :=
         _ = 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.
+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
+
+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]
 
 def cast_norm : XTuple α (n, m - 1) → Tuple α (m + k)
-  | xs => cast (lift_eq_size q) xs.norm 
+  | xs => cast (by rw [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
+  | xs => cast (by rw [n_eq_succ_k p q]) xs.fst
   
-def cast_init_seq (ys : Tuple α (m + k)) :=
+def cast_take (ys : Tuple α (m + k)) :=
-  cast (lift_eq_size (min_comm_succ_eq p)) (ys.take (k + 1))
+  cast (by rw [min_comm_succ_eq p]) (ys.take (k + 1))
 
 end Lemma_0a
 
@@ -181,8 +234,44 @@ 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_norm q xs = ys) → (cast_fst p q xs = cast_init_seq p ys) :=
+  : (cast_norm q xs = ys) → (cast_fst p q xs = cast_take p ys) := by
-  fun h => sorry
+  intro h
+  suffices HEq
+    (cast (_ : Tuple α n = Tuple α (k + 1)) (fst xs))
+    (cast (_ : Tuple α (min (m + k) (k + 1)) = Tuple α (k + 1)) (Tuple.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 [self_fst_eq_norm_take]
+    unfold cast_norm at h
+    simp at h
+    rw [←h, ←n_eq_succ_k p q]
+    have h₂ := Eq.recOn
+      (motive := fun x h => HEq
+        (Tuple.take xs.norm n)
+        (Tuple.take (cast (show Tuple α (n + (m - 1)) = Tuple α 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 (Tuple.take xs.norm n))
+        (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