From b2fddc321d802b291ac49dbdac4cadf13bbb3fe3 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 28 Apr 2023 07:35:58 -0600 Subject: [PATCH] Finish proving partition proofs. --- Bookshelf/List/Basic.lean | 249 +++++++++++--------- OneVariableCalculus/Real/Function/Step.lean | 21 +- OneVariableCalculus/Real/Set/Partition.lean | 56 +++-- TheoremProvingInLean/Avigad/Chapter3.lean | 6 +- 4 files changed, 196 insertions(+), 136 deletions(-) diff --git a/Bookshelf/List/Basic.lean b/Bookshelf/List/Basic.lean index 60ae2bd..9ceeb03 100644 --- a/Bookshelf/List/Basic.lean +++ b/Bookshelf/List/Basic.lean @@ -3,44 +3,27 @@ import Mathlib.Tactic.NormNum namespace List +-- ======================================== +-- Indexing +-- ======================================== + +/-- +Getting an element `i` from a list is equivalent to `get`ting an element `i + 1` +from that list as a tail. +-/ +theorem get_cons_succ_self_eq_get_tail_self + : get (x :: xs) (Fin.succ i) = get xs i := by + conv => lhs; unfold get; simp only + -- ======================================== -- Length -- ======================================== -/-- -Only the empty list has length zero. --/ -theorem length_zero_iff_self_eq_nil : length xs = 0 ↔ xs = [] := by - apply Iff.intro - · intro h - cases xs with - | nil => rfl - | cons a as => simp at h - · intro h - rw [h] - simp - -/-- -If the length of a list is greater than zero, it cannot be `List.nil`. --/ -theorem length_gt_zero_imp_not_nil : xs.length > 0 → xs ≠ [] := by - intro h - by_contra nh - rw [nh] at h - have : 0 > 0 := calc 0 - _ = length [] := by rw [← length_zero_iff_self_eq_nil.mpr nh, nh] - _ > 0 := h - simp at this - --- ======================================== --- Membership --- ======================================== - /-- A list is nonempty if and only if it can be written as a head concatenated with a tail. -/ -theorem self_nonempty_imp_exists_mem : xs ≠ [] ↔ (∃ a as, xs = a :: as) := by +theorem self_neq_nil_imp_exists_mem : xs ≠ [] ↔ (∃ a as, xs = a :: as) := by apply Iff.intro · intro h cases hx : xs with @@ -50,25 +33,45 @@ theorem self_nonempty_imp_exists_mem : xs ≠ [] ↔ (∃ a as, xs = a :: as) := rw [hx] simp +/-- +Only the empty list has length zero. +-/ +theorem eq_nil_iff_length_zero : xs = [] ↔ length xs = 0 := by + apply Iff.intro + · intro h + rw [h] + simp + · intro h + cases xs with + | nil => rfl + | cons a as => simp at h + +/-- +If the length of a list is greater than zero, it cannot be `List.nil`. +-/ +theorem neq_nil_iff_length_gt_zero : xs ≠ [] ↔ xs.length > 0 := by + have : ¬xs = [] ↔ ¬length xs = 0 := Iff.not eq_nil_iff_length_zero + rwa [ + show ¬xs = [] ↔ xs ≠ [] from Iff.rfl, + show ¬length xs = 0 ↔ length xs ≠ 0 from Iff.rfl, + ← zero_lt_iff + ] at this + +-- ======================================== +-- Membership +-- ======================================== + /-- If there exists a member of a list, the list must be nonempty. -/ -theorem nonempty_iff_mem : xs ≠ [] ↔ ∃ x, x ∈ xs := by +theorem exists_mem_iff_neq_nil : (∃ x, x ∈ xs) ↔ xs ≠ [] := by apply Iff.intro + · intro ⟨x, hx⟩ + induction hx <;> simp · intro hx cases xs with | nil => simp at hx | cons a as => exact ⟨a, by simp⟩ - · intro ⟨x, hx⟩ - induction hx <;> simp - -/-- -Getting an element `i` from a list is equivalent to `get`ting an element `i + 1` -from that list as a tail. --/ -theorem get_cons_succ_self_eq_get_tail_self - : get (x :: xs) (Fin.succ i) = get xs i := by - conv => lhs; unfold get; simp only /-- Any value that can be retrieved via `get` must be a member of the list argument. @@ -114,6 +117,44 @@ theorem mem_iff_exists_get {xs : List α} | nil => have nh := i.2; simp at nh | cons a bs => rw [← hi]; exact get_mem_self +-- ======================================== +-- Sublists +-- ======================================== + +/-- +Given nonempty list `xs`, `head` is equivalent to `get`ting the `0`th index. +-/ +theorem head_eq_get_zero {xs : List α} (h : xs ≠ []) + : head xs h = get xs ⟨0, neq_nil_iff_length_gt_zero.mp h⟩ := by + have ⟨a, ⟨as, hs⟩⟩ := self_neq_nil_imp_exists_mem.mp h + subst hs + simp + +/-- +Given nonempty list `xs`, `getLast xs` is equivalent to `get`ting the +`length - 1`th index. +-/ +theorem getLast_eq_get_length_sub_one {xs : List α} (h : xs ≠ []) + : getLast xs h = get xs ⟨xs.length - 1, by + have ⟨_, ⟨_, hs⟩⟩ := self_neq_nil_imp_exists_mem.mp h + rw [hs] + simp⟩ := by + induction xs with + | nil => simp at h + | cons _ as ih => + match as with + | nil => simp + | cons b bs => unfold getLast; rw [ih]; simp + +/-- +If a `List` has a `tail?` defined, it must be nonempty. +-/ +theorem some_tail?_imp_cons (h : tail? xs = some ys) : ∃ x, xs = x :: ys := by + unfold tail? at h + cases xs with + | nil => simp at h + | cons r rs => exact ⟨r, by simp at h; rw [h]⟩ + -- ======================================== -- Zips -- ======================================== @@ -121,7 +162,7 @@ theorem mem_iff_exists_get {xs : List α} /-- The length of a list zipped with its tail is the length of the tail. -/ -theorem length_zip_with_self_tail_eq_length_sub_one +theorem length_zipWith_self_tail_eq_length_sub_one : length (zipWith f (a :: as) as) = length as := by rw [length_zipWith] simp only [length_cons, ge_iff_le, min_eq_right_iff] @@ -132,22 +173,42 @@ theorem length_zip_with_self_tail_eq_length_sub_one The result of a `zipWith` is nonempty if and only if both arguments are nonempty. -/ -theorem zip_with_nonempty_iff_args_nonempty +theorem zipWith_nonempty_iff_args_nonempty : zipWith f as bs ≠ [] ↔ as ≠ [] ∧ bs ≠ [] := by apply Iff.intro · intro h - rw [self_nonempty_imp_exists_mem] at h + rw [self_neq_nil_imp_exists_mem] at h have ⟨z, ⟨zs, hzs⟩⟩ := h refine ⟨?_, ?_⟩ <;> · by_contra nh rw [nh] at hzs simp at hzs · intro ⟨ha, hb⟩ - have ⟨a', ⟨as', has⟩⟩ := self_nonempty_imp_exists_mem.mp ha - have ⟨b', ⟨bs', hbs⟩⟩ := self_nonempty_imp_exists_mem.mp hb + have ⟨a', ⟨as', has⟩⟩ := self_neq_nil_imp_exists_mem.mp ha + have ⟨b', ⟨bs', hbs⟩⟩ := self_neq_nil_imp_exists_mem.mp hb rw [has, hbs] simp +/-- +An index less than the length of a `zip` is less than the length of the left +operand. +-/ +theorem fin_zipWith_imp_val_lt_length_left {i : Fin (zipWith f xs ys).length} + : ↑i < length xs := by + have hi := i.2 + simp only [length_zipWith, ge_iff_le, lt_min_iff] at hi + exact hi.left + +/-- +An index less than the length of a `zip` is less than the length of the left +operand. +-/ +theorem fin_zipWith_imp_val_lt_length_right {i : Fin (zipWith f xs ys).length} + : ↑i < length ys := by + have hi := i.2 + simp only [length_zipWith, ge_iff_le, lt_min_iff] at hi + exact hi.right + -- ======================================== -- Pairwise -- ======================================== @@ -180,13 +241,11 @@ theorem len_pairwise_len_cons_sub_one {xs : List α} (h : xs.length > 0) unfold pairwise tail? cases xs with | nil => - have h' := length_gt_zero_imp_not_nil h - simp at h' + have := neq_nil_iff_length_gt_zero.mpr h + simp at this | cons a bs => - suffices length (zipWith f (a :: bs) bs) = length bs by - rw [this] - simp - rw [length_zip_with_self_tail_eq_length_sub_one] + rw [length_zipWith_self_tail_eq_length_sub_one] + conv => lhs; unfold length /-- If the `pairwise` list isn't empty, then the original list must have at least @@ -203,74 +262,38 @@ theorem mem_pairwise_imp_length_self_ge_2 {xs : List α} (h : xs.pairwise f ≠ | nil => rw [hx'] at h; simp at h | cons a' bs' => unfold length length; rw [add_assoc]; norm_num -private lemma fin_zip_with_imp_val_lt_length_left {i : Fin (zipWith f xs ys).length} - : i.1 < length xs := by - have hi := i.2 - simp only [length_zipWith, ge_iff_le, lt_min_iff] at hi - exact hi.left - /-- If `x` is a member of the pairwise'd list, there must exist two (adjacent) elements of the list, say `x₁` and `x₂`, such that `x = f x₁ x₂`. -/ -theorem mem_pairwise_imp_exists {xs : List α} (h : x ∈ xs.pairwise f) - : ∃ x₁ x₂, x₁ ∈ xs ∧ x₂ ∈ xs ∧ x = f x₁ x₂ := by +theorem mem_pairwise_imp_exists_adjacent {xs : List α} (h : x ∈ xs.pairwise f) + : ∃ i : Fin (xs.length - 1), ∃ x₁ x₂, + x₁ = get xs ⟨i.1, Nat.lt_of_lt_pred i.2⟩ ∧ + x₂ = get xs ⟨i.1 + 1, lt_tsub_iff_right.mp i.2⟩ ∧ + x = f x₁ x₂ := by unfold pairwise at h - cases hys : tail? xs with - | none => rw [hys] at h; cases h + cases hs : tail? xs with + | none => rw [hs] at h; cases h | some ys => - rw [hys] at h + rw [hs] at h simp only at h - - -- Since our `tail?` result isn't `none`, we should be able to decompose - -- `xs` into concatenation operands. - have ⟨r, hrs⟩ : ∃ r, xs = r :: ys := by - unfold tail? at hys - cases xs with - | nil => simp at hys - | cons r rs => exact ⟨r, by simp at hys; rw [hys]⟩ - - -- Maintain a collection of relations related to `i` and the length of `xs`. - -- Because of the proof-carrying `Fin` index, we find ourselves needing to - -- cast these values around periodically. + -- Find index `i` that corresponds to the index `x₁`. We decompose this + -- `Fin` type into `j` and `hj` to make rewriting easier. + have ⟨_, hy⟩ := some_tail?_imp_cons hs have ⟨i, hx⟩ := mem_iff_exists_get.mp h - have succ_i_lt_length_xs : ↑i + 1 < length xs := by - have hi := add_lt_add_right i.2 1 - conv at hi => rhs; rw [hrs, length_zip_with_self_tail_eq_length_sub_one] - conv => rhs; rw [congrArg length hrs]; unfold length - exact hi - have succ_i_lt_length_cons_r_ys : ↑i + 1 < length (r :: ys) := by - have hi := i.2 - conv at hi => rhs; rw [hrs, length_zip_with_self_tail_eq_length_sub_one] - exact add_lt_add_right hi 1 - have i_lt_length_ys : ↑i < length ys := by - unfold length at succ_i_lt_length_cons_r_ys - exact Nat.lt_of_succ_lt_succ succ_i_lt_length_cons_r_ys - - -- Choose the indices `x₁` and `x₂` that correspond to our `x` member. We - -- massage these values into the correct shape and then prove `x = f x₁ x₂`. - let x₁ := xs.get ⟨i, fin_zip_with_imp_val_lt_length_left⟩ - let x₂ := xs.get ⟨i + 1, succ_i_lt_length_xs⟩ - - have hx₁ : x₁ = xs.get ⟨i, fin_zip_with_imp_val_lt_length_left⟩ := rfl - have hx₂ : x₂ = get (r :: ys) { val := ↑i + 1, isLt := succ_i_lt_length_cons_r_ys } := by - rw [show x₂ = xs.get _ by rfl] - congr - exact Eq.recOn - (motive := fun x h => HEq - succ_i_lt_length_xs - (cast (show (↑i + 1 < length xs) = (↑i + 1 < length x) by rw [← h]) - succ_i_lt_length_xs)) - (show xs = r :: ys from hrs) - HEq.rfl - - refine ⟨x₁, ⟨x₂, ⟨get_mem_self, ⟨get_mem_self, ?_⟩⟩⟩⟩ - have hx₂_offset_idx - : get (r :: ys) { val := ↑i + 1, isLt := succ_i_lt_length_cons_r_ys} - = get ys { val := ↑i, isLt := i_lt_length_ys } := by - conv => lhs; unfold get; simp - rw [hx₂_offset_idx] at hx₂ - rw [get_zipWith, ← hx₁, ← hx₂] at hx - exact Eq.symm hx + have ⟨j, hj⟩ := i + rw [ + hy, + length_zipWith_self_tail_eq_length_sub_one, + show length ys = length xs - 1 by rw [hy]; simp + ] at hj + refine + ⟨⟨j, hj⟩, + ⟨get xs ⟨j, Nat.lt_of_lt_pred hj⟩, + ⟨get xs ⟨j + 1, lt_tsub_iff_right.mp hj⟩, + ⟨rfl, ⟨rfl, ?_⟩⟩⟩⟩⟩ + rw [← hx, get_zipWith] + subst hy + simp only [length_cons, get, Nat.add_eq, add_zero] end List diff --git a/OneVariableCalculus/Real/Function/Step.lean b/OneVariableCalculus/Real/Function/Step.lean index fa0c768..d11e031 100644 --- a/OneVariableCalculus/Real/Function/Step.lean +++ b/OneVariableCalculus/Real/Function/Step.lean @@ -11,14 +11,25 @@ Any member of a subinterval of a partition `P` must also be a member of `P`. lemma mem_open_subinterval_imp_mem_partition {p : Partition} (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => i(x₁, x₂))) (hy : y ∈ I) : y ∈ p := by - -- By definition, a partition must always have at least two points in the - -- interval. We can disregard the empty case. cases h : p.xs with - | nil => rw [h] at hI; cases hI + | nil => + -- By definition, a partition must always have at least two points in the + -- interval. Discharge the empty case. + rw [h] at hI + cases hI | cons x ys => - have ⟨x₁, ⟨x₂, ⟨hx₁, ⟨hx₂, hI'⟩⟩⟩⟩ := List.mem_pairwise_imp_exists hI + have ⟨i, x₁, ⟨x₂, ⟨hx₁, ⟨hx₂, hI'⟩⟩⟩⟩ := + List.mem_pairwise_imp_exists_adjacent hI + have hx₁ : x₁ ∈ p.xs := by + rw [hx₁] + let j : Fin (List.length p.xs) := ⟨i.1, Nat.lt_of_lt_pred i.2⟩ + exact List.mem_iff_exists_get.mpr ⟨j, rfl⟩ + have hx₂ : x₂ ∈ p.xs := by + rw [hx₂] + let j : Fin (List.length p.xs) := ⟨i.1 + 1, lt_tsub_iff_right.mp i.2⟩ + exact List.mem_iff_exists_get.mpr ⟨j, rfl⟩ rw [hI'] at hy - refine ⟨?_, ?_⟩ + apply And.intro · calc p.left _ ≤ x₁ := (subdivision_point_mem_partition hx₁).left _ ≤ y := le_of_lt hy.left diff --git a/OneVariableCalculus/Real/Set/Partition.lean b/OneVariableCalculus/Real/Set/Partition.lean index 56e4ca4..faaccf4 100644 --- a/OneVariableCalculus/Real/Set/Partition.lean +++ b/OneVariableCalculus/Real/Set/Partition.lean @@ -1,8 +1,12 @@ +import Mathlib.Data.List.Sort + import Bookshelf.List.Basic import Bookshelf.Real.Set.Interval namespace Real +open List + /-- A `Partition` is some finite subset of `[a, b]` containing points `a` and `b`. @@ -11,27 +15,36 @@ use of a `List` ensures finite-ness. -/ structure Partition where xs : List ℝ + sorted : Sorted LT.lt xs has_min_length : xs.length ≥ 2 - sorted : ∀ x ∈ xs.pairwise (fun x₁ x₂ => x₁ < x₂), x -namespace Partition - -lemma length_partition_gt_zero (p : Partition) : p.xs.length > 0 := +/-- +The length of any list associated with a `Partition` is `> 0`. +-/ +private lemma length_gt_zero (p : Partition) : p.xs.length > 0 := calc p.xs.length _ ≥ 2 := p.has_min_length _ > 0 := by simp +/-- +The length of any list associated with a `Partition` is `≠ 0`. +-/ +instance (p : Partition) : NeZero (length p.xs) where + out := LT.lt.ne' (length_gt_zero p) + +namespace Partition + /-- The left-most subdivision point of the `Partition`. -/ def left (p : Partition) : ℝ := - p.xs.head (List.length_gt_zero_imp_not_nil (length_partition_gt_zero p)) + p.xs.head (neq_nil_iff_length_gt_zero.mpr (length_gt_zero p)) /-- The right-most subdivision point of the `Partition`. -/ def right (p : Partition) : ℝ := - p.xs.getLast (List.length_gt_zero_imp_not_nil (length_partition_gt_zero p)) + p.xs.getLast (neq_nil_iff_length_gt_zero.mpr (length_gt_zero p)) /-- Define `∈` syntax for a `Partition`. We say a real is a member of a partition @@ -45,19 +58,34 @@ Every subdivision point is `≥` the left-most point of the partition. -/ theorem subdivision_point_geq_left {p : Partition} (h : x ∈ p.xs) : p.left ≤ x := by - suffices ∀ i : Fin p.xs.length, p.left ≤ List.get p.xs i by - rw [List.mem_iff_exists_get] at h - have ⟨i, hi⟩ := h - rw [← hi] - exact this i - intro ⟨i, hi⟩ - sorry + unfold left + rw [head_eq_get_zero (exists_mem_iff_neq_nil.mp ⟨x, h⟩)] + have ⟨i, hi⟩ := mem_iff_exists_get.mp h + conv => rhs; rw [← hi] + by_cases hz : i = (0 : Fin (length p.xs)) + · rw [hz] + simp + · refine le_of_lt (Sorted.rel_get_of_lt p.sorted ?_) + rwa [← ne_eq, ← Fin.pos_iff_ne_zero i] at hz /-- Every subdivision point is `≤` the right-most point of the partition. -/ theorem subdivision_point_leq_right {p : Partition} (h : x ∈ p.xs) - : x ≤ p.right := sorry + : x ≤ p.right := by + unfold right + have hx := exists_mem_iff_neq_nil.mp ⟨x, h⟩ + rw [getLast_eq_get_length_sub_one hx] + have ⟨i, hi⟩ := mem_iff_exists_get.mp h + conv => lhs; rw [← hi] + have ⟨_, ⟨_, hs⟩⟩ := self_neq_nil_imp_exists_mem.mp hx + by_cases hz : i = ⟨p.xs.length - 1, by rw [hs]; simp⟩ + · rw [hz] + simp + · refine le_of_lt (Sorted.rel_get_of_lt p.sorted ?_) + rw [← ne_eq, Fin.ne_iff_vne] at hz + rw [Fin.lt_iff_val_lt_val] + exact lt_of_le_of_ne (le_tsub_of_add_le_right i.2) hz /-- Every subdivision point of a `Partition` is itself a member of the `Partition`. diff --git a/TheoremProvingInLean/Avigad/Chapter3.lean b/TheoremProvingInLean/Avigad/Chapter3.lean index 51856c6..98c325c 100644 --- a/TheoremProvingInLean/Avigad/Chapter3.lean +++ b/TheoremProvingInLean/Avigad/Chapter3.lean @@ -7,8 +7,7 @@ Propositions and Proofs -- ======================================== -- Exercise 1 -- --- Prove the following identities, replacing the "sorry" placeholders with --- actual proofs. +-- Prove the following identities. -- ======================================== namespace ex1 @@ -108,8 +107,7 @@ end ex1 -- ======================================== -- Exercise 2 -- --- Prove the following identities, replacing the “sorry” placeholders with --- actual proofs. These require classical reasoning. +-- Prove the following identities. These require classical reasoning. -- ======================================== namespace ex2