Theorem: Fitree.seqLeft_eq (MLIR/Semantics/FitreeLaws.lean)

State before:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (SeqLeft.seqLeft t₁ fun x => t₂) = Seq.seq (Function.const R₂ <$> t₁) fun x => t₂
Tactic:
simp [SeqLeft.seqLeft, Seq.seq]
State after:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (bind t₁ fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> t₁) fun y => bind t₂ (ret ∘ y)

State before:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (bind t₁ fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> t₁) fun y => bind t₂ (ret ∘ y)
Tactic:
induction t₁ with
| Ret _ => rfl
| Vis _ _ ih => simp [bind]; funext _; simp [ih]; sorry
State after:
no goals

State before:
case Ret
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
r✝ : R₁
⊢ (bind (Ret r✝) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> Ret r✝) fun y => bind t₂ (ret ∘ y)
Tactic:
rfl
State after:
no goals

State before:
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (bind (Vis e✝ k✝) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> Vis e✝ k✝) fun y => bind t₂ (ret ∘ y)
Tactic:
simp [bind]
State after:
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (fun r => bind (k✝ r) fun a => bind t₂ fun x => ret a) = fun r =>
    bind (k✝ r) fun x => bind t₂ (ret ∘ Function.const R₂ x)

State before:
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (fun r => bind (k✝ r) fun a => bind t₂ fun x => ret a) = fun r =>
    bind (k✝ r) fun x => bind t₂ (ret ∘ Function.const R₂ x)
Tactic:
funext _
State after:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (k✝ x✝) fun a => bind t₂ fun x => ret a) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ Function.const R₂ x)

State before:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (k✝ x✝) fun a => bind t₂ fun x => ret a) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ Function.const R₂ x)
Tactic:
simp [ih]
State after:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (Function.const R₂ <$> k✝ x✝) fun y => bind t₂ (ret ∘ y)) =
    bind (k✝ x✝) fun x => bind t₂ (ret ∘ Function.const R₂ x)

State before:
case Vis.h
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih :
  ∀ (a : T✝),
    (bind (k✝ a) fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (Function.const R₂ <$> k✝ x✝) fun y => bind t₂ (ret ∘ y)) =
    bind (k✝ x✝) fun x => bind t₂ (ret ∘ Function.const R₂ x)
Tactic:
sorry
State after:
no goals