more lemmas

Author: datokrat

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

@@ -748,6 +748,20 @@ theorem Iter.findSomeM?_eq_match_step {α β : Type w} {γ : Type x} {m : Type x
   · simp [findSomeM?]
   · simp
 
+theorem Iter.findSomeM?_toList {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [IteratorCollect α Id Id]
+    [LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {f : β → m (Option γ)} :
+    it.toList.findSomeM? f = it.findSomeM? f := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [it.findSomeM?_eq_match_step, it.toList_eq_match_step]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only [List.findSomeM?_cons]
+    apply bind_congr; intro fx
+    split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
 theorem Iter.findSome?_eq_findSomeM? {α β : Type w} {γ : Type x}
     [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
     {it : Iter (α := α) β} {f : β → Option γ} :
@@ -761,7 +775,7 @@ theorem Iter.findSome?_eq_findSome?_toIterM {α β γ : Type w}
   (rfl)
 
 theorem Iter.findSome?_eq_match_step {α β : Type w} {γ : Type x}
-    [Iterator α Id β] [IteratorLoop α Id Id] [LawfulMonad Id] [Finite α Id]
+    [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
     [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} {f : β → Option γ} :
     it.findSome? f = (match it.step.val with
       | .yield it' out =>
@@ -777,6 +791,21 @@ theorem Iter.findSome?_eq_match_step {α β : Type w} {γ : Type x}
   · simp [findSome?_eq_findSomeM?]
   · simp
 
+theorem Iter.findSome?_toList {α β : Type w} {γ : Type x}
+    [Iterator α Id β] [IteratorLoop α Id Id] [IteratorCollect α Id Id]
+    [Finite α Id] [LawfulIteratorLoop α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {f : β → Option γ} :
+    it.toList.findSome? f = it.findSome? f := by
+  simp [findSome?_eq_findSomeM?, List.findSome?_eq_findSomeM?, findSomeM?_toList]
+
+theorem Iter.findSomeM?_pure {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [IteratorLoop α Id Id]
+    [LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {f : β → Option γ} :
+    it.findSomeM? (pure <| f ·) = pure (f := m) (it.findSome? f) := by
+  letI : IteratorCollect α Id Id := .defaultImplementation
+  simp [← findSomeM?_toList, ← findSome?_toList, List.findSomeM?_pure]
+
 theorem Iter.findM?_eq_findSomeM? {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
     {it : Iter (α := α) β} {f : β → m (ULift Bool)} :
@@ -800,6 +829,20 @@ theorem Iter.findM?_eq_match_step {α β : Type w} {m : Type w → Type w'} [Mon
   · simp [findM?_eq_findSomeM?]
   · simp
 
+theorem Iter.findM?_toList {α β : Type} {m : Type → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [IteratorCollect α Id Id]
+    [LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {f : β → m Bool} :
+    it.toList.findM? f = it.findM? (.up <$> f ·) := by
+  simp [findM?_eq_findSomeM?, List.findM?_eq_findSomeM?, findSomeM?_toList]
+
+theorem Iter.findM?_eq_findM?_toList {α β : Type} {m : Type → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [IteratorCollect α Id Id]
+    [LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {f : β → m (ULift Bool)} :
+    it.findM? f = it.toList.findM? (ULift.down <$> f ·) := by
+  simp [findM?_toList]
+
 theorem Iter.find?_eq_findM? {α β : Type w} [Iterator α Id β]
     [IteratorLoop α Id Id] [Finite α Id] {it : Iter (α := α) β} {f : β → Bool} :
     it.find? f = Id.run (it.findM? (pure <| .up <| f ·)) :=
@@ -830,4 +873,26 @@ theorem Iter.find?_eq_match_step {α β : Type w}
   · simp [find?_eq_findM?]
   · simp
 
+theorem Iter.find?_toList {α β : Type w}
+    [Iterator α Id β] [IteratorLoop α Id Id] [IteratorCollect α Id Id]
+    [Finite α Id] [LawfulIteratorLoop α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} {f : β → Bool} :
+    it.toList.find? f = it.find? f := by
+  simp [find?_eq_findSome?, List.find?_eq_findSome?_guard, findSome?_toList, Option.guard_def]
+
+theorem Iter.findM?_pure {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [IteratorLoop α Id Id]
+    [LawfulMonad m] [Finite α Id] [LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {f : β → ULift Bool} :
+    it.findM? (pure (f := m) <| f ·) = pure (f := m) (it.find? (ULift.down <| f ·)) := by
+  induction it using Iter.inductSteps with | step it ihy ihs
+  rw [findM?_eq_match_step, find?_eq_match_step]
+  cases it.step using PlausibleIterStep.casesOn
+  · simp only [pure_bind]
+    split
+    · simp
+    · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
 end Std.Iterators

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

@@ -554,6 +554,20 @@ theorem IterM.findSome?_eq_match_step {α β γ : Type w} {m : Type w → Type w
   apply bind_congr; intro step
   split <;> simp [findSome?_eq_findSomeM?]
 
+theorem IterM.findSomeM?_pure {α β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoop α m m]
+    [LawfulMonad m] [Finite α m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → Option γ} :
+    it.findSomeM? (pure <| f ·) = it.findSome? f := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [findSomeM?_eq_match_step, findSome?_eq_match_step]
+  apply bind_congr; intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp only [pure_bind]
+    split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
 theorem IterM.findM?_eq_findSomeM? {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m β] [IteratorLoop α m m] [Finite α m]
     {it : IterM (α := α) m β} {f : β → m (ULift Bool)} :
@@ -605,4 +619,20 @@ theorem IterM.find?_eq_match_step {α β : Type w} {m : Type w → Type w'} [Mon
   · simp [find?_eq_findM?]
   · simp
 
+theorem IterM.findM?_pure {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoop α m m]
+    [LawfulMonad m] [Finite α m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → ULift Bool} :
+    it.findM? (pure (f := m) <| f ·) = it.find? (ULift.down <| f ·) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [findM?_eq_match_step, find?_eq_match_step]
+  apply bind_congr; intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp only [pure_bind]
+    split
+    · simp
+    · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
 end Std.Iterators

src/Init/Data/List/Control.lean

@@ -405,6 +405,21 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
     | some b => pure (some b)
     | none   => findSomeM? f as
 
+@[simp, grind =]
+theorem findSomeM?_nil [Monad m] {α : Type w} {β : Type u}
+    {f : α → m (Option β)} :
+    ([] : List α).findSomeM? f = pure none :=
+  (rfl)
+
+@[grind =]
+theorem findSomeM?_cons [Monad m] {α : Type w} {β : Type u}
+    {f : α → m (Option β)} {a : α} {as : List α} :
+    (a::as).findSomeM? f = (do
+      match ← f a with
+      | some b => return some b
+      | none => as.findSomeM? f) :=
+  (rfl)
+
 @[simp]
 theorem findSomeM?_pure [Monad m] [LawfulMonad m] {f : α → Option β} {as : List α} :
     findSomeM? (m := m) (pure <| f ·) as = pure (as.findSome? f) := by
@@ -426,6 +441,10 @@ theorem findSomeM?_id (f : α → Id (Option β)) (as : List α) :
     findSomeM? (m := Id) f as = as.findSome? f :=
   findSomeM?_pure
 
+theorem findSome?_eq_findSomeM? {f : α → Option β} {as : List α} :
+    as.findSome? f = (as.findSomeM? (pure (f := Id) <| f ·)).run := by
+  simp
+
 theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} :
     as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none := by
   induction as with