import Do.Return

Iteration

open Lean

/- Disable the automatic monadic lifting feature described in the paper.
   We want to make it clear that we do not depend on it. -/
set_option autoLift false

syntax "for" ident "in" term "do'" stmt:1 : stmt
syntax "break " : stmt
syntax "continue " : stmt

syntax "break" : expander
syntax "continue" : expander
syntax "lift" : expander

macro_rules
  | `(stmt| expand! $_   in break) => `(stmt| break): MacroM Syntax
`(stmt| `(stmt| break): MacroM Syntax
break`(stmt| break): MacroM Syntax
)                                              -- subsumes (S7, R7, B2, L1)
  | `(stmt| expand! $_   in continue) => `(stmt| continue): MacroM Syntax
`(stmt| `(stmt| continue): MacroM Syntax
continue`(stmt| continue): MacroM Syntax
)                                        -- subsumes (S8, R8, L2)
  | `(stmt| expand! $exp: TSyntax `expander
exp in for $x: TSyntax `ident
x in $e: TSyntax `term
e do' $s: TSyntax `stmt
s) => `(stmt| for $x: TSyntax `ident
x in $e: TSyntax `term
e do' expand! $exp: TSyntax `expander
exp in $s: TSyntax `stmt
s)  -- subsumes (L8, R9)

macro_rules
  | `(d! for $x: TSyntax `ident
x in $e: TSyntax `term
e do' $s: TSyntax `stmt
s) => do  -- (D5), optimized like (1')
    let mut s: TSyntax `stmt
s := s: TSyntax `stmt
s
    let sb: TSyntax `stmt
sb ← expandStmt: TSyntax `stmt → MacroM (TSyntax `stmt)
expandStmt (← `(stmt| expand! break in $s)): TSyntax `stmt
(← `(stmt| (← `(stmt| expand! break in $s)): TSyntax `stmt
expand!(← `(stmt| expand! break in $s)): TSyntax `stmt
 (← `(stmt| expand! break in $s)): TSyntax `stmt
break(← `(stmt| expand! break in $s)): TSyntax `stmt
 (← `(stmt| expand! break in $s)): TSyntax `stmt
in(← `(stmt| expand! break in $s)): TSyntax `stmt
 $s: TSyntax `stmt
s(← `(stmt| expand! break in $s)): TSyntax `stmt
))
    let hasBreak: Prop
hasBreak := sb: TSyntax `stmt
sb.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw.count: Syntax → (Syntax → Bool) → Nat
count (· matches `(stmt| break)) < s: TSyntax `stmt
s.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw.count: Syntax → (Syntax → Bool) → Nat
count (· matches `(stmt| break))
    if hasBreak: Prop
hasBreak then
      s: TSyntax `stmt
s := sb: TSyntax `stmt
sb
    let sc: TSyntax `stmt
sc ← expandStmt: TSyntax `stmt → MacroM (TSyntax `stmt)
expandStmt (← `(stmt| expand! continue in $s)): TSyntax `stmt
(← `(stmt| (← `(stmt| expand! continue in $s)): TSyntax `stmt
expand!(← `(stmt| expand! continue in $s)): TSyntax `stmt
 (← `(stmt| expand! continue in $s)): TSyntax `stmt
continue(← `(stmt| expand! continue in $s)): TSyntax `stmt
 (← `(stmt| expand! continue in $s)): TSyntax `stmt
in(← `(stmt| expand! continue in $s)): TSyntax `stmt
 $s: TSyntax `stmt
s(← `(stmt| expand! continue in $s)): TSyntax `stmt
))
    let hasContinue: Prop
hasContinue := sc: TSyntax `stmt
sc.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw.count: Syntax → (Syntax → Bool) → Nat
count (· matches `(stmt| continue)) < s: TSyntax `stmt
s.raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw.count: Syntax → (Syntax → Bool) → Nat
count (· matches `(stmt| continue))
    if hasContinue: Prop
hasContinue then
      s: TSyntax `stmt
s := sc: TSyntax `stmt
sc
    let mut body: TSyntax `term
body ← `(d! $s: TSyntax `stmt
s)
    if hasContinue: Prop
hasContinue then
      body: TSyntax `term
body ← `(ExceptCpsT.runCatch $body: TSyntax `term
body)
    let mut loop: TSyntax `term
loop ← `(forM $e: TSyntax `term
e (fun $x: TSyntax `ident
x => $body: TSyntax `term
body))
    if hasBreak: Prop
hasBreak then
      loop: TSyntax `term
loop ← `(ExceptCpsT.runCatch $loop: TSyntax `term
loop)
    pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure loop: TSyntax `term
loop
  | `(d! break%$b: Syntax
b) =>
    throw: {ε : Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α
throw <| Macro.Exception.error: Syntax → String → Macro.Exception
Macro.Exception.error b: Syntax
b "unexpected 'break' outside loop": String
"unexpected 'break' outside loop"
  | `(d! continue%$c: Syntax
c) =>
    throw: {ε : Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α
throw <| Macro.Exception.error: Syntax → String → Macro.Exception
Macro.Exception.error c: Syntax
c "unexpected 'continue' outside loop": String
"unexpected 'continue' outside loop"

macro_rules
  | `(stmt| expand! break in break) => `(stmt| throw ()): MacroM Syntax
`(stmt| throw ())                                           -- (B1)
  | `(stmt| expand! break in $e: TSyntax `term
e:term) => `(stmt| ExceptCpsT.lift $e: TSyntax `term
e)                               -- (B3)
  | `(stmt| expand! break in for $x: TSyntax `ident
