long lines

leanprover-community · Nov 20, 2024 · 9b9f4d0 · 9b9f4d0
1 parent 58b1558
commit 9b9f4d0
Show file tree

Hide file tree

Showing 2 changed files with 84 additions and 76 deletions.
diff --git a/Batteries/Data/Range/Lemmas.lean b/Batteries/Data/Range/Lemmas.lean
@@ -48,55 +48,59 @@ theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r
 -- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
 -- and am hoping it is not necessary to get Mathlib working again
 
--- theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
---     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
---     forIn' r init f =
---     forIn
---       ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
---       init (fun ⟨a, h⟩ => f a h) := by
---   let ⟨start, stop, step⟩ := r
---   let L := List.range' start (numElems ⟨start, stop, step⟩) step
---   let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
---   suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
---   intro H; dsimp only [forIn', Range.forIn']
---   if h : start < stop then
---     simp [numElems, Nat.not_le.2 h, L]; split
---     · subst step
---       suffices ∀ n H init,
---           forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
---           forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
---       intro n; induction n with (intro H init; unfold forIn'.loop; simp [*])
---       | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
---     · next step0 =>
---       have hstep := Nat.pos_of_ne_zero step0
---       suffices ∀ fuel l i hle H, l ≤ fuel →
---           (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
---           forIn'.loop start stop step f fuel i hle init =
---           forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
---         refine this _ _ _ _ _
---           ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
---           (fun _ => (numElems_le_iff hstep).symm) _
---         conv => lhs; rw [← Nat.one_mul stop]
---         exact Nat.mul_le_mul_right stop hstep
---       intro fuel; induction fuel with intro l i hle H h1 h2 init
---       | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
---       | succ fuel ih =>
---         cases l with
---         | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
---         | succ l =>
---           have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
---             (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
---               rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
---           have := h2 0; simp at this
---           rw [forIn'.loop]; simp [this, ih]; rfl
---   else
---     simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
---     cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
+/-
+
+theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
+    (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
+    forIn' r init f =
+    forIn
+      ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r)
+      init (fun ⟨a, h⟩ => f a h) := by
+  let ⟨start, stop, step⟩ := r
+  let L := List.range' start (numElems ⟨start, stop, step⟩) step
+  let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h
+  suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _
+  intro H; dsimp only [forIn', Range.forIn']
+  if h : start < stop then
+    simp [numElems, Nat.not_le.2 h, L]; split
+    · subst step
+      suffices ∀ n H init,
+          forIn'.loop start stop 0 f n start (Nat.le_refl _) init =
+          forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ ..
+      intro n; induction n with (intro H init; unfold forIn'.loop; simp [*])
+      | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl
+    · next step0 =>
+      have hstep := Nat.pos_of_ne_zero step0
+      suffices ∀ fuel l i hle H, l ≤ fuel →
+          (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init,
+          forIn'.loop start stop step f fuel i hle init =
+          forIn ((List.range' i l step).pmap Subtype.mk H) init f' by
+        refine this _ _ _ _ _
+          ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..)))
+          (fun _ => (numElems_le_iff hstep).symm) _
+        conv => lhs; rw [← Nat.one_mul stop]
+        exact Nat.mul_le_mul_right stop hstep
+      intro fuel; induction fuel with intro l i hle H h1 h2 init
+      | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
+      | succ fuel ih =>
+        cases l with
+        | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
+        | succ l =>
+          have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..))
+            (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by
+              rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff]
+          have := h2 0; simp at this
+          rw [forIn'.loop]; simp [this, ih]; rfl
+  else
+    simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L]
+    cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h]
 
--- theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
---     (init : β) (f : Nat → β → m (ForInStep β)) :
---     forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
---   refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
---   · simp [forIn, forIn']
---   · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
---     intro L; induction L generalizing init <;> intro H <;> simp [*]
+theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
+    (init : β) (f : Nat → β → m (ForInStep β)) :
+    forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by
+  refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_
+  · simp [forIn, forIn']
+  · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
+    intro L; induction L generalizing init <;> intro H <;> simp [*]
+
+-/
diff --git a/Batteries/Data/Vector/Basic.lean b/Batteries/Data/Vector/Basic.lean
@@ -266,31 +266,35 @@ proof_wanted instLawfulBEq (α n) [BEq α] [LawfulBEq α] : LawfulBEq (Vector α
 -- FIXME: temporarily commented out; I've broken this on nightly-2024-11-20,
 -- and am hoping it is not necessary to get Mathlib working again
 
--- /-- Delete an element of a vector using a `Fin` index. -/
--- @[inline] def feraseIdx (v : Vector α n) (i : Fin n) : Vector α (n-1) :=
---   ⟨v.toArray.feraseIdx (Fin.cast v.size_toArray.symm i), by simp [Array.size_feraseIdx]⟩
-
--- /-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
--- @[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
---   if _ : i < n then
---     ⟨v.toArray.eraseIdx i, by simp [*]⟩
---   else
---     have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
---     panic! "index out of bounds"
-
--- /-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
--- @[inline] def tail (v : Vector α n) : Vector α (n-1) :=
---   if _ : 0 < n then
---     ⟨v.toArray.eraseIdx 0, by simp [*]⟩
---   else
---     v.cast (by omega)
-
--- /--
--- Delete an element of a vector using a `Nat` index. By default, the `get_elem_tactic` is used to
--- synthesise a proof that the index is within bounds.
--- -/
--- @[inline] def eraseIdxN (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
---   Vector α (n - 1) := ⟨v.toArray.eraseIdxN i (by simp [*]), by simp⟩
+/-
+
+/-- Delete an element of a vector using a `Fin` index. -/
+@[inline] def feraseIdx (v : Vector α n) (i : Fin n) : Vector α (n-1) :=
+  ⟨v.toArray.feraseIdx (Fin.cast v.size_toArray.symm i), by simp [Array.size_feraseIdx]⟩
+
+/-- Delete an element of a vector using a `Nat` index. Panics if the index is out of bounds. -/
+@[inline] def eraseIdx! (v : Vector α n) (i : Nat) : Vector α (n-1) :=
+  if _ : i < n then
+    ⟨v.toArray.eraseIdx i, by simp [*]⟩
+  else
+    have : Inhabited (Vector α (n-1)) := ⟨v.pop⟩
+    panic! "index out of bounds"
+
+/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
+@[inline] def tail (v : Vector α n) : Vector α (n-1) :=
+  if _ : 0 < n then
+    ⟨v.toArray.eraseIdx 0, by simp [*]⟩
+  else
+    v.cast (by omega)
+
+/--
+Delete an element of a vector using a `Nat` index. By default, the `get_elem_tactic` is used to
+synthesise a proof that the index is within bounds.
+-/
+@[inline] def eraseIdxN (v : Vector α n) (i : Nat) (h : i < n := by get_elem_tactic) :
+  Vector α (n - 1) := ⟨v.toArray.eraseIdxN i (by simp [*]), by simp⟩
+
+-/
 
 /--
 Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the