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

State before:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (SeqRight.seqRight t₁ fun x => t₂) = Seq.seq (Function.const R₁ id <$> t₁) fun x => t₂
Tactic:
simp [SeqRight.seqRight, Seq.seq]
State after:
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (bind t₁ fun x => t₂) = bind (Function.const R₁ id <$> 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 x => t₂) = bind (Function.const R₁ id <$> t₁) fun y => bind t₂ (ret ∘ y)
Tactic:
induction t₁ with
| Ret _ =>
  simp [Function.const, Function.comp, bind]
| 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 x => t₂) = bind (Function.const R₁ id <$> Ret r✝) fun y => bind t₂ (ret ∘ y)
Tactic:
simp [Function.const, Function.comp, bind]
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 x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (bind (Vis e✝ k✝) fun x => t₂) = bind (Function.const R₁ id <$> 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 x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (fun r => bind (k✝ r) fun x => t₂) = fun r => bind (k✝ r) fun x => bind t₂ (ret ∘ id)

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 x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (fun r => bind (k✝ r) fun x => t₂) = fun r => bind (k✝ r) fun x => bind t₂ (ret ∘ id)
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 x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (k✝ x✝) fun x => t₂) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ id)

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 x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (k✝ x✝) fun x => t₂) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ id)
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 x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (Function.const R₁ id <$> k✝ x✝) fun y => bind t₂ (ret ∘ y)) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ id)

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 x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (Function.const R₁ id <$> k✝ x✝) fun y => bind t₂ (ret ∘ y)) = bind (k✝ x✝) fun x => bind t₂ (ret ∘ id)
Tactic:
sorry
State after:
no goals