x in $e: TSyntax `term
e do' $s: TSyntax `stmt
s) => `(stmt| for $x: TSyntax `ident
x in $e: TSyntax `term
e do' expand! lift in $s: TSyntax `stmt
s)  -- (B8)
  | `(stmt| expand! continue in continue) => `(stmt| throw ()): MacroM Syntax
`(stmt| throw ())
  | `(stmt| expand! continue in $e: TSyntax `term
e:term) => `(stmt| ExceptCpsT.lift $e: TSyntax `term
e)
  | `(stmt| expand! continue in for $x: TSyntax `ident
x in $e: TSyntax `term
e do' $s: TSyntax `stmt
s) => `(stmt| for $x: TSyntax `ident
x in $e: TSyntax `term
e do' expand! lift in $s: TSyntax `stmt
s)

macro_rules
  | `(stmt| expand! lift in $e: TSyntax `term
e:term) => `(stmt| ExceptCpsT.lift $e: TSyntax `term
e)  -- (L3)

macro_rules
  | `(stmt| expand! mut $y: TSyntax `ident
y in for $x: TSyntax `ident
x in $e: TSyntax `term
e do' $s: TSyntax `stmt
s) => `(stmt| for $x: TSyntax `ident
x in $e: TSyntax `term
e do' { let $y: TSyntax `ident
y ← get; expand! mut $y: TSyntax `ident
y in $s: TSyntax `stmt
s })  -- (S9)

variable [Monad: (Type ?u.36846 → Type ?u.36845) → Type (max (?u.36846 + 1) ?u.36845)
Monad m: Type ?u.7311 → Type ?u.7310
m]
variable (ma: m α
ma ma': m α
ma' : m: Type ?u.7322 → Type ?u.7321
m α: Type
α)
variable (b: Bool
b : Bool: Type
Bool)
variable (xs: List α
xs : List: Type → Type
List α: Type
α) (act: α → m Unit
act : α: Type
α → m: Type → Type u_1
m Unit: Type
Unit)

attribute [local simp] map_eq_pure_bind: ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m] (f : α → β) (x : m α),
  f <$> x = do
    let a ← x
    pure (f a)
map_eq_pure_bind

example: ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] (xs : List α) (act : α → m Unit) [inst_1 : LawfulMonad m],
  (forM xs fun x => act x) = List.forM xs act
example [LawfulMonad: (m : Type → Type u_1) → [inst : Monad m] → Prop
LawfulMonad m: Type → Type u_1
m] :
    (do' for x: α
x in xs: List α
xs do' {
           act: α → m Unit
act x: α
x
         })
    =
    xs: List α
xs.forM: {m : Type → Type u_1} → [inst : Monad m] → {α : Type} → List α → (α → m PUnit) → m PUnit
forM act: α → m Unit
act
:= bym: Type → Type ?u.7430
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
(forM xs fun x => act x) = List.forM xs act induction xs: List α
xsm: Type → Type ?u.7430
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
nil(forM [] fun x => act x) = List.forM [] act
m: Type → Type ?u.7430
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
head✝: α
tail✝: List α
cons(forM (head✝ :: tail✝) fun x => act x) = List.forM (head✝ :: tail✝) act <;>m: Type → Type ?u.7430
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
nil(forM [] fun x => act x) = List.forM [] act
m: Type → Type ?u.7430
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
head✝: α
tail✝: List α
cons(forM (head✝ :: tail✝) fun x => act x) = List.forM (head✝ :: tail✝) act simp_all!Goals accomplished! 🐙

def ex2: {β : Type} → (β → α → m β) → β → List α → m β
ex2 (f: β → α → m β
f : β: Type
β → α: Type
α → m: Type → Type u_1
m β: Type
β) (init: β
init : β: Type
β) (xs: List α
xs : List: Type → Type
List α: Type
α) : m: Type → Type u_1
m β: Type
β := do'
  let mut y: β
y := init: β
init;
  for x: α
x in xs: List α
xs do' {
    y ← f: β → α → m β
f y: β
y x: α
x
  };
  return y: β
y

example: ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] (xs : List α) {β : Type} {init : β} [inst_1 : LawfulMonad m]
  (f : β → α → m β), ex2 f init xs = List.foldlM f init xs
example [LawfulMonad: (m : Type ?u.8985 → Type ?u.8984) → [inst : Monad m] → Prop
LawfulMonad m: Type → Type u_1
m] (f: β → α → m β
f : β: Type
β → α: Type
α → m: Type → Type u_1
m β: Type
β) :
    ex2: {m : Type → Type u_1} → {α : Type} → [inst : Monad m] → {β : Type} → (β → α → m β) → β → List α → m β
