Theorem: Fitree.interp_bind (MLIR/Semantics/Fitree.lean)

State before:
E✝¹ E✝ : Type → Type
h : E✝¹ ~> Fitree E✝
R✝¹ : Type
t : Fitree E✝¹ R✝¹
R✝ : Type
k : R✝¹ → Fitree E✝¹ R✝
⊢ interp h (bind t k) = bind (interp h t) fun x => interp h (k x)
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
State after:
no goals

State before:
case Ret
E✝¹ E✝ : Type → Type
h : E✝¹ ~> Fitree E✝
R✝¹ R✝ : Type
k : R✝¹ → Fitree E✝¹ R✝
r✝ : R✝¹
⊢ interp h (bind (Ret r✝) k) = bind (interp h (Ret r✝)) fun x => interp h (k x)
Tactic:
rfl
State after:
no goals

State before:
case Vis
E✝¹ E✝ : Type → Type
h : E✝¹ ~> Fitree E✝
R✝¹ R✝ : Type
k : R✝¹ → Fitree E✝¹ R✝
T✝ : Type
e✝ : E✝¹ T✝
k✝ : T✝ → Fitree E✝¹ R✝¹
ih : ∀ (a : T✝), interp h (bind (k✝ a) k) = bind (interp h (k✝ a)) fun x => interp h (k x)
⊢ interp h (bind (Vis e✝ k✝) k) = bind (interp h (Vis e✝ k✝)) fun x => interp h (k x)
Tactic:
simp [bind, ih]
State after:
no goals