internlm/Lean-Github huggingface dataset:
Theorem: Fitree.interpState_bind
Proof 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
Proof 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'
Theorem: Fitree.interpState_bind
Proof 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]
Proof state after:
no goals
Theorem: Fitree.interpState_bind
Proof 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
Proof 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'
Theorem: Fitree.interpState_bind
Proof 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
Proof state after:
no goals
Theorem: Fitree.interpState_bind
Proof 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 *
Proof 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
Theorem: Fitree.interpState_bind
Proof 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]
Proof 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
Theorem: Fitree.interpState_bind
Proof 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]
Proof state after:
no goals
Theorem: Fitree.interpWriter_bind
Proof state before:
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
t : Fitree E T
k : T → Fitree E R
⊢ interpWriter h (bind t k) =
    bind (interpWriter h t) fun x =>
      match x with
      | (x, s₁) =>
        bind (interpWriter h (k x)) fun x =>
          match x with
          | (y, s₂) => ret (y, s₁ ++ s₂)
Tactic:
induction t with
| Ret _ =>
    simp [bind, interpWriter]
    have h₁: forall x, "" ++ x = x := by
      simp [HAppend.hAppend, Append.append, String.append]
      simp [List.nil_append]
    simp [h₁]
    have h₂: forall (α β: Type) (x: α × β), (x.fst, x.snd) = x := by simp
    simp [h₂]
| Vis _ _ ih =>
    simp [interpWriter] at *
    simp [interp, Bind.bind, WriterT.bindCont, WriterT.mk]
    have h: forall (x y z: String), x ++ (y ++ z) = x ++ y ++ z := by
      simp [HAppend.hAppend, Append.append, String.append]
      simp [List.append_assoc]
    simp [ih, h]
Proof state after:
no goals
Theorem: Fitree.interpWriter_bind
Proof state before:
case Ret
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ interpWriter h (bind (Ret r✝) k) =
    bind (interpWriter h (Ret r✝)) fun x =>
      match x with
      | (x, s₁) =>
        bind (interpWriter h (k x)) fun x =>
          match x with
          | (y, s₂) => ret (y, s₁ ++ s₂)
Tactic:
simp [bind, interpWriter]
Proof state after:
case Ret
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ interp h (k r✝) = bind (interp h (k r✝)) fun x => ret (x.fst, "" ++ x.snd)
Theorem: Fitree.interpWriter_bind
Proof state before:
case Ret
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ interp h (k r✝) = bind (interp h (k r✝)) fun x => ret (x.fst, "" ++ x.snd)
Tactic:
have h₁: forall x, "" ++ x = x := by
  simp [HAppend.hAppend, Append.append, String.append]
  simp [List.nil_append]
Proof state after:
case Ret
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
h₁ : ∀ (x : String), "" ++ x = x
⊢ interp h (k r✝) = bind (interp h (k r✝)) fun x => ret (x.fst, "" ++ x.snd)
Theorem: Fitree.interpWriter_bind
Proof state before:
case Ret
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
h₁ : ∀ (x : String), "" ++ x = x
⊢ interp h (k r✝) = bind (interp h (k r✝)) fun x => ret (x.fst, "" ++ x.snd)
Tactic:
simp [h₁]
Proof state after:
case Ret
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
h₁ : ∀ (x : String), "" ++ x = x
⊢ interp h (k r✝) = bind (interp h (k r✝)) fun x => ret (x.fst, x.snd)
Theorem: Fitree.interpWriter_bind
Proof state before:
case Ret
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
h₁ : ∀ (x : String), "" ++ x = x
⊢ interp h (k r✝) = bind (interp h (k r✝)) fun x => ret (x.fst, x.snd)
Tactic:
have h₂: forall (α β: Type) (x: α × β), (x.fst, x.snd) = x := by simp
Proof state after:
case Ret
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
h₁ : ∀ (x : String), "" ++ x = x
h₂ : ∀ (α β : Type) (x : α × β), (x.fst, x.snd) = x
⊢ interp h (k r✝) = bind (interp h (k r✝)) fun x => ret (x.fst, x.snd)
Theorem: Fitree.interpWriter_bind
Proof state before:
case Ret
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
h₁ : ∀ (x : String), "" ++ x = x
h₂ : ∀ (α β : Type) (x : α × β), (x.fst, x.snd) = x
⊢ interp h (k r✝) = bind (interp h (k r✝)) fun x => ret (x.fst, x.snd)
Tactic:
simp [h₂]
Proof state after:
no goals
Theorem: Fitree.interpWriter_bind
Proof state before:
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ ∀ (x : String), "" ++ x = x
Tactic:
simp [HAppend.hAppend, Append.append, String.append]
Proof state after:
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ ∀ (x : String), { data := [] ++ x.data } = x
Theorem: Fitree.interpWriter_bind
Proof state before:
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ ∀ (x : String), { data := [] ++ x.data } = x
Tactic:
simp [List.nil_append]
Proof state after:
no goals
Theorem: Fitree.interpWriter_bind
Proof state before:
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
h₁ : ∀ (x : String), "" ++ x = x
⊢ ∀ (α β : Type) (x : α × β), (x.fst, x.snd) = x
Tactic:
simp
Proof state after:
no goals
Theorem: Fitree.interpWriter_bind
Proof state before:
case Vis
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interpWriter h (bind (k✝ a) k) =
      bind (interpWriter h (k✝ a)) fun x =>
        match x with
        | (x, s₁) =>
          bind (interpWriter h (k x)) fun x =>
            match x with
            | (y, s₂) => ret (y, s₁ ++ s₂)
⊢ interpWriter h (bind (Vis e✝ k✝) k) =
    bind (interpWriter h (Vis e✝ k✝)) fun x =>
      match x with
      | (x, s₁) =>
        bind (interpWriter h (k x)) fun x =>
          match x with
          | (y, s₂) => ret (y, s₁ ++ s₂)
Tactic:
simp [interpWriter] at *
Proof state after:
case Vis
E F : Type → Type
T R : Type
h : E ~> WriterT (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 => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
⊢ interp h (bind (Vis e✝ k✝) k) =
    bind (interp h (Vis e✝ k✝)) fun x => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
Theorem: Fitree.interpWriter_bind
Proof state before:
case Vis
E F : Type → Type
T R : Type
h : E ~> WriterT (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 => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
⊢ interp h (bind (Vis e✝ k✝) k) =
    bind (interp h (Vis e✝ k✝)) fun x => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
Tactic:
simp [interp, Bind.bind, WriterT.bindCont, WriterT.mk]
Proof state after:
case Vis
E F : Type → Type
T R : Type
h : E ~> WriterT (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 => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
⊢ (bind (h T✝ e✝) fun x => bind (interp h (bind (k✝ x.fst) k)) fun y => ret (y.fst, x.snd ++ y.snd)) =
    bind (h T✝ e✝) fun x =>
      bind (interp h (k✝ x.fst)) fun x_1 =>
        bind (interp h (k x_1.fst)) fun x_2 => ret (x_2.fst, x.snd ++ x_1.snd ++ x_2.snd)
Theorem: Fitree.interpWriter_bind
Proof state before:
case Vis
E F : Type → Type
T R : Type
h : E ~> WriterT (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 => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
⊢ (bind (h T✝ e✝) fun x => bind (interp h (bind (k✝ x.fst) k)) fun y => ret (y.fst, x.snd ++ y.snd)) =
    bind (h T✝ e✝) fun x =>
      bind (interp h (k✝ x.fst)) fun x_1 =>
        bind (interp h (k x_1.fst)) fun x_2 => ret (x_2.fst, x.snd ++ x_1.snd ++ x_2.snd)
Tactic:
have h: forall (x y z: String), x ++ (y ++ z) = x ++ y ++ z := by
  simp [HAppend.hAppend, Append.append, String.append]
  simp [List.append_assoc]
Proof state after:
case Vis
E F : Type → Type
T R : Type
h✝ : E ~> WriterT (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 => bind (interp h✝ (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
h : ∀ (x y z : String), x ++ (y ++ z) = x ++ y ++ z
⊢ (bind (h✝ T✝ e✝) fun x => bind (interp h✝ (bind (k✝ x.fst) k)) fun y => ret (y.fst, x.snd ++ y.snd)) =
    bind (h✝ T✝ e✝) fun x =>
      bind (interp h✝ (k✝ x.fst)) fun x_1 =>
        bind (interp h✝ (k x_1.fst)) fun x_2 => ret (x_2.fst, x.snd ++ x_1.snd ++ x_2.snd)
Theorem: Fitree.interpWriter_bind
Proof state before:
case Vis
E F : Type → Type
T R : Type
h✝ : E ~> WriterT (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 => bind (interp h✝ (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
h : ∀ (x y z : String), x ++ (y ++ z) = x ++ y ++ z
⊢ (bind (h✝ T✝ e✝) fun x => bind (interp h✝ (bind (k✝ x.fst) k)) fun y => ret (y.fst, x.snd ++ y.snd)) =
    bind (h✝ T✝ e✝) fun x =>
      bind (interp h✝ (k✝ x.fst)) fun x_1 =>
        bind (interp h✝ (k x_1.fst)) fun x_2 => ret (x_2.fst, x.snd ++ x_1.snd ++ x_2.snd)
Tactic:
simp [ih, h]
Proof state after:
no goals
Theorem: Fitree.interpWriter_bind
Proof state before:
E F : Type → Type
T R : Type
h : E ~> WriterT (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 => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
⊢ ∀ (x y z : String), x ++ (y ++ z) = x ++ y ++ z
Tactic:
simp [HAppend.hAppend, Append.append, String.append]
Proof state after:
E F : Type → Type
T R : Type
h : E ~> WriterT (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 => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
⊢ ∀ (x y z : String), { data := x.data ++ (y.data ++ z.data) } = { data := x.data ++ y.data ++ z.data }
Theorem: Fitree.interpWriter_bind
Proof state before:
E F : Type → Type
T R : Type
h : E ~> WriterT (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 => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
⊢ ∀ (x y z : String), { data := x.data ++ (y.data ++ z.data) } = { data := x.data ++ y.data ++ z.data }
Tactic:
simp [List.append_assoc]
Proof state after:
no goals
Theorem: Fitree.interpOption_bind
Proof 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]
Proof state after:
no goals
Theorem: Fitree.interpOption_bind
Proof 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
Proof state after:
no goals
Theorem: Fitree.interpOption_bind
Proof 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 *
Proof 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
Theorem: Fitree.interpOption_bind
Proof 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]
Proof 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
Theorem: Fitree.interpOption_bind
Proof 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₂]
Proof 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
Theorem: Fitree.interpOption_bind
Proof 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
Proof 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
Theorem: Fitree.interpOption_bind
Proof 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
Proof 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