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

State before:
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
s : S
h : E ~> StateT S (Fitree F)
t : Fitree E R
⊢ interpState h (bind t k) s =
    bind (interpState h t s) fun x =>
      match x with
      | (x, s') => interpState h (k x) s'
Tactic:
revert s
State after:
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
t : Fitree E R
⊢ ∀ {s : S},
    interpState h (bind t k) s =
      bind (interpState h t s) fun x =>
        match x with
        | (x, s') => interpState h (k x) s'

State before:
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
t : Fitree E R
⊢ ∀ {s : S},
    interpState h (bind t k) s =
      bind (interpState h t s) fun x =>
        match x with
        | (x, s') => interpState h (k x) s'
Tactic:
induction t with
| Ret _ => intros s; rfl
| Vis _ _ ih =>
  simp [interpState] at *
  simp [interp, Bind.bind, StateT.bind]
  simp [ih]
State after:
no goals

State before:
case Ret
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
r✝ : R
⊢ ∀ {s : S},
    interpState h (bind (Ret r✝) k) s =
      bind (interpState h (Ret r✝) s) fun x =>
        match x with
        | (x, s') => interpState h (k x) s'
Tactic:
intros s
State after:
case Ret
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
r✝ : R
s : S
⊢ interpState h (bind (Ret r✝) k) s =
    bind (interpState h (Ret r✝) s) fun x =>
      match x with
      | (x, s') => interpState h (k x) s'

State before:
case Ret
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
r✝ : R
s : S
⊢ interpState h (bind (Ret r✝) k) s =
    bind (interpState h (Ret r✝) s) fun x =>
      match x with
      | (x, s') => interpState h (k x) s'
Tactic:
rfl
State after:
no goals

State before:
case Vis
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R
ih :
  ∀ (a : T✝) {s : S},
    interpState h (bind (k✝ a) k) s =
      bind (interpState h (k✝ a) s) fun x =>
        match x with
        | (x, s') => interpState h (k x) s'
⊢ ∀ {s : S},
    interpState h (bind (Vis e✝ k✝) k) s =
      bind (interpState h (Vis e✝ k✝) s) fun x =>
        match x with
        | (x, s') => interpState h (k x) s'
Tactic:
simp [interpState] at *
State after:
case Vis
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R
ih : ∀ (a : T✝) {s : S}, interp h (bind (k✝ a) k) s = bind (interp h (k✝ a) s) fun x => interp h (k x.fst) x.snd
⊢ ∀ {s : S}, interp h (bind (Vis e✝ k✝) k) s = bind (interp h (Vis e✝ k✝) s) fun x => interp h (k x.fst) x.snd

State before:
case Vis
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R
ih : ∀ (a : T✝) {s : S}, interp h (bind (k✝ a) k) s = bind (interp h (k✝ a) s) fun x => interp h (k x.fst) x.snd
⊢ ∀ {s : S}, interp h (bind (Vis e✝ k✝) k) s = bind (interp h (Vis e✝ k✝) s) fun x => interp h (k x.fst) x.snd
Tactic:
simp [interp, Bind.bind, StateT.bind]
State after:
case Vis
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R
ih : ∀ (a : T✝) {s : S}, interp h (bind (k✝ a) k) s = bind (interp h (k✝ a) s) fun x => interp h (k x.fst) x.snd
⊢ ∀ {s : S},
    (bind (h T✝ e✝ s) fun __discr => interp h (bind (k✝ __discr.fst) k) __discr.snd) =
      bind (h T✝ e✝ s) fun x => bind (interp h (k✝ x.fst) x.snd) fun x => interp h (k x.fst) x.snd

State before:
case Vis
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R
ih : ∀ (a : T✝) {s : S}, interp h (bind (k✝ a) k) s = bind (interp h (k✝ a) s) fun x => interp h (k x.fst) x.snd
⊢ ∀ {s : S},
    (bind (h T✝ e✝ s) fun __discr => interp h (bind (k✝ __discr.fst) k) __discr.snd) =
      bind (h T✝ e✝ s) fun x => bind (interp h (k✝ x.fst) x.snd) fun x => interp h (k x.fst) x.snd
Tactic:
simp [ih]
State after:
no goals