wip: move consumer lemmas to Init

Author: datokrat

src/Init/Data/Iterators.lean

@@ -9,3 +9,4 @@ prelude
 import Init.Data.Iterators.Basic
 import Init.Data.Iterators.PostconditionMonad
 import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.Lemmas

src/Init/Data/Iterators/Lemmas.lean

@@ -0,0 +1,4 @@
+module
+
+prelude
+import Init.Data.Iterators.Lemmas.Consumers

src/Init/Data/Iterators/Lemmas/Consumers.lean

@@ -0,0 +1,6 @@
+module
+
+prelude
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Loop

…/Iterators/Lemmas/Consumers/Collect.lean …/Iterators/Lemmas/Consumers/Collect.leansrc/Std/Data/Iterators/Lemmas/Consumers/Collect.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.Iterators.Consumers.Access
 import Init.Data.Iterators.Consumers.Collect
 import Std.Data.Iterators.Lemmas.Basic
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 
 namespace Std.Iterators
 

…ata/Iterators/Lemmas/Consumers/Loop.lean …ata/Iterators/Lemmas/Consumers/Loop.leansrc/Std/Data/Iterators/Lemmas/Consumers/Loop.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean

@@ -6,8 +6,8 @@ Authors: Paul Reichert
 prelude
 import Init.Data.List.Control
 import Std.Data.Iterators.Lemmas.Basic
-import Std.Data.Iterators.Lemmas.Consumers.Collect
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+import Init.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 import Init.Data.Iterators.Consumers.Collect
 import Init.Data.Iterators.Consumers.Loop
 

…/Iterators/Lemmas/Consumers/Monadic.lean …/Iterators/Lemmas/Consumers/Monadic.leansrc/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean

@@ -4,5 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop

…rs/Lemmas/Consumers/Monadic/Collect.lean …rs/Lemmas/Consumers/Monadic/Collect.leansrc/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean

@@ -8,7 +8,7 @@ import Init.Control.Lawful.Basic
 import Init.Data.Iterators.Consumers.Monadic.Collect
 import Init.Data.Iterators.Consumers.Monadic.Loop
 import Std.Data.Iterators.Lemmas.Monadic.Basic
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 import Std.Data.Iterators.Lemmas.Equivalence.StepCongr
 
 namespace Std.Iterators

…ators/Lemmas/Consumers/Monadic/Loop.lean …ators/Lemmas/Consumers/Monadic/Loop.leansrc/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean renamed to src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean

@@ -8,6 +8,7 @@ module
 prelude
 import Init.Data.List.Pairwise
 import Init.Data.List.Zip
+import Init.Data.Range.Classes
 
 /-!
 # Lemmas about `List.range` and `List.zipIdx`

src/Init/Data/List/Range.lean

@@ -0,0 +1,49 @@
+module
+
+prelude
+import Init.Core
+import Init.Data.Nat.Basic
+import Init.Data.Option.Basic
+
+class Succ? (α : Type u) where
+  succ? : α → Option α
+  succAtIdx? (n : Nat) (a : α) : Option α := Nat.repeat (· >>= succ?) n (some a)
+
+class LawfulSucc? (α : Type u) [Succ? α] where
+  succAtIdx?_zero {a : α} : Succ?.succAtIdx? 0 a = some a
+  succAtIdx?_succ {a : α} : Succ?.succAtIdx? (n + 1) a = Succ?.succAtIdx? n a >>= Succ?.succ?
+
+class LawfulLESucc? (α : Type u) [LE α] [Succ? α] where
+  le_rfl : {a : α} → a ≤ a
+  le_succ? : {a b : α} → Succ?.succ? a = some b → a ≤ b
+  le_succ?_of_le : {a b c : α} → a ≤ b → (h : Succ?.succ? b = some c) → a ≤ c
+  le_succAtIdx?_of_le : {a b c : α} → {n : Nat} → a ≤ b → (h : Succ?.succAtIdx? n b = some c) → a ≤ c
+
+class LawfulLTSucc? [LT α] [Succ? α] where
+  lt_succ? : {a b : α} → (h : Succ?.succ? a = some b) → a < b
+  lt_succ?_of_lt : {a b c : α} → a < b → (h : Succ?.succ? b = some c) → a < c
+
+class HasDownwardUnboundedRanges (α : Type u) where
+  min : α
+
+instance : Succ? Nat where
+  succ? n := some (n + 1)
+  succAtIdx? k n := some (n + k)
+
+instance : LawfulSucc? Nat where
+  succAtIdx?_zero := by simp [Succ?.succAtIdx?]
+  succAtIdx?_succ := by simp [Succ?.succAtIdx?, Succ?.succ?, Bind.bind, Nat.add_assoc]
+
+instance : LawfulLESucc? Nat where
+  le_rfl := Nat.le_refl _
+  le_succ? := sorry
+  le_succ?_of_le hle h := by
+    simp only [Succ?.succ?, Option.some.injEq] at h
+    rw [← h]
+    exact Nat.le_trans hle (Nat.le_succ _)
+  le_succAtIdx?_of_le {a b c n} hle h := by
+    simp only [Succ?.succAtIdx?, Option.some.injEq] at h
+    rw [← h]
+    exact Nat.le_trans hle (Nat.le_add_right _ _)
+
+#print instLawfulLESucc?Nat._proof_2