diff --git a/bookshelf/Bookshelf/Tuple.lean b/bookshelf/Bookshelf/Tuple.lean index 2e098cb..1ab7204 100644 --- a/bookshelf/Bookshelf/Tuple.lean +++ b/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) - | snoc vs _, _ => vs +def init : (t : Tuple α (n + 1)) → Tuple α n + | snoc vs _ => vs /-- Returns the last entry of the `Tuple`. -/ -def last : Tuple α n → 1 ≤ n → α - | snoc _ v, _ => v +def last : Tuple α (n + 1) → α + | 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 := - have _ : 1 ≤ n := Nat.le_trans p.left p.right +theorem self_concat_nil_eq_self (t : Tuple α m) : concat t t[] = t := 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') + | t[] => rfl + | snoc _ _ => rfl + +/-- +Concatenating `nil` with a `Tuple` yields the `Tuple`. +-/ +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 diff --git a/bookshelf/Bookshelf/Vector.lean b/bookshelf/Bookshelf/Vector.lean index e402f3c..8c9b34d 100644 --- a/bookshelf/Bookshelf/Vector.lean +++ b/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 → α - | cons v _, _ => v +def head : Vector α (n + 1) → α + | 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 +def last : Vector α (n + 1) → α + | cons v vs => if _ : n = 0 then v else + match n with + | _ + 1 => vs.last /-- Returns all but the `head` of the `Vector`. -/ -def tail : Vector α n → 1 ≤ n → Vector α (n - 1) - | cons _ vs, _ => vs +def tail : Vector α (n + 1) → Vector α n + | cons _ vs => vs /-- Appends an entry to the end of the `Vector`. diff --git a/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean b/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean index 04f8741..bc35fe8 100644 --- a/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean +++ b/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 - | snoc ts _, _ => ts.norm +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)) + : 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 (qₘ : 1 ≤ m) +variable (p : 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 - (by simp) - (calc - k + 1 ≤ k + m := Nat.add_le_add_left qₘ k - _ = m + k := by rw [Nat.add_comm]) +lemma min_comm_succ_eq : min (m + k) (k + 1) = k + 1 := + Nat.recOn k + (by simp; exact p) + (fun k' ih => calc + 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 (cast_eq_size (aux1 p qₘ)) (xs.first qₙ) = ys.take (k + 1) (aux2 qₘ)) - := sorry + : (cast_norm q xs = ys) → (cast_fst p q xs = cast_init_seq p ys) := + fun h => sorry end