This file contains simp lemmas for proofs about code that uses the do notation together with Except and Option.

@[simp]

theorem Except.bind_ok_T {α ε β : Type u_1} (a : α) (f : α → ExceptT ε Id β) : ok a >>= f = f a

@[simp]

theorem Except.bind_ok {α : Type u_1} {ε : Type u_2} {β : Type u_1} (a : α) (f : α → Except ε β) : ok a >>= f = f a

@[simp]

theorem Except.bind_err {ε : Type u_1} {α β : Type u_2} (e : ε) (f : α → Except ε β) : error e >>= f = error e

theorem bind_ne_error {α β : Type u_1} {ε : Type u_2} {r : Except ε α} {f : α → Except ε β} {e : ε} (hr : r ≠ Except.error e) (hf : ∀ (a : α), r = Except.ok a → f a ≠ Except.error e) : r >>= f ≠ Except.error e

Monadic bind preserves "not this error": if neither the first computation nor the continuation (on success) yields error e, the bind does not either.

@[simp]

theorem Option.bind_some_T {α β : Type u_1} (a : α) (f : α → OptionT Id β) : some a >>= f = f a

@[simp]

theorem Option.bind_some_fun {α β : Type u_1} (a : α) (f : α → Option β) : some a >>= f = f a

@[simp]

theorem Option.bind_none_fun {α β : Type u_1} (f : α → Option β) : none >>= f = none

theorem do_some {α β : Type u_1} {b : β} {opt : Option α} {f : α → β} : (do let v ← opt some (f v)) = some b ↔ ∃ (a : α), opt = some a ∧ f a = b

theorem do_error {ε : Type u_1} {α β : Type u_2} {res : Except ε α} {e : ε} {f : α → β} : (do let v ← res Except.ok (f v)) = Except.error e ↔ res = Except.error e

theorem do_ok_eq_ok {ε : Type u_1} {α β : Type u_2} {b : β} {res : Except ε α} {f : α → β} : (do let v ← res Except.ok (f v)) = Except.ok b ↔ ∃ (a : α), res = Except.ok a ∧ f a = b

theorem do_eq_ok {ε : Type u_1} {α β : Type u_2} {b : β} {res : Except ε α} {f : α → Except ε β} : (do let v ← res f v) = Except.ok b ↔ ∃ (a : α), res = Except.ok a ∧ f a = Except.ok b

theorem do_eq_ok₂ {ε : Type u_1} {res₁ res₂ : Except ε PUnit} : (do res₁ res₂) = Except.ok () → res₁ = Except.ok () ∧ res₂ = Except.ok ()

theorem to_option_some {α : Type u_1} {ε : Type u_2} {v : α} {res : Except ε α} : res.toOption = some v ↔ res = Except.ok v

theorem to_option_none {ε : Type u_1} {α : Type u_2} {res : Except ε α} : res.toOption = none ↔ ∃ (err : ε), res = Except.error err

theorem to_option_left_ok {α : Type u_1} {ε₁ : Type u_2} {ε₂ : Type u_3} {v : α} {res₁ : Except ε₁ α} {res₂ : Except ε₂ α} : res₁.toOption = res₂.toOption → res₁ = Except.ok v → res₂ = Except.ok v

theorem to_option_right_ok {α : Type u_1} {ε₁ : Type u_2} {ε₂ : Type u_3} {v : α} {res₁ : Except ε₁ α} {res₂ : Except ε₂ α} : res₁.toOption = res₂.toOption → res₂ = Except.ok v → res₁ = Except.ok v

theorem to_option_right_ok' {α : Type u_1} {ε₁ : Type u_2} {ε₂ : Type u_3} {v : α} {res₁ : Except ε₁ α} : res₁.toOption = (Except.ok v).toOption → res₁ = Except.ok v

theorem to_option_left_ok' {α : Type u_1} {ε₁ : Type u_2} {ε₂ : Type u_3} {v : α} {res₂ : Except ε₂ α} : (Except.ok v).toOption = res₂.toOption → res₂ = Except.ok v

theorem to_option_left_err {ε₁ : Type u_1} {ε₂ : Type u_2} {α : Type u_3} {err₁ : ε₁} {res₂ : Except ε₂ α} : (Except.error err₁).toOption = res₂.toOption → ∃ (err₂ : ε₂), res₂ = Except.error err₂

theorem to_option_right_err {ε₂ : Type u_1} {ε₁ : Type u_2} {α : Type u_3} {err₂ : ε₂} {res₁ : Except ε₁ α} : res₁.toOption = (Except.error err₂).toOption → ∃ (err₁ : ε₁), res₁ = Except.error err₁

theorem do_error_to_option {ε : Type u_1} {α : Type u_2} {res : Except ε α} {e : ε} : (do let __x ← res match __x with | x => Except.error e).toOption = none

theorem do_to_option_none {ε : Type u_1} {α β : Type u_2} {res : Except ε α} {f : α → Except ε β} : res.toOption = none → (do let x ← res f x).toOption = none

theorem do_to_option_some {ε : Type u_1} {α β : Type u_2} {res : Except ε α} {v : α} {f : α → Except ε β} : res.toOption = some v → (do let x ← res f x) = f v

theorem to_option_eq_do₁ {α β : Type u_1} {ε : Type u_2} {res₁ res₂ : Except ε α} (f : α → Except ε β) : res₁.toOption = res₂.toOption → (do let x ← res₁ f x).toOption = (do let x ← res₂ f x).toOption

theorem to_option_eq_do₂ {α : Type u_1} {ε : Type u_2} {res₁ res₂ res₃ res₄ : Except ε α} (f : α → α → Except ε α) : res₁.toOption = res₃.toOption → res₂.toOption = res₄.toOption → (do let x ← res₁ let y ← res₂ f x y).toOption = (do let x ← res₃ let y ← res₄ f x y).toOption

@[simp]

theorem to_option_distr_map {ε : Type u_1} {α : Type u_2} {β : Type u_3} {x : Except ε α} {f : α → β} : (Except.map f x).toOption = Option.map f x.toOption

@[simp]

theorem to_option_distr_fmap {ε : Type u_1} {α β : Type u_2} {x : Except ε α} {f : α → β} : (f <$> x).toOption = f <$> x.toOption