From 87c1fb2a240cf8f3f3c01fba193e3da90db77e19 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 8 Apr 2023 10:46:27 -0600 Subject: [PATCH] Use induction/cases tactics where it makes sense. --- common/Common/Sequence/Arithmetic.lean | 28 ++-------- common/Common/Sequence/Geometric.lean | 11 ++-- common/Common/Tuple.lean | 54 ++++++++++--------- .../Enderton/Chapter0.lean | 14 ++--- 4 files changed, 45 insertions(+), 62 deletions(-) diff --git a/common/Common/Sequence/Arithmetic.lean b/common/Common/Sequence/Arithmetic.lean index 16d4166..cb6df03 100644 --- a/common/Common/Sequence/Arithmetic.lean +++ b/common/Common/Sequence/Arithmetic.lean @@ -27,17 +27,16 @@ The recursive definition and closed definitions of an arithmetic sequence are equivalent. -/ theorem term_recursive_closed (seq : Arithmetic) (n : Nat) - : seq.termRecursive n = seq.termClosed n := - Nat.recOn - n - (by unfold termRecursive termClosed; norm_num) - (fun n ih => calc + : seq.termRecursive n = seq.termClosed n := by + induction n with + | zero => unfold termRecursive termClosed; norm_num + | succ n ih => calc termRecursive seq (Nat.succ n) = seq.Δ + seq.termRecursive n := rfl _ = seq.Δ + seq.termClosed n := by rw [ih] _ = seq.Δ + (seq.a₀ + seq.Δ * n) := rfl _ = seq.a₀ + seq.Δ * (n + 1) := by ring - _ = termClosed seq (n + 1) := rfl) + _ = termClosed seq (n + 1) := rfl /--[1] Summation of the first `n` terms of an arithmetic sequence. @@ -46,21 +45,4 @@ def sum : Arithmetic → Nat → Int | _, 0 => 0 | seq, (n + 1) => seq.termClosed n + seq.sum n -/--[1] -The closed formula of the summation of the first `n` terms of an arithmetic -series. ---/ -theorem sum_closed_formula (seq : Arithmetic) (n : Nat) - : seq.sum n = (n / 2) * (seq.a₀ + seq.termClosed (n - 1)) := - Nat.recOn - n - (by unfold sum termClosed; norm_num) - (fun n ih => calc - sum seq n.succ - = seq.termClosed n + seq.sum n := rfl - _ = seq.termClosed n + (n / 2 * (seq.a₀ + seq.termClosed (n - 1))) := by rw [ih] - _ = seq.a₀ + seq.Δ * n + (n / 2 * (seq.a₀ + (seq.a₀ + seq.Δ * ↑(n - 1)))) := rfl - -- TODO: To continue, need to find how to deal with division. - _ = ↑(n + 1) / 2 * (seq.a₀ + seq.termClosed n) := by sorry) - end Arithmetic diff --git a/common/Common/Sequence/Geometric.lean b/common/Common/Sequence/Geometric.lean index 81797c2..e5079a9 100644 --- a/common/Common/Sequence/Geometric.lean +++ b/common/Common/Sequence/Geometric.lean @@ -27,17 +27,16 @@ The recursive definition and closed definitions of a geometric sequence are equivalent. -/ theorem term_recursive_closed (seq : Geometric) (n : Nat) - : seq.termRecursive n = seq.termClosed n := - Nat.recOn - n - (by unfold termClosed termRecursive; norm_num) - (fun n ih => calc + : seq.termRecursive n = seq.termClosed n := by + induction n with + | zero => unfold termClosed termRecursive; norm_num + | succ n ih => calc seq.termRecursive (n + 1) = seq.r * (seq.termRecursive n) := rfl _ = seq.r * (seq.termClosed n) := by rw [ih] _ = seq.r * (seq.a₀ * seq.r ^ n) := rfl _ = seq.a₀ * seq.r ^ (n + 1) := by ring - _ = seq.termClosed (n + 1) := rfl) + _ = seq.termClosed (n + 1) := rfl /--[1] Summation of the first `n` terms of a geometric sequence. diff --git a/common/Common/Tuple.lean b/common/Common/Tuple.lean index 52c8865..5040a18 100644 --- a/common/Common/Tuple.lean +++ b/common/Common/Tuple.lean @@ -133,11 +133,10 @@ 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 := - Tuple.recOn - t - (by unfold concat; simp) - (@fun n as a ih => by +theorem nil_concat_self_eq_self (t : Tuple α m) : concat t[] t = t := by + induction t with + | nil => unfold concat; simp + | @snoc n as a ih => unfold concat rw [ih] suffices HEq (snoc (cast (_ : Tuple α n = Tuple α (0 + n)) as) a) ↑(snoc as a) @@ -153,7 +152,7 @@ theorem nil_concat_self_eq_self (t : Tuple α m) : concat t[] t = t := (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₁) + h₁ /-- Concatenating a `Tuple` to a nonempty `Tuple` moves `concat` calls closer to @@ -166,11 +165,11 @@ theorem concat_snoc_snoc_concat {bs : Tuple α n} /-- `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 _ _ => by simp; unfold concat concat; rfl) +theorem snoc_eq_init_concat_last (as : Tuple α m) + : snoc as a = concat as t[a] := by + cases as with + | nil => rfl + | snoc _ _ => simp; unfold concat concat; rfl -- ======================================== -- Initial sequences @@ -196,10 +195,10 @@ def take (t : Tuple α n) (k : Nat) : Tuple α (min n k) := /-- 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) +theorem self_take_zero_eq_nil (t : Tuple α n) : take t 0 = @nil α := by + induction t with + | nil => simp; rfl + | snoc as a ih => unfold take; simp; rw [ih]; simp /-- Taking any number of entries from an empty `Tuple` should yield an empty one. @@ -210,10 +209,10 @@ theorem nil_take_zero_eq_nil (k : Nat) : (take (@nil α) k) = @nil α := by /-- 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) +theorem self_take_size_eq_self (t : Tuple α n) : take t n = t := by + cases t with + | nil => simp; rfl + | snoc as a => unfold take; simp /-- Taking all but the last entry of a `Tuple` is the same result, regardless of the @@ -229,7 +228,11 @@ 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 + | 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 @@ -244,16 +247,15 @@ 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 + : take (concat t₁ t₂) m = t₁ := by + induction t₂ with + | nil => simp; rw [self_concat_nil_eq_self, self_take_size_eq_self] + | @snoc n' as a ih => simp rw [concat_snoc_snoc_concat] unfold take simp rw [ih] - simp) + simp end Tuple diff --git a/mathematical-introduction-logic/Enderton/Chapter0.lean b/mathematical-introduction-logic/Enderton/Chapter0.lean index 6189b37..74ec787 100644 --- a/mathematical-introduction-logic/Enderton/Chapter0.lean +++ b/mathematical-introduction-logic/Enderton/Chapter0.lean @@ -66,18 +66,18 @@ theorem norm_snoc_nil_nil_eq_nil : @norm α 0 0 (snoc x[] t[]) = t[] := by Normalization elimates `snoc` when the `snd` component is `nil`. -/ theorem norm_snoc_nil_elim {t : XTuple α (p, q)} - : norm (snoc t t[]) = norm t := - XTuple.casesOn t - (motive := fun _ t => norm (snoc t t[]) = norm t) - (by simp; unfold norm norm; rfl) - (fun tf tl => by + : norm (snoc t t[]) = norm t := by + cases t with + | nil => simp; unfold norm norm; rfl + | snoc tf tl => simp - conv => lhs; unfold norm) + 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 +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]