ex2 f: β → α → m β
f init: β
init xs: List α
xs = xs: List α
xs.foldlM: {m : Type → Type u_1} → [inst : Monad m] → {s α : Type} → (s → α → m s) → s → List α → m s
foldlM f: β → α → m β
f init: β
init := bym: Type → Type ?u.8948
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
β: Type
init: β
f: β → α → m β
ex2 f init xs = List.foldlM f init xs
  unfold ex2m: Type → Type ?u.8948
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
β: Type
init: β
f: β → α → m β
ExceptCpsT.runCatch
    (let y := init;
    StateT.run'
      (do
        forM xs fun x => do
            let y ← get
            let y ← StateT.lift (ExceptCpsT.lift (f y x))
            let _ ← get
            set y
        let y ← get
        StateT.lift (throw y))
      y) =
  List.foldlM f init xs; induction xs: List α
xs generalizing init: β
initm: Type → Type ?u.8948
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
β: Type
f: β → α → m β
init: β
nilExceptCpsT.runCatch
    (let y := init;
    StateT.run'
      (do
        forM [] fun x => do
            let y ← get
            let y ← StateT.lift (ExceptCpsT.lift (f y x))
            let _ ← get
            set y
        let y ← get
        StateT.lift (throw y))
      y) =
  List.foldlM f init []
m: Type → Type ?u.8948
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
β: Type
f: β → α → m β
head✝: α
tail✝: List α
init: β
consExceptCpsT.runCatch
    (let y := init;
    StateT.run'
      (do
        forM (head✝ :: tail✝) fun x => do
            let y ← get
            let y ← StateT.lift (ExceptCpsT.lift (f y x))
            let _ ← get
            set y
        let y ← get
        StateT.lift (throw y))
      y) =
  List.foldlM f init (head✝ :: tail✝) <;>m: Type → Type ?u.8948
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
β: Type
f: β → α → m β
init: β
nilExceptCpsT.runCatch
    (let y := init;
    StateT.run'
      (do
        forM [] fun x => do
            let y ← get
            let y ← StateT.lift (ExceptCpsT.lift (f y x))
            let _ ← get
            set y
        let y ← get
        StateT.lift (throw y))
      y) =
  List.foldlM f init []
m: Type → Type ?u.8948
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
β: Type
f: β → α → m β
head✝: α
tail✝: List α
init: β
consExceptCpsT.runCatch
    (let y := init;
    StateT.run'
      (do
        forM (head✝ :: tail✝) fun x => do
            let y ← get
            let y ← StateT.lift (ExceptCpsT.lift (f y x))
            let _ ← get
            set y
        let y ← get
        StateT.lift (throw y))
      y) =
  List.foldlM f init (head✝ :: tail✝) simp_all!Goals accomplished! 🐙

@[simp] theorem List.find?_cons: ∀ {x : α} {p : α → Bool} {xs : List α}, find? p (x :: xs) = if p x = true then some x else find? p xs
List.find?_cons {xs: List α
xs : List: Type ?u.17785 → Type ?u.17785
List α: Type
α} : (x: α
x::xs: List α
xs).find?: {α : Type} → (α → Bool) → List α → Option α
find? p: α → Bool
p = if p: α → Bool
p x: α
x then some: {α : Type} → α → Option α
some x: α
x else xs: List α
xs.find?: {α : Type} → (α → Bool) → List α → Option α
find? p: α → Bool
p := bym: Type → Type ?u.17767
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
x: α
p: α → Bool
xs: List α
find? p (x :: xs) = if p x = true then some x else find? p xs
  cases h : p: α → Bool
p x: α
xm: Type → Type ?u.17767
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
x: α
p: α → Bool
xs: List α
h: p x = false
falsefind? p (x :: xs) = if false = true then some x else find? p xs
m: Type → Type ?u.17767
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
x: α
p: α → Bool
xs: List α
h: p x = true
truefind? p (x :: xs) = if true = true then some x else find? p xs <;>m: Type → Type ?u.17767
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
x: α
p: α → Bool
xs: List α
h: p x = false
falsefind? p (x :: xs) = if false = true then some x else find? p xs
m: Type → Type ?u.17767
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
x: α
p: α → Bool
xs: List α
h: p x = true
truefind? p (x :: xs) = if true = true then some x else find? p xs simp_all!Goals accomplished! 🐙

example: ∀ {α : Type} (xs : List α) (p : α → Bool),
  Id.run
      (ExceptCpsT.runCatch do
        forM xs fun x => if p x = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)) =
    List.find? p xs
example (p: α → Bool
p : α: Type
α → Bool: Type
Bool) : Id.run: {α : Type} → Id α → α
Id.run
    (do' for x: α
x in xs: List α
xs do' {
           if p: α → Bool
p x: α
x then {
             return some: {α : Type} → α → Option α
some x: α
x
           }
         };
         pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure none: {α : Type} → Option α
none)
    =
    xs: List α
xs.find?: {α : Type} → (α → Bool) → List α → Option α
find? p: α → Bool
p
:= bym: Type → Type ?u.18571
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → Bool
Id.run
    (ExceptCpsT.runCatch do
      forM xs fun x => if p x = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
  List.find? p xs induction xs: List α
xs withm: Type → Type ?u.18571
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → Bool
Id.run
    (ExceptCpsT.runCatch do
      forM xs fun x => if p x = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
  List.find? p xs
      | nil =>m: Type → Type ?u.18571
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → Bool
nilId.run
    (ExceptCpsT.runCatch do
      forM [] fun x => if p x = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
  List.find? p [] simp [Id.run: {α : Type ?u.18948} → Id α → α
Id.run, List.find?: {α : Type ?u.18951} → (α → Bool) → List α → Option α
List.find?]Goals accomplished! 🐙
      | cons x: α
x =>m: Type → Type ?u.18571
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → Bool
x: α
tail✝: List α
consId.run
    (ExceptCpsT.runCatch do
      forM (x :: tail✝) fun x => if p x = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
  List.find? p (x :: tail✝) cases h : p: α → Bool
p x: α
xm: Type → Type ?u.18571
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → Bool
x: α
tail✝: List α
h: p x = false
cons.falseId.run
    (ExceptCpsT.runCatch do
      forM (x :: tail✝) fun x => if p x = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
  List.find? p (x :: tail✝)
m: Type → Type ?u.18571
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → Bool
x: α
tail✝: List α
h: p x = true
cons.trueId.run
    (ExceptCpsT.runCatch do
      forM (x :: tail✝) fun x => if p x = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
  List.find? p (x :: tail✝) <;>m: Type → Type ?u.18571
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → Bool
x: α
tail✝: List α
h: p x = false
cons.falseId.run
    (ExceptCpsT.runCatch do
      forM (x :: tail✝) fun x => if p x = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
  List.find? p (x :: tail✝)
m: Type → Type ?u.18571
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → Bool
x: α
tail✝: List α
h: p x = true
cons.trueId.run
    (ExceptCpsT.runCatch do
      forM (x :: tail✝) fun x => if p x = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
  List.find? p (x :: tail✝) simp_all [Id.run: {α : Type ?u.19970} → Id α → α
Id.run]Goals accomplished! 🐙

variable (p: α → m Bool
p : α: Type
α → m: Type → Type ?u.38841
m Bool: Type
Bool)

theorem byCases_Bool_bind: ∀ {m : Type → Type u_1} [inst : Monad m] {β : Type} (x : m Bool) (f g : Bool → m β),
  f true = g true → f false = g false → x >>= f = x >>= g
byCases_Bool_bind (x: m Bool
x : m: Type → Type u_1
m Bool: Type
Bool) (f: Bool → m β
f g: Bool → m β
g : Bool: Type
Bool → m: Type → Type u_1
m β: Type
β) (isTrue: f true = g true
isTrue : f: Bool → m β
f true: Bool
true = g: Bool → m β
g true: Bool
true) (isFalse: f false = g false
isFalse : f: Bool → m β
f false: Bool
false = g: Bool → m β
g false: Bool
false) : (x: m Bool
x >>= f: Bool → m β
f) = (x: m Bool
x >>= g: Bool → m β
g) := bym: Type → Type u_1
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
β: Type
x: m Bool
f, g: Bool → m β
isTrue: f true = g true
isFalse: f false = g false
x >>= f = x >>= g
  have : f: Bool → m β
f = g: Bool → m β
g :=m: Type → Type u_1
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
β: Type
x: m Bool
f, g: Bool → m β
isTrue: f true = g true
isFalse: f false = g false
x >>= f = x >>= g bym: Type → Type u_1
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
β: Type
x: m Bool
f, g: Bool → m β
isTrue: f true = g true
isFalse: f false = g false
f = g
    funext b: Bool
bm: Type → Type u_1
α: Type
inst✝: Monad m
ma, ma': m α
b✝: Bool
xs: List α
act: α → m Unit
p: α → m Bool
β: Type
x: m Bool
f, g: Bool → m β
isTrue: f true = g true
isFalse: f false = g false
b: Bool
hf b = g b
    cases b: Bool
b withm: Type → Type u_1
α: Type
inst✝: Monad m
ma, ma': m α
b✝: Bool
xs: List α
act: α → m Unit
p: α → m Bool
β: Type
x: m Bool
f, g: Bool → m β
isTrue: f true = g true
isFalse: f false = g false
b: Bool
hf b = g b
    | true  =>m: Type → Type u_1
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
β: Type
x: m Bool
f, g: Bool → m β
isTrue: f true = g true
isFalse: f false = g false
h.truef true = g true exact isTrue: f true = g true
isTrueGoals accomplished! 🐙
    | false =>m: Type → Type u_1
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
β: Type
x: m Bool
f, g: Bool → m β
isTrue: f true = g true
isFalse: f false = g false
h.falsef false = g false exact isFalse: f false = g false
isFalseGoals accomplished! 🐙
  rw [m: Type → Type u_1
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
β: Type
x: m Bool
f, g: Bool → m β
isTrue: f true = g true
isFalse: f false = g false
this: f = g
x >>= f = x >>= gthis: f = g
thism: Type → Type u_1
α: Type
inst✝: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
β: Type
x: m Bool
f, g: Bool → m β
isTrue: f true = g true
isFalse: f false = g false
this: f = g
x >>= g = x >>= g]Goals accomplished! 🐙

theorem eq_findM: ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] (xs : List α) (p : α → m Bool) [inst_1 : LawfulMonad m],
  (ExceptCpsT.runCatch do
      forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
    List.findM? p xs
eq_findM [LawfulMonad: (m : Type → Type u_1) → [inst : Monad m] → Prop
LawfulMonad m: Type → Type u_1
m] :
    (do' for x: α
x in xs: List α
xs do' {
           let b: Bool
b ← p: α → m Bool
p x: α
x;
           if b: Bool
b then {
             return some: {α : Type} → α → Option α
some x: α
x
           }
         };
         pure: {f : Type → Type u_1} → [self : Pure f] → {α : Type} → α → f α
pure none: {α : Type} → Option α
none)
    =
    xs: List α
xs.findM?: {m : Type → Type u_1} → [inst : Monad m] → {α : Type} → (α → m Bool) → List α → m (Option α)
findM? p: α → m Bool
p
:= bym: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
(ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs induction xs: List α
xs withm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
(ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
      | nil =>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
nil(ExceptCpsT.runCatch do
    forM [] fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p [] simp!Goals accomplished! 🐙
      | cons x: α
x xs: List α
xs ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
ih =>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons(ExceptCpsT.runCatch do
    forM (x :: xs) fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p (x :: xs)
        rw [m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons(ExceptCpsT.runCatch do
    forM (x :: xs) fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p (x :: xs)List.findM?,m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons(ExceptCpsT.runCatch do
    forM (x :: xs) fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ← p x
  match a with
    | true => pure (some x)
    | false => List.findM? p xs ← ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
ihm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons(ExceptCpsT.runCatch do
    forM (x :: xs) fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ← p x
  match a with
    | true => pure (some x)
    | false =>
      ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)]m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons(ExceptCpsT.runCatch do
    forM (x :: xs) fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ← p x
  match a with
    | true => pure (some x)
    | false =>
      ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none); simpm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons(do
    let a ← p x
    ExceptCpsT.runCatch do
        if a = true then throw (some x) else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)) =
  do
  let a ← p x
  match a with
    | true => pure (some x)
    | false =>
      ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
        apply byCases_Bool_bind: ∀ {m : Type → Type u_1} [inst : Monad m] {β : Type} (x : m Bool) (f g : Bool → m β),
  f true = g true → f false = g false → x >>= f = x >>= g
byCases_Bool_bindm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons.isTrue(ExceptCpsT.runCatch do
    if true = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  match true with
  | true => pure (some x)
  | false =>
    ExceptCpsT.runCatch do
      forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)
m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons.isFalse(ExceptCpsT.runCatch do
    if false = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  match false with
  | true => pure (some x)
  | false =>
    ExceptCpsT.runCatch do
      forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none) <;>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons.isTrue(ExceptCpsT.runCatch do
    if true = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  match true with
  | true => pure (some x)
  | false =>
    ExceptCpsT.runCatch do
      forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)
m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findM? p xs
cons.isFalse(ExceptCpsT.runCatch do
    if false = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  match false with
  | true => pure (some x)
  | false =>
    ExceptCpsT.runCatch do
      forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none) simpGoals accomplished! 🐙

def ex3: [inst : Monad m] → (α → m Bool) → List (List α) → m (Option α)
ex3 [Monad: (Type → Type u_1) → Type (max 1 u_1)
Monad m: Type → Type u_1
m] (p: α → m Bool
p : α: Type
α → m: Type → Type u_1
m Bool: Type
Bool) (xss: List (List α)
xss : List: Type → Type
List (List: Type → Type
List α: Type
α)) : m: Type → Type u_1
m (Option: Type → Type
Option α: Type
α) := do'
  for xs: List α
xs in xss: List (List α)
xss do' {
    for x: α
x in xs: List α
xs do' {
      let b: Bool
b ← p: α → m Bool
p x: α
x;
      if b: Bool
b then {
        return some: {α : Type} → α → Option α
some x: α
x
      }
    }
  };
  pure: {f : Type → Type u_1} → [self : Pure f] → {α : Type} → α → f α
pure none: {α : Type} → Option α
none

theorem eq_findSomeM_findM: ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] (p : α → m Bool) [inst_1 : LawfulMonad m] (xss : List (List α)),
  ex3 p xss = List.findSomeM? (fun xs => List.findM? p xs) xss
eq_findSomeM_findM [LawfulMonad: (m : Type → Type u_1) → [inst : Monad m] → Prop
LawfulMonad m: Type → Type u_1
m] (xss: List (List α)
xss : List: Type → Type
List (List: Type → Type
List α: Type
α)) :
    ex3: {m : Type → Type u_1} → {α : Type} → [inst : Monad m] → (α → m Bool) → List (List α) → m (Option α)
ex3 p: α → m Bool
p xss: List (List α)
xss = xss: List (List α)
xss.findSomeM?: {m : Type → Type u_1} → [inst : Monad m] → {α β : Type} → (α → m (Option β)) → List α → m (Option β)
findSomeM? (fun xs: List α
xs => xs: List α
xs.findM?: {m : Type → Type u_1} → [inst : Monad m] → {α : Type} → (α → m Bool) → List α → m (Option α)
findM? p: α → m Bool
p) := bym: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
ex3 p xss = List.findSomeM? (fun xs => List.findM? p xs) xss
  unfold ex3m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
(ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
  induction xss: List (List α)
xss withm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
(ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
  | nil =>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
nil(ExceptCpsT.runCatch do
    forM [] fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) [] simp!Goals accomplished! 🐙
  | cons xs: List α
xs xss: List (List α)
xss ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
ih =>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xs: List α
xss: List (List α)
ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
cons(ExceptCpsT.runCatch do
    forM (xs :: xss) fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) (xs :: xss)
    simp [List.findSomeM?: {m : Type ?u.27569 → Type ?u.27568} →
  [inst : Monad m] → {α : Type ?u.27567} → {β : Type ?u.27569} → (α → m (Option β)) → List α → m (Option β)
List.findSomeM?]m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xs: List α
xss: List (List α)
ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
cons(ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ← List.findM? p xs
  match a with
    | some b => pure (some b)
    | none => List.findSomeM? (fun xs => List.findM? p xs) xss
    rw [m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xs: List α
xss: List (List α)
ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
cons(ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ← List.findM? p xs
  match a with
    | some b => pure (some b)
    | none => List.findSomeM? (fun xs => List.findM? p xs) xss← ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
ih,m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xs: List α
xss: List (List α)
ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
cons(ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ← List.findM? p xs
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none) ← eq_findM: ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] (xs : List α) (p : α → m Bool) [inst_1 : LawfulMonad m],
  (ExceptCpsT.runCatch do
      forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift (pure none)) =
    List.findM? p xs
eq_findMm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xs: List α
xss: List (List α)
ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
cons(ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)]m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xs: List α
xss: List (List α)
ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
cons(ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
    induction xs: List α
xs withm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xs: List α
xss: List (List α)
ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
cons(ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
    | nil =>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
ih: (ExceptCpsT.runCatch do
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  List.findSomeM? (fun xs => List.findM? p xs) xss
cons.nil(ExceptCpsT.runCatch do
    forM [] fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM [] fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none) simpGoals accomplished! 🐙
    | cons x: α
x xs: List α
xs ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
ih =>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
cons.cons(ExceptCpsT.runCatch do
    forM (x :: xs) fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM (x :: xs) fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none) simpm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
cons.cons(do
    let a ← p x
    ExceptCpsT.runCatch do
        if a = true then throw (some x) else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)) =
  do
  let x_1 ← p x
  let a ←
    ExceptCpsT.runCatch do
        if x_1 = true then throw (some x) else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none); apply byCases_Bool_bind: ∀ {m : Type → Type u_1} [inst : Monad m] {β : Type} (x : m Bool) (f g : Bool → m β),
  f true = g true → f false = g false → x >>= f = x >>= g
byCases_Bool_bindm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
cons.cons.isTrue(ExceptCpsT.runCatch do
    if true = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        if true = true then throw (some x) else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
cons.cons.isFalse(ExceptCpsT.runCatch do
    if false = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        if false = true then throw (some x) else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none) <;>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
cons.cons.isTrue(ExceptCpsT.runCatch do
    if true = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        if true = true then throw (some x) else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
xss: List (List α)
x: α
xs: List α
ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
cons.cons.isFalse(ExceptCpsT.runCatch do
    if false = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        if false = true then throw (some x) else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none) simp [ih: (ExceptCpsT.runCatch do
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    forM xss fun xs =>
        forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw (some x) else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift (pure none)) =
  do
  let a ←
    ExceptCpsT.runCatch do
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
  match a with
    | some b => pure (some b)
    | none =>
      ExceptCpsT.runCatch do
        forM xss fun xs =>
            forM xs fun x => do
              let b ← ExceptCpsT.lift (p x)
              if b = true then throw (some x) else ExceptCpsT.lift (pure ())
        ExceptCpsT.lift (pure none)
ih]Goals accomplished! 🐙

def List.untilM: {m : Type → Type u_1} → {α : Type} → [inst : Monad m] → (α → m Bool) → List α → m Unit
List.untilM (p: α → m Bool
p : α: Type
α → m: Type → Type u_1
m Bool: Type
Bool) : List: Type → Type
List α: Type
α → m: Type → Type u_1
m Unit: Type
Unit
  | []    => pure: {f : Type → Type u_1} → [self : Pure f] → {α : Type} → α → f α
pure (): Unit
()
  | a: α
a::as: List α
as => p: α → m Bool
p a: α
a >>= fun | true: Bool
true => pure: {f : Type → Type u_1} → [self : Pure f] → {α : Type} → α → f α
pure (): Unit
() | false: Bool
false => as: List α
as.untilM: (α → m Bool) → List α → m Unit
untilM p: α → m Bool
p

theorem eq_untilM: ∀ [inst : LawfulMonad m],
  ExceptCpsT.runCatch
      (forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw () else ExceptCpsT.lift (pure ())) =
    List.untilM p xs
eq_untilM [LawfulMonad: (m : Type → Type u_1) → [inst : Monad m] → Prop
LawfulMonad m: Type → Type u_1
m] :
  (do' for x: α
x in xs: List α
xs do' {
         let b: Bool
b ← p: α → m Bool
p x: α
x;
         if b: Bool
b then {
           break
         }
       })
  =
  xs: List α
xs.untilM: {m : Type → Type u_1} → {α : Type} → [inst : Monad m] → (α → m Bool) → List α → m Unit
untilM p: α → m Bool
p
:= bym: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs induction xs: List α
xs withm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs
      | nil =>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs: List α
act: α → m Unit
p: α → m Bool
nilExceptCpsT.runCatch
    (forM [] fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p [] simp!Goals accomplished! 🐙
      | cons x: α
x xs: List α
xs ih: ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs
ih =>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs
consExceptCpsT.runCatch
    (forM (x :: xs) fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p (x :: xs)
        simp [List.untilM: {m : Type → Type ?u.34317} → {α : Type} → [inst : Monad m] → (α → m Bool) → List α → m Unit
List.untilM]m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs
cons(do
    let a ← p x
    ExceptCpsT.runCatch do
        if a = true then throw () else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw () else ExceptCpsT.lift (pure ())) =
  do
  let x ← p x
  match x with
    | true => pure ()
    | false => List.untilM p xs; rw [m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs
cons(do
    let a ← p x
    ExceptCpsT.runCatch do
        if a = true then throw () else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw () else ExceptCpsT.lift (pure ())) =
  do
  let x ← p x
  match x with
    | true => pure ()
    | false => List.untilM p xs← ih: ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs
ihm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs
cons(do
    let a ← p x
    ExceptCpsT.runCatch do
        if a = true then throw () else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw () else ExceptCpsT.lift (pure ())) =
  do
  let x ← p x
  match x with
    | true => pure ()
    | false =>
      ExceptCpsT.runCatch
        (forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw () else ExceptCpsT.lift (pure ()))]m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
ih: ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs
cons(do
    let a ← p x
    ExceptCpsT.runCatch do
        if a = true then throw () else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw () else ExceptCpsT.lift (pure ())) =
  do
  let x ← p x
  match x with
    | true => pure ()
    | false =>
      ExceptCpsT.runCatch
        (forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw () else ExceptCpsT.lift (pure ())); clear ih: ExceptCpsT.runCatch
    (forM xs fun x => do
      let b ← ExceptCpsT.lift (p x)
      if b = true then throw () else ExceptCpsT.lift (pure ())) =
  List.untilM p xs
ihm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
cons(do
    let a ← p x
    ExceptCpsT.runCatch do
        if a = true then throw () else ExceptCpsT.lift (pure ())
        forM xs fun x => do
            let b ← ExceptCpsT.lift (p x)
            if b = true then throw () else ExceptCpsT.lift (pure ())) =
  do
  let x ← p x
  match x with
    | true => pure ()
    | false =>
      ExceptCpsT.runCatch
        (forM xs fun x => do
          let b ← ExceptCpsT.lift (p x)
          if b = true then throw () else ExceptCpsT.lift (pure ()))
        apply byCases_Bool_bind: ∀ {m : Type → Type u_1} [inst : Monad m] {β : Type} (x : m Bool) (f g : Bool → m β),
  f true = g true → f false = g false → x >>= f = x >>= g
byCases_Bool_bindm: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
cons.isTrue(ExceptCpsT.runCatch do
    if true = true then throw () else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw () else ExceptCpsT.lift (pure ())) =
  match true with
  | true => pure ()
  | false =>
    ExceptCpsT.runCatch
      (forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw () else ExceptCpsT.lift (pure ()))
m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
cons.isFalse(ExceptCpsT.runCatch do
    if false = true then throw () else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw () else ExceptCpsT.lift (pure ())) =
  match false with
  | true => pure ()
  | false =>
    ExceptCpsT.runCatch
      (forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw () else ExceptCpsT.lift (pure ())) <;>m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
cons.isTrue(ExceptCpsT.runCatch do
    if true = true then throw () else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw () else ExceptCpsT.lift (pure ())) =
  match true with
  | true => pure ()
  | false =>
    ExceptCpsT.runCatch
      (forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw () else ExceptCpsT.lift (pure ()))
m: Type → Type u_1
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
xs✝: List α
act: α → m Unit
p: α → m Bool
x: α
xs: List α
cons.isFalse(ExceptCpsT.runCatch do
    if false = true then throw () else ExceptCpsT.lift (pure ())
    forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw () else ExceptCpsT.lift (pure ())) =
  match false with
  | true => pure ()
  | false =>
    ExceptCpsT.runCatch
      (forM xs fun x => do
        let b ← ExceptCpsT.lift (p x)
        if b = true then throw () else ExceptCpsT.lift (pure ())) simpGoals accomplished! 🐙

/-
The notation `[0:10]` is a range from 0 to 10 (exclusively).
-/

#eval0
0
1
0
2
0
3
0
4
0
5
 do'
  for x: Nat
x in [0: Nat
0:10: Nat
10] do' {
    if x: Nat
x > 5: Nat
5 then {
      break
    };
    for y: Nat
y in [0: Nat
0:x: Nat
x] do' {
      IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println y: Nat
y;
      break
    };
    IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println x: Nat
x
  }

#eval0
1
2
3
4
5
 do'
  for x: Nat
x in [0: Nat
0:10: Nat
10] do' {
    if x: Nat
x > 5: Nat
5 then {
      break
    };
    IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println x: Nat
x
  }

#eval1
3
5
 do'
  for x: Nat
x in [0: Nat
0:10: Nat
10] do' {
    if x: Nat
x % 2: Nat
2 == 0: Nat
0 then {
      continue
    };
    if x: Nat
x > 5: Nat
5 then {
      break
    };
    IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println x: Nat
x
  }

#eval1
3
5
 do'
  for x: Nat
x in [0: Nat
0:10: Nat
10] do' {
    if x: Nat
x % 2: Nat
2 == 0: Nat
0 then {
      continue
    };
    if x: Nat
x > 5: Nat
5 then {
      return ()
    };
    IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println x: Nat
x
  }


-- set_option trace.compiler.ir.init true
def ex1: List Nat → Nat → Id Nat
ex1 (xs: List Nat
xs : List: Type → Type
List Nat: Type
Nat) (z: Nat
z : Nat: Type
Nat) : Id: Type → Type
Id Nat: Type
Nat := do'
  let mut s1: Nat
s1 := 0: Nat
0;
  let mut s2: Nat
s2 := 0: Nat
0;
  for x: Nat
x in xs: List Nat
xs do' {
    if x: Nat
x % 2: Nat
2 == 0: Nat
0 then {
      continue
    };
    if x: Nat
x == z: Nat
z then {
      return s1: Nat
s1
    };
    s1 := s1: Nat
s1 + x: Nat
x;
    s2 := s2: Nat
s2 + s1: Nat
s1
  };
  return (s1: Nat
s1 + s2: Nat
s2)

/-
Adding `repeat` and `while` statements
-/

-- The "partial" keyword allows users to define non-terminating functions in Lean.
-- However, we currently cannot reason about them.
@[specialize] partial def loopForever: [inst : Monad m] → (Unit → m Unit) → m Unit
loopForever [Monad: (Type → Type u_1) → Type (max 1 u_1)
Monad m: Type → Type u_1
m] (f: Unit → m Unit
f : Unit: Type
Unit → m: Type → Type u_1
m Unit: Type
Unit) : m: Type → Type u_1
m Unit: Type
Unit :=
  f: Unit → m Unit
f (): Unit
() *> loopForever: [inst : Monad m] → (Unit → m Unit) → m Unit
loopForever f: Unit → m Unit
f

-- `Loop'` is a "helper" type. It is similar to `Unit`.
-- Its `ForM` instance produces an "infinite" sequence of units.
inductive Loop': Type
Loop' where
  | mk: Loop'
mk : Loop': Type
Loop'

instance: {m : Type → Type u_1} → ForM m Loop' Unit
instance : ForM: (Type → Type u_1) → Type → outParam Type → Type (max (max 1 u_1) 0)
ForM m: Type → Type u_1
m Loop': Type
Loop' Unit: Type
Unit where
  forM _ f: Unit → m PUnit
f := loopForever: {m : Type → Type u_1} → [inst : Monad m] → (Unit → m Unit) → m Unit
loopForever f: Unit → m PUnit
f

macro:0 "repeat" s: TSyntax `stmt
s:stmt:1 : stmt => `(stmt| for u in Loop'.mk do' $s: TSyntax `stmt
s)

#eval0
1
2
3
4
5
6
7
8
9
10
11
 do'
  let mut i: Nat
i := 0: Nat
0;
  repeat {
    if i: Nat
i > 10: Nat
10 then {
      break
    };
    IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println i: Nat
i;
    i := i: Nat
i + 1: Nat
1
  };
  return i: Nat
i

macro:0 "while" c: TSyntax `term
c:term "do'" s: TSyntax `stmt
s:stmt:1 : stmt => `(stmt| repeat { unless $c: TSyntax `term
c do' break; { $s: TSyntax `stmt
s } })

#eval0
1
2
3
4
5
6
7
8
9
10
 do'
  let mut i: Nat
i := 0: Nat
0;
  while (i: Nat
i < 10: Nat
10) do' {
    IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println i: Nat
i;
    i := i: Nat
i + 1: Nat
1
  };
  return i: Nat
i

"'do' Unchained" rendered supplement

Iteration