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

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]
State after:
no goals

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]
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)

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]
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)

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₁]
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)

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
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)

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₂]
State after:
no goals

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]
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

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]
State after:
no goals

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
State after:
no goals

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 *
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)

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]
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)

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]
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)

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]
State after:
no goals

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]
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 }

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]
State after:
no goals