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

State before:
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
t : Fitree E T
k : T → Fitree E R
⊢ interpExcept h (bind t k) =
    bind (interpExcept h t) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interpExcept h (k x)
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih =>
    simp [interpExcept] at *
    simp [interp, bind, Bind.bind]
    simp [ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
    have fequal2 α β (f g: α → β) x y: f = g → x = y → f x = g y :=
      fun h₁ h₂ => by simp [h₁, h₂]
    apply fequal2; rfl; funext x
    cases x <;> simp [ih]
State after:
no goals

State before:
case Ret
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ interpExcept h (bind (Ret r✝) k) =
    bind (interpExcept h (Ret r✝)) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interpExcept h (k x)
Tactic:
rfl
State after:
no goals

State before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interpExcept h (bind (k✝ a) k) =
      bind (interpExcept h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interpExcept h (k x)
⊢ interpExcept h (bind (Vis e✝ k✝) k) =
    bind (interpExcept h (Vis e✝ k✝)) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interpExcept h (k x)
Tactic:
simp [interpExcept] at *
State after:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ interp h (bind (Vis e✝ k✝) k) =
    bind (interp h (Vis e✝ k✝)) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interp h (k x)

State before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ interp h (bind (Vis e✝ k✝) k) =
    bind (interp h (Vis e✝ k✝)) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interp h (k x)
Tactic:
simp [interp, bind, Bind.bind]
State after:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ bind (h T✝ e✝) (ExceptT.bindCont fun t => interp h (bind (k✝ t) k)) =
    bind (h T✝ e✝) fun x =>
      bind (ExceptT.bindCont (fun t => interp h (k✝ t)) x) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)

State before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ bind (h T✝ e✝) (ExceptT.bindCont fun t => interp h (bind (k✝ t) k)) =
    bind (h T✝ e✝) fun x =>
      bind (ExceptT.bindCont (fun t => interp h (k✝ t)) x) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
Tactic:
simp [ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
State after:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ (bind (h T✝ e✝) fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | Except.ok a => interp h (k✝ a)
        | Except.error e => ret (Except.error e))
        fun x? =>
        match x? with
        | Except.error e => ret (Except.error e)
        | Except.ok x => interp h (k x)

State before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ (bind (h T✝ e✝) fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | Except.ok a => interp h (k✝ a)
        | Except.error e => ret (Except.error e))
        fun x? =>
        match x? with
        | Except.error e => ret (Except.error e)
        | Except.ok x => interp h (k x)
Tactic:
have fequal2 α β (f g: α → β) x y: f = g → x = y → f x = g y :=
  fun h₁ h₂ => by simp [h₁, h₂]
State after:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α : Sort ?u.50273) (β : Sort ?u.50274) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (bind (h T✝ e✝) fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | Except.ok a => interp h (k✝ a)
        | Except.error e => ret (Except.error e))
        fun x? =>
        match x? with
        | Except.error e => ret (Except.error e)
        | Except.ok x => interp h (k x)

State before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α : Sort ?u.50273) (β : Sort ?u.50274) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (bind (h T✝ e✝) fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | Except.ok a => interp h (k✝ a)
        | Except.error e => ret (Except.error e))
        fun x? =>
        match x? with
        | Except.error e => ret (Except.error e)
        | Except.ok x => interp h (k x)
Tactic:
apply fequal2
State after:
case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ bind (h T✝ e✝) = bind (h T✝ e✝)

case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    fun x =>
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)

State before:
case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ bind (h T✝ e✝) = bind (h T✝ e✝)

case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    fun x =>
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)
Tactic:
rfl
State after:
case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    fun x =>
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)

State before:
case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    fun x =>
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)
Tactic:
funext x
State after:
case Vis.a.h
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Except ε T✝
⊢ (match x with
    | Except.ok a => interp h (bind (k✝ a) k)
    | Except.error e => ret (Except.error e)) =
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)

State before:
case Vis.a.h
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Except ε T✝
⊢ (match x with
    | Except.ok a => interp h (bind (k✝ a) k)
    | Except.error e => ret (Except.error e)) =
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)
Tactic:
cases x <;> simp [ih]
State after:
no goals

State before:
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
α : Sort ?u.50273
β : Sort ?u.50274
f g : α → β
x y : α
h₁ : f = g
h₂ : x = y
⊢ f x = g y
Tactic:
simp [h₁, h₂]
State after:
no goals