feat: more Nat range lemmas (#11321)

This PR provides specialized lemmas about `Nat` ranges, including `simp`
annotations and induction principles for proving properties for all
ranges.

Author: datokrat

src/Init/Data/Array/Lex/Lemmas.lean

@@ -73,19 +73,11 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
        (lt a b || a == b && xs.lex ys lt) := by
   simp only [lex, size_append, List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add,
     Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList]
-  conv =>
-    lhs; congr; congr
-    rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if_roo rfl (fun _ _ _ => rfl)]
-    simp only [bind_pure_comp, map_pure]
-    rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [Std.toList_roo_eq_toList_rco_of_isSome_succ? (lo := 0) (h := rfl),
-    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_rco_succ_succ,
-    Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
-    Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
-  cases lt a b
-  · rw [bne]
-    cases a == b <;> simp
-  · simp
+  rw [cons_lex_cons.forIn'_congr_aux (Nat.toList_rco_eq_cons (by omega)) rfl (fun _ _ _ => rfl)]
+  simp only [bind_pure_comp, map_pure, Nat.toList_rco_succ_succ, Nat.add_comm 1]
+  cases h : lt a b
+  · cases h' : a == b <;> simp [bne, *]
+  · simp [*]
 
 @[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by

src/Init/Data/List/Range.lean

@@ -37,7 +37,7 @@ open Nat
   rw [← length_eq_zero_iff, length_range']
 
 theorem range'_ne_nil_iff (s : Nat) {n step : Nat} : range' s n step ≠ [] ↔ n ≠ 0 := by
-  cases n <;> simp
+  simp
 
 theorem range'_eq_cons_iff : range' s n step = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + step) (n - 1) step := by
   induction n generalizing s with

src/Init/Data/Range/Polymorphic/Lemmas.lean

@@ -467,6 +467,23 @@ public theorem Rxo.Iterator.toArray_eq_match [LT α] [DecidableLT α]
   · rfl
   · split <;> simp
 
+public theorem Rxc.Iterator.toList_eq_toList_rxoIterator [LE α] [DecidableLE α] [LT α] [DecidableLT α]
+    [UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
+    [InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] {it : Iter (α := Rxc.Iterator α) α}:
+    it.toList = (⟨⟨it.internalState.next, succ it.internalState.upperBound⟩⟩ : Iter (α := Rxo.Iterator α) α).toList := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [Rxc.Iterator.toList_eq_match, Rxo.Iterator.toList_eq_match]
+  split
+  · simp [*]
+  · simp only [UpwardEnumerable.le_iff, UpwardEnumerable.lt_iff, *]
+    split <;> rename_i h
+    · rw [ihy]; rotate_left
+      · simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          Iterator.Monadic.step, Iter.toIterM, *]; rfl
+      · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h
+    · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h
+
 public theorem Rxi.Iterator.toList_eq_match
     [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     {it : Iter (α := Rxi.Iterator α) α} :
@@ -561,22 +578,6 @@ namespace Rcc
 
 variable {r : Rcc α}
 
-public theorem toList_eq_if_roo [UpwardEnumerable α] [LE α] [DecidableLE α]
-    [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerableLE α] :
-    r.toList = if r.lower ≤ r.upper then r.lower :: (r.lower<...=r.upper).toList else [] := by
-  rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match]; rfl
-
-@[deprecated toList_eq_if_roo (since := "2025-10-29")]
-def toList_eq_if_Roo := @toList_eq_if_roo
-
-public theorem toArray_eq_if_roo [UpwardEnumerable α] [LE α] [DecidableLE α]
-    [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerableLE α] :
-    r.toArray = if r.lower ≤ r.upper then #[r.lower] ++ (r.lower<...=r.upper).toArray else #[] := by
-  rw [Internal.toArray_eq_toArray_iter, Rxc.Iterator.toArray_eq_match]; rfl
-
-@[deprecated toArray_eq_if_roo (since := "2025-10-29")]
-def toArray_eq_if_Roo := @toArray_eq_if_roo
-
 public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
     r.toList = if r.lower ≤ r.upper then
@@ -585,6 +586,16 @@ public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
         [] := by
   rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match]; rfl
 
+@[simp]
+public theorem toList_eq_toList_rco [LE α] [DecidableLE α] [LT α] [DecidableLT α]
+    [UpwardEnumerable α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
+    [Rxc.IsAlwaysFinite α] [Rxo.IsAlwaysFinite α]
+    [InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] :
+    r.toList = (r.lower...(succ r.upper)).toList := by
+  simp [Internal.toList_eq_toList_iter, Rco.Internal.toList_eq_toList_iter,
+    Internal.iter, Rco.Internal.iter, Rxc.Iterator.toList_eq_toList_rxoIterator]
+
 @[deprecated toList_eq_if_roc (since := "2025-10-29")]
 def toList_eq_match := @toList_eq_if_roc
 
@@ -816,6 +827,23 @@ public theorem toArray_eq_if_roo [UpwardEnumerable α] [LT α] [DecidableLT α]
         #[] := by
   rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl
 
+public theorem toList_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
+    [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] :
+    r.toList = if r.lower < r.upper then
+        match UpwardEnumerable.succ? r.lower with
+        | none => [r.lower]
+        | some next => r.lower :: (next...r.upper).toList
+      else
+        [] := by
+  rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match]
+  simp only [Internal.iter]
+  split
+  · split
+    · simp [Rxo.Iterator.toList_eq_match, *]
+    · simp only [*]
+      rfl
+  · rfl
+
 public theorem toArray_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] :
     r.toArray = if r.lower < r.upper then
@@ -1272,6 +1300,16 @@ public theorem toArray_eq_match_rcc [LE α] [DecidableLE α] [UpwardEnumerable 
   simp only [← Internal.toList_eq_toList_iter, toList_eq_match_rcc]
   split <;> simp
 
+@[simp]
+public theorem toList_eq_toList_roo [LE α] [DecidableLE α] [LT α] [DecidableLT α]
+    [UpwardEnumerable α] [LawfulUpwardEnumerable α]
+    [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
+    [Rxc.IsAlwaysFinite α] [Rxo.IsAlwaysFinite α]
+    [InfinitelyUpwardEnumerable α] [LinearlyUpwardEnumerable α] :
+    r.toList = (r.lower<...(succ r.upper)).toList := by
+  simp [Internal.toList_eq_toList_iter, Roo.Internal.toList_eq_toList_iter,
+    Internal.iter, Roo.Internal.iter, Rxc.Iterator.toList_eq_toList_rxoIterator]
+
 @[simp]
 public theorem toArray_toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxc.IsAlwaysFinite α] :
@@ -2856,7 +2894,7 @@ public theorem length_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
   · simpa [toList_eq_nil_iff, size_eq_if_roc] using h
   · rename_i n ih
     rw [size_eq_if_rcc] at h
-    simp only [toList_eq_if_roo, ← h]
+    simp only [toList_eq_if_roc, ← h]
     simp only [Roc.toList_eq_match_rcc]
     split
     · split