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

State before:
E F : Type → Type
T R : Type
h : E ~> OptionT (Fitree F)
t : Fitree E T
k : T → Fitree E R
⊢ interpOption h (bind t k) =
    bind (interpOption h t) fun x? =>
      match x? with
      | some x => interpOption h (k x)
      | none => ret none
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih =>
    simp [interpOption] at *
    simp [interp, bind, Bind.bind, OptionT.bind, OptionT.mk]
    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 F : Type → Type
T R : Type
h : E ~> OptionT (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ interpOption h (bind (Ret r✝) k) =
    bind (interpOption h (Ret r✝)) fun x? =>
      match x? with
      | some x => interpOption h (k x)
      | none => ret none
Tactic:
rfl
State after:
no goals

State before:
case Vis
E F : Type → Type
T R : Type
h : E ~> OptionT (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interpOption h (bind (k✝ a) k) =
      bind (interpOption h (k✝ a)) fun x? =>
        match x? with
        | some x => interpOption h (k x)
        | none => ret none
⊢ interpOption h (bind (Vis e✝ k✝) k) =
    bind (interpOption h (Vis e✝ k✝)) fun x? =>
      match x? with
      | some x => interpOption h (k x)
      | none => ret none
Tactic:
simp [interpOption] at *
State after:
case Vis
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
⊢ interp h (bind (Vis e✝ k✝) k) =
    bind (interp h (Vis e✝ k✝)) fun x? =>
      match x? with
      | some x => interp h (k x)
      | none => ret none

State before:
case Vis
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
⊢ interp h (bind (Vis e✝ k✝) k) =
    bind (interp h (Vis e✝ k✝)) fun x? =>
      match x? with
      | some x => interp h (k x)
      | none => ret none
Tactic:
simp [interp, bind, Bind.bind, OptionT.bind, OptionT.mk]
State after:
case Vis
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
⊢ (bind (h T✝ e✝) fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | some a => interp h (k✝ a)
        | none => ret none)
        fun x? =>
        match x? with
        | some x => interp h (k x)
        | none => ret none

State before:
case Vis
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
⊢ (bind (h T✝ e✝) fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | some a => interp h (k✝ a)
        | none => ret none)
        fun x? =>
        match x? with
        | some x => interp h (k x)
        | none => ret none
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 F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
fequal2 : ∀ (α : Sort ?u.47259) (β : Sort ?u.47260) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (bind (h T✝ e✝) fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | some a => interp h (k✝ a)
        | none => ret none)
        fun x? =>
        match x? with
        | some x => interp h (k x)
        | none => ret none

State before:
case Vis
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
fequal2 : ∀ (α : Sort ?u.47259) (β : Sort ?u.47260) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (bind (h T✝ e✝) fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | some a => interp h (k✝ a)
        | none => ret none)
        fun x? =>
        match x? with
        | some x => interp h (k x)
        | none => ret none
Tactic:
apply fequal2
State after:
case Vis.a
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
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 F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    fun x =>
    bind
      (match x with
      | some a => interp h (k✝ a)
      | none => ret none)
      fun x? =>
      match x? with
      | some x => interp h (k x)
      | none => ret none

State before:
case Vis.a
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
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 F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    fun x =>
    bind
      (match x with
      | some a => interp h (k✝ a)
      | none => ret none)
      fun x? =>
      match x? with
      | some x => interp h (k x)
      | none => ret none
Tactic:
rfl
State after:
case Vis.a
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    fun x =>
    bind
      (match x with
      | some a => interp h (k✝ a)
      | none => ret none)
      fun x? =>
      match x? with
      | some x => interp h (k x)
      | none => ret none

State before:
case Vis.a
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    fun x =>
    bind
      (match x with
      | some a => interp h (k✝ a)
      | none => ret none)
      fun x? =>
      match x? with
      | some x => interp h (k x)
      | none => ret none
Tactic:
funext x
State after:
case Vis.a.h
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Option T✝
⊢ (match x with
    | some a => interp h (bind (k✝ a) k)
    | none => ret none) =
    bind
      (match x with
      | some a => interp h (k✝ a)
      | none => ret none)
      fun x? =>
      match x? with
      | some x => interp h (k x)
      | none => ret none

State before:
case Vis.a.h
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Option T✝
⊢ (match x with
    | some a => interp h (bind (k✝ a) k)
    | none => ret none) =
    bind
      (match x with
      | some a => interp h (k✝ a)
      | none => ret none)
      fun x? =>
      match x? with
      | some x => interp h (k x)
      | none => ret none
Tactic:
cases x <;> simp [ih]
State after:
no goals

State before:
E F : Type → Type
T R : Type
h : E ~> OptionT (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
        | some x => interp h (k x)
        | none => ret none
α : Sort ?u.47259
β : Sort ?u.47260
f g : α → β
x y : α
h₁ : f = g
h₂ : x = y
⊢ f x = g y
Tactic:
simp [h₁, h₂]
State after:
no goals