Finish proving partition proofs.

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 ⟨a', ⟨as', has⟩⟩ := self_neq_nil_imp_exists_mem.mp ha
-    have ⟨b', ⟨bs', hbs⟩⟩ := self_nonempty_imp_exists_mem.mp hb
+    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
+    have := neq_nil_iff_length_gt_zero.mpr h
-    simp at h'
+    simp at this
   | cons a bs =>
-    suffices length (zipWith f (a :: bs) bs) = length bs by
+    rw [length_zipWith_self_tail_eq_length_sub_one]
-      rw [this]
+    conv => lhs; unfold length
-      simp
-    rw [length_zip_with_self_tail_eq_length_sub_one]
 
 /--
 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)
+theorem mem_pairwise_imp_exists_adjacent {xs : List α} (h : x ∈ xs.pairwise f)
-  : ∃ x₁ x₂, x₁ ∈ xs ∧ x₂ ∈ xs ∧ x = f x₁ x₂ := by
+  : ∃ 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
+  cases hs : tail? xs with
-  | none => rw [hys] at h; cases h
+  | none => rw [hs] at h; cases h
   | some ys =>
-    rw [hys] at h
+    rw [hs] at h
     simp only at h
-
+    -- Find index `i` that corresponds to the index `x₁`. We decompose this
-    -- Since our `tail?` result isn't `none`, we should be able to decompose
+    -- `Fin` type into `j` and `hj` to make rewriting easier.
-    -- `xs` into concatenation operands.
+    have ⟨_, hy⟩ := some_tail?_imp_cons hs    
-    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.
     have ⟨i, hx⟩ := mem_iff_exists_get.mp h
-    have succ_i_lt_length_xs : ↑i + 1 < length xs := by
+    have ⟨j, hj⟩ := i
-      have hi := add_lt_add_right i.2 1
+    rw [
-      conv at hi => rhs; rw [hrs, length_zip_with_self_tail_eq_length_sub_one]
+      hy,
-      conv => rhs; rw [congrArg length hrs]; unfold length
+      length_zipWith_self_tail_eq_length_sub_one,
-      exact hi
+      show length ys = length xs - 1 by rw [hy]; simp
-    have succ_i_lt_length_cons_r_ys : ↑i + 1 < length (r :: ys) := by
+    ] at hj
-      have hi := i.2
+    refine
-      conv at hi => rhs; rw [hrs, length_zip_with_self_tail_eq_length_sub_one]
+      ⟨⟨j, hj⟩,
-      exact add_lt_add_right hi 1
+        ⟨get xs ⟨j, Nat.lt_of_lt_pred hj⟩,
-    have i_lt_length_ys : ↑i < length ys := by
+          ⟨get xs ⟨j + 1, lt_tsub_iff_right.mp hj⟩,
-      unfold length at succ_i_lt_length_cons_r_ys
+            ⟨rfl, ⟨rfl, ?_⟩⟩⟩⟩⟩
-      exact Nat.lt_of_succ_lt_succ succ_i_lt_length_cons_r_ys
+    rw [← hx, get_zipWith]
-
+    subst hy
-    -- Choose the indices `x₁` and `x₂` that correspond to our `x` member. We
+    simp only [length_cons, get, Nat.add_eq, add_zero]
-    -- 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
 
 end List

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

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
+/--
-
+The length of any list associated with a `Partition` is `> 0`.
-lemma length_partition_gt_zero (p : Partition) : p.xs.length > 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
+  unfold left
-    rw [List.mem_iff_exists_get] at h
+  rw [head_eq_get_zero (exists_mem_iff_neq_nil.mp ⟨x, h⟩)]
-    have ⟨i, hi⟩ := h
+  have ⟨i, hi⟩ := mem_iff_exists_get.mp h
-    rw [← hi]
+  conv => rhs; rw [← hi]
-    exact this i
+  by_cases hz : i = (0 : Fin (length p.xs))
-  intro ⟨i, hi⟩
+  · rw [hz]
-  sorry
+    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`.

TheoremProvingInLean/Avigad/Chapter3.lean

@@ -7,8 +7,7 @@ Propositions and Proofs
 -- ========================================
 -- Exercise 1
 --
--- Prove the following identities, replacing the "sorry" placeholders with
+-- Prove the following identities.
--- actual proofs.
 -- ========================================
 
 namespace ex1
@@ -108,8 +107,7 @@ end ex1
 -- ========================================
 -- Exercise 2
 --
--- Prove the following identities, replacing the “sorry” placeholders with
+-- Prove the following identities. These require classical reasoning.
--- actual proofs. These require classical reasoning.
 -- ========================================
 
 namespace ex2