internlm/Lean-Github huggingface dataset:
Theorem: interpUB'_bind
Proof state before:
case Vis.a
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝) =
    Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝)

case Vis.a
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (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 => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    fun x =>
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Tactic:
rfl
Proof state after:
case Vis.a
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (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 => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    fun x =>
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Theorem: interpUB'_bind
Proof state before:
case Vis.a
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (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 => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    fun x =>
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Tactic:
funext x
Proof state after:
case Vis.a.h
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Except String T✝
⊢ (match x with
    | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k)
    | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Theorem: interpUB'_bind
Proof state before:
case Vis.a.h
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Except String T✝
⊢ (match x with
    | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k)
    | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Tactic:
cases x <;> simp [ih]
Proof state after:
no goals
Theorem: interpUB'_bind
Proof state before:
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
α : Sort ?u.10648
β : Sort ?u.10649
f g : α → β
x y : α
h₁ : f = g
h₂ : x = y
⊢ f x = g y
Tactic:
simp [h₁, h₂]
Proof state after:
no goals
Theorem: MLIR.AST.AttrDict.find_none
Proof state before:
α σ : Type
ε : σ → Type
n' : String
δ : Dialect α σ ε
⊢ find (mk []) n' = none
Tactic:
simp [AttrDict.find, List.find?]
Proof state after:
no goals
Theorem: MLIR.AST.AttrDict.find_next
Proof state before:
α σ : Type
ε : σ → Type
n n' : String
δ : Dialect α σ ε
v : AttrValue δ
l : List (AttrEntry δ)
⊢ find (mk (AttrEntry.mk n v :: l)) n' = if (n == n') = true then some v else find (mk l) n'
Tactic:
cases H: n == n' <;>
simp [AttrDict.find, List.find?, AttrEntry.key, AttrEntry.value, H]
Proof state after:
no goals
Theorem: Tensor.eq_of_fields_eq
Proof state before:
τ : MLIRTy
t₁ t₂ : Tensor τ
⊢ t₁.shape = t₂.shape → t₁.data = t₂.data → t₁ = t₂
Tactic:
intros h_shape h_data
Proof state after:
τ : MLIRTy
t₁ t₂ : Tensor τ
h_shape : t₁.shape = t₂.shape
h_data : t₁.data = t₂.data
⊢ t₁ = t₂
Theorem: Tensor.eq_of_fields_eq
Proof state before:
τ : MLIRTy
t₁ t₂ : Tensor τ
h_shape : t₁.shape = t₂.shape
h_data : t₁.data = t₂.data
⊢ t₁ = t₂
Tactic:
cases t₁
Proof state after:
case mk
τ : MLIRTy
t₂ : Tensor τ
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape = t₂.shape
h_data : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data = t₂.data
⊢ { shape := shape✝, data := data✝, h_data_size := h_data_size✝ } = t₂
Theorem: Tensor.eq_of_fields_eq
Proof state before:
case mk
τ : MLIRTy
t₂ : Tensor τ
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape = t₂.shape
h_data : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data = t₂.data
⊢ { shape := shape✝, data := data✝, h_data_size := h_data_size✝ } = t₂
Tactic:
cases t₂
Proof state after:
case mk.mk
τ : MLIRTy
shape✝¹ : List ℕ
data✝¹ : List (MLIRType.eval τ)
h_data_size✝¹ : List.length data✝¹ = shapeProd shape✝¹
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.shape =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape
h_data :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.data =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data
⊢ { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ } =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }
Theorem: Tensor.eq_of_fields_eq
Proof state before:
case mk.mk
τ : MLIRTy
shape✝¹ : List ℕ
data✝¹ : List (MLIRType.eval τ)
h_data_size✝¹ : List.length data✝¹ = shapeProd shape✝¹
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.shape =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape
h_data :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.data =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data
⊢ { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ } =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }
Tactic:
simp at *
Proof state after:
case mk.mk
τ : MLIRTy
shape✝¹ : List ℕ
data✝¹ : List (MLIRType.eval τ)
h_data_size✝¹ : List.length data✝¹ = shapeProd shape✝¹
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape : shape✝¹ = shape✝
h_data : data✝¹ = data✝
⊢ shape✝¹ = shape✝ ∧ data✝¹ = data✝
Theorem: Tensor.eq_of_fields_eq
Proof state before:
case mk.mk
τ : MLIRTy
shape✝¹ : List ℕ
data✝¹ : List (MLIRType.eval τ)
h_data_size✝¹ : List.length data✝¹ = shapeProd shape✝¹
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape : shape✝¹ = shape✝
h_data : data✝¹ = data✝
⊢ shape✝¹ = shape✝ ∧ data✝¹ = data✝
Tactic:
trivial
Proof state after:
no goals
Theorem: Tensor.map_shape
Proof state before:
σ τ : MLIRTy
v : Tensor σ
f : MLIRType.eval σ → MLIRType.eval τ
⊢ v.shape = (map v f).shape
Tactic:
simp [Tensor.map]
Proof state after:
no goals
Theorem: arg_equal_implies_fn_equal
Proof state before:
α β : Type
x y : α
f : α → β
EQ : x = y
⊢ f x = f y
Tactic:
simp [EQ]
Proof state after:
no goals
Theorem: arg_equal_implies_fn_equal_2
Proof state before:
α β γ : Type
a a' : α
b b' : β
f : α → β → γ
EQα : a = a'
EQβ : b = b'
⊢ f a b = f a' b'
Tactic:
simp [EQα, EQβ]
Proof state after:
no goals
Theorem: RankedTensor.eq_of_fields_eq
Proof state before:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
⊢ t₁.toTensor.shape = t₂.toTensor.shape → t₁.toTensor.data = t₂.toTensor.data → t₁ = t₂
Tactic:
intros h_shape h_data
Proof state after:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
⊢ t₁ = t₂
Theorem: RankedTensor.eq_of_fields_eq
Proof state before:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
⊢ t₁ = t₂
Tactic:
suffices t₁.toTensor = t₂.toTensor by
  cases t₁; cases t₂; simp at *; trivial
Proof state after:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
⊢ t₁.toTensor = t₂.toTensor
Theorem: RankedTensor.eq_of_fields_eq
Proof state before:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
⊢ t₁.toTensor = t₂.toTensor
Tactic:
apply Tensor.eq_of_fields_eq <;> trivial
Proof state after:
no goals
Theorem: RankedTensor.eq_of_fields_eq
Proof state before:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
this : t₁.toTensor = t₂.toTensor
⊢ t₁ = t₂
Tactic:
cases t₁
Proof state after:
case mk
τ : DimList
D : MLIRTy
t₂ : RankedTensor τ D
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape = t₂.toTensor.shape
h_data : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data = t₂.toTensor.data
this : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor = t₂.toTensor
⊢ { toTensor := toTensor✝, h_refines := h_refines✝ } = t₂
Theorem: RankedTensor.eq_of_fields_eq
Proof state before:
case mk
τ : DimList
D : MLIRTy
t₂ : RankedTensor τ D
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape = t₂.toTensor.shape
h_data : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data = t₂.toTensor.data
this : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor = t₂.toTensor
⊢ { toTensor := toTensor✝, h_refines := h_refines✝ } = t₂
Tactic:
cases t₂
Proof state after:
case mk.mk
τ : DimList
D : MLIRTy
toTensor✝¹ : Tensor D
h_refines✝¹ : DimList.shapeRefines toTensor✝¹.shape τ = true
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.shape =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape
h_data :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.data =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data
this :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor
⊢ { toTensor := toTensor✝¹, h_refines := h_refines✝¹ } = { toTensor := toTensor✝, h_refines := h_refines✝ }
Theorem: RankedTensor.eq_of_fields_eq
Proof state before:
case mk.mk
τ : DimList
D : MLIRTy
toTensor✝¹ : Tensor D
h_refines✝¹ : DimList.shapeRefines toTensor✝¹.shape τ = true
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.shape =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape
h_data :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.data =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data
this :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor
⊢ { toTensor := toTensor✝¹, h_refines := h_refines✝¹ } = { toTensor := toTensor✝, h_refines := h_refines✝ }
Tactic:
simp at *
Proof state after:
case mk.mk
τ : DimList
D : MLIRTy
toTensor✝¹ : Tensor D
h_refines✝¹ : DimList.shapeRefines toTensor✝¹.shape τ = true
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : toTensor✝¹.shape = toTensor✝.shape
h_data : toTensor✝¹.data = toTensor✝.data
this : toTensor✝¹ = toTensor✝
⊢ toTensor✝¹ = toTensor✝
Theorem: RankedTensor.eq_of_fields_eq
Proof state before:
case mk.mk
τ : DimList
D : MLIRTy
toTensor✝¹ : Tensor D
h_refines✝¹ : DimList.shapeRefines toTensor✝¹.shape τ = true
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : toTensor✝¹.shape = toTensor✝.shape
h_data : toTensor✝¹.data = toTensor✝.data
this : toTensor✝¹ = toTensor✝
⊢ toTensor✝¹ = toTensor✝
Tactic:
trivial
Proof state after:
no goals
Theorem: reshape_self
Proof state before:
τ : MLIRTy
D : DimList
H₁ H₂ : known D = true
Hprod : prod D = prod D
t : RankedTensor D τ
⊢ reshape D H₁ H₂ Hprod t = t
Tactic:
simp [reshape, dim_known_project_eq H₁ t.h_refines]
Proof state after:
no goals
Theorem: Vector.eq_of_fields_eq
Proof state before:
τ fixed : List ℕ
scalable : MLIRTy
v₁ v₂ : Vector τ fixed scalable
⊢ v₁.scale = v₂.scale → v₁.data = v₂.data → v₁ = v₂
Tactic:
intros h_scale h_data
Proof state after:
τ fixed : List ℕ
scalable : MLIRTy
v₁ v₂ : Vector τ fixed scalable
h_scale : v₁.scale = v₂.scale
h_data : v₁.data = v₂.data
⊢ v₁ = v₂
Theorem: Vector.eq_of_fields_eq
Proof state before:
τ fixed : List ℕ
scalable : MLIRTy
v₁ v₂ : Vector τ fixed scalable
h_scale : v₁.scale = v₂.scale
h_data : v₁.data = v₂.data
⊢ v₁ = v₂
Tactic:
cases v₁
Proof state after:
case mk
τ fixed : List ℕ
scalable : MLIRTy
v₂ : Vector τ fixed scalable
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale = v₂.scale
h_data : { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data = v₂.data
⊢ { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ } = v₂
Theorem: Vector.eq_of_fields_eq
Proof state before:
case mk
τ fixed : List ℕ
scalable : MLIRTy
v₂ : Vector τ fixed scalable
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale = v₂.scale
h_data : { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data = v₂.data
⊢ { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ } = v₂
Tactic:
cases v₂
Proof state after:
case mk.mk
τ fixed : List ℕ
scalable : MLIRTy
scale✝¹ : List ℕ
data✝¹ : List (MLIRType.eval scalable)
h_scale_size✝¹ : List.length scale✝¹ = List.length fixed
h_data_size✝¹ : List.length data✝¹ = size τ fixed scale✝¹ h_scale_size✝¹
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.scale =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale
h_data :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.data =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data
⊢ { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ } =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }
Theorem: Vector.eq_of_fields_eq
Proof state before:
case mk.mk
τ fixed : List ℕ
scalable : MLIRTy
scale✝¹ : List ℕ
data✝¹ : List (MLIRType.eval scalable)
h_scale_size✝¹ : List.length scale✝¹ = List.length fixed
h_data_size✝¹ : List.length data✝¹ = size τ fixed scale✝¹ h_scale_size✝¹
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.scale =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale
h_data :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.data =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data
⊢ { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ } =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }
Tactic:
simp at *
Proof state after:
case mk.mk
τ fixed : List ℕ
scalable : MLIRTy
scale✝¹ : List ℕ
data✝¹ : List (MLIRType.eval scalable)
h_scale_size✝¹ : List.length scale✝¹ = List.length fixed
h_data_size✝¹ : List.length data✝¹ = size τ fixed scale✝¹ h_scale_size✝¹
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale : scale✝¹ = scale✝
h_data : data✝¹ = data✝
⊢ scale✝¹ = scale✝ ∧ data✝¹ = data✝
Theorem: Vector.eq_of_fields_eq
Proof state before:
case mk.mk
τ fixed : List ℕ
scalable : MLIRTy
scale✝¹ : List ℕ
data✝¹ : List (MLIRType.eval scalable)
h_scale_size✝¹ : List.length scale✝¹ = List.length fixed
h_data_size✝¹ : List.length data✝¹ = size τ fixed scale✝¹ h_scale_size✝¹
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale : scale✝¹ = scale✝
h_data : data✝¹ = data✝
⊢ scale✝¹ = scale✝ ∧ data✝¹ = data✝
Tactic:
trivial
Proof state after:
no goals
Theorem: SSAScope.equiv_refl
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope : SSAScope δ
⊢ equiv scope scope
Tactic:
intros name τ
Proof state after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope : SSAScope δ
name : SSAVal
τ : MLIRType δ
⊢ get name scope τ = get name scope τ
Theorem: SSAScope.equiv_refl
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope : SSAScope δ
name : SSAVal
τ : MLIRType δ
⊢ get name scope τ = get name scope τ
Tactic:
rfl
Proof state after:
no goals
Theorem: SSAScope.equiv_symm
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
⊢ equiv scope scope' → equiv scope' scope
Tactic:
intros H name τ
Proof state after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
H : equiv scope scope'
name : SSAVal
τ : MLIRType δ
⊢ get name scope' τ = get name scope τ
Theorem: SSAScope.equiv_symm
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
H : equiv scope scope'
name : SSAVal
τ : MLIRType δ
⊢ get name scope' τ = get name scope τ
Tactic:
specialize H name τ
Proof state after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
name : SSAVal
τ : MLIRType δ
H : get name scope τ = get name scope' τ
⊢ get name scope' τ = get name scope τ
Theorem: SSAScope.equiv_symm
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope scope' : SSAScope δ
name : SSAVal
τ : MLIRType δ
H : get name scope τ = get name scope' τ
⊢ get name scope' τ = get name scope τ
Tactic:
simp [H]
Proof state after:
no goals
Theorem: SSAScope.equiv_trans
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ : SSAScope δ
⊢ equiv scope₁ scope₂ → ∀ ⦃scope₃ : SSAScope δ⦄, equiv scope₂ scope₃ → equiv scope₁ scope₃
Tactic:
intros H1 scope₃ H2 name τ
Proof state after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ : SSAScope δ
H1 : equiv scope₁ scope₂
scope₃ : SSAScope δ
H2 : equiv scope₂ scope₃
name : SSAVal
τ : MLIRType δ
⊢ get name scope₁ τ = get name scope₃ τ