internlm/Lean-Github huggingface dataset:
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
⊢ (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
Proof 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
Theorem: Fitree.interpOption_bind
Proof 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]
Proof state after:
no goals
Theorem: Fitree.interpOption_bind
Proof 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₂]
Proof state after:
no goals
Theorem: Fitree.interpExcept_bind
Proof state before:
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
t : Fitree E T
k : T → Fitree E R
⊢ interpExcept h (bind t k) =
    bind (interpExcept h t) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interpExcept h (k x)
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih =>
    simp [interpExcept] at *
    simp [interp, bind, Bind.bind]
    simp [ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
    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.interpExcept_bind
Proof state before:
case Ret
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ interpExcept h (bind (Ret r✝) k) =
    bind (interpExcept h (Ret r✝)) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interpExcept h (k x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Fitree.interpExcept_bind
Proof state before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interpExcept h (bind (k✝ a) k) =
      bind (interpExcept h (k✝ a)) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interpExcept h (k x)
⊢ interpExcept h (bind (Vis e✝ k✝) k) =
    bind (interpExcept h (Vis e✝ k✝)) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interpExcept h (k x)
Tactic:
simp [interpExcept] at *
Proof state after:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ interp h (bind (Vis e✝ k✝) k) =
    bind (interp h (Vis e✝ k✝)) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interp h (k x)
Theorem: Fitree.interpExcept_bind
Proof state before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ interp h (bind (Vis e✝ k✝) k) =
    bind (interp h (Vis e✝ k✝)) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interp h (k x)
Tactic:
simp [interp, bind, Bind.bind]
Proof state after:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ bind (h T✝ e✝) (ExceptT.bindCont fun t => interp h (bind (k✝ t) k)) =
    bind (h T✝ e✝) fun x =>
      bind (ExceptT.bindCont (fun t => interp h (k✝ t)) x) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
Theorem: Fitree.interpExcept_bind
Proof state before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ bind (h T✝ e✝) (ExceptT.bindCont fun t => interp h (bind (k✝ t) k)) =
    bind (h T✝ e✝) fun x =>
      bind (ExceptT.bindCont (fun t => interp h (k✝ t)) x) fun x? =>
        match x? with
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
Tactic:
simp [ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
Proof state after:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ (bind (h T✝ e✝) fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | Except.ok a => interp h (k✝ a)
        | Except.error e => ret (Except.error e))
        fun x? =>
        match x? with
        | Except.error e => ret (Except.error e)
        | Except.ok x => interp h (k x)
Theorem: Fitree.interpExcept_bind
Proof state before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
⊢ (bind (h T✝ e✝) fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | Except.ok a => interp h (k✝ a)
        | Except.error e => ret (Except.error e))
        fun x? =>
        match x? with
        | Except.error e => ret (Except.error e)
        | Except.ok x => interp h (k x)
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 : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α : Sort ?u.50273) (β : Sort ?u.50274) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (bind (h T✝ e✝) fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | Except.ok a => interp h (k✝ a)
        | Except.error e => ret (Except.error e))
        fun x? =>
        match x? with
        | Except.error e => ret (Except.error e)
        | Except.ok x => interp h (k x)
Theorem: Fitree.interpExcept_bind
Proof state before:
case Vis
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α : Sort ?u.50273) (β : Sort ?u.50274) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (bind (h T✝ e✝) fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | Except.ok a => interp h (k✝ a)
        | Except.error e => ret (Except.error e))
        fun x? =>
        match x? with
        | Except.error e => ret (Except.error e)
        | Except.ok x => interp h (k x)
Tactic:
apply fequal2
Proof state after:
case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
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 : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    fun x =>
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)
Theorem: Fitree.interpExcept_bind
Proof state before:
case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
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 : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    fun x =>
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)
Tactic:
rfl
Proof state after:
case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    fun x =>
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)
Theorem: Fitree.interpExcept_bind
Proof state before:
case Vis.a
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => interp h (bind (k✝ a) k)
      | Except.error e => ret (Except.error e)) =
    fun x =>
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)
Tactic:
funext x
Proof state after:
case Vis.a.h
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Except ε T✝
⊢ (match x with
    | Except.ok a => interp h (bind (k✝ a) k)
    | Except.error e => ret (Except.error e)) =
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)
Theorem: Fitree.interpExcept_bind
Proof state before:
case Vis.a.h
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Except ε T✝
⊢ (match x with
    | Except.ok a => interp h (bind (k✝ a) k)
    | Except.error e => ret (Except.error e)) =
    bind
      (match x with
      | Except.ok a => interp h (k✝ a)
      | Except.error e => ret (Except.error e))
      fun x? =>
      match x? with
      | Except.error e => ret (Except.error e)
      | Except.ok x => interp h (k x)
Tactic:
cases x <;> simp [ih]
Proof state after:
no goals
Theorem: Fitree.interpExcept_bind
Proof state before:
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (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
        | Except.error ε_1 => ret (Except.error ε_1)
        | Except.ok x => interp h (k x)
α : Sort ?u.50273
β : Sort ?u.50274
f g : α → β
x y : α
h₁ : f = g
h₂ : x = y
⊢ f x = g y
Tactic:
simp [h₁, h₂]
Proof state after:
no goals
Theorem: double_transpose_correct
Proof state before:
⊢ ∀ (t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
    run_toy (toy_semantics_region double_transpose)
        (SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })]) =
      Fitree.ret
        ((),
          SSAEnv.One
            [(SSAVal.SSAVal "t1",
                { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 }),
              (SSAVal.SSAVal "t2",
                { fst := builtin.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32, snd := transpose t1 }),
              (SSAVal.SSAVal "t3",
                { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })])
Tactic:
intros t1
Proof state after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ run_toy (toy_semantics_region double_transpose)
      (SSAEnv.One
        [(SSAVal.SSAVal "t1",
            { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })]) =
    Fitree.ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := builtin.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32, snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })])
Theorem: double_transpose_correct
Proof state before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ (Fitree.bind
      (ToyOp.handle (RankedTensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32))
        (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 t1))
      fun x =>
      Fitree.bind
        (ToyOp.handle (RankedTensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32))
          (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x))
        fun x_1 =>
        Fitree.ret
          ((),
            SSAEnv.One
              [(SSAVal.SSAVal "t1",
                  { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                    snd := t1 }),
                (SSAVal.SSAVal "t2",
                  {
                    fst :=
                      MLIRType.extended
                        (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)),
                    snd := x }),
                (SSAVal.SSAVal "t3",
                  {
                    fst :=
                      MLIRType.extended
                        (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)),
                    snd := x_1 })])) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])
Tactic:
simp_itree
Proof state after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)),
          snd := transpose (transpose t1) })] =
    [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 })]
Theorem: double_transpose_correct
Proof state before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)),
          snd := transpose (transpose t1) })] =
    [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 })]
Tactic:
rw [transpose_involutive]
Proof state after:
no goals
Theorem: interpUB_bind
Proof state before:
T R : Type
t : Fitree UBE T
k : T → Fitree UBE R
⊢ interpUB (Fitree.bind t k) =
    Fitree.bind (interpUB t) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => interpUB (k x)
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih =>
    simp [interpUB, Fitree.interpExcept] at *
    simp [Fitree.interp, Fitree.bind, Bind.bind]
    simp [ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
    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: interpUB_bind
Proof state before:
case Ret
T R : Type
k : T → Fitree UBE R
r✝ : T
⊢ interpUB (Fitree.bind (Fitree.Ret r✝) k) =
    Fitree.bind (interpUB (Fitree.Ret r✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => interpUB (k x)
Tactic:
rfl
Proof state after:
no goals