internlm/Lean-Github huggingface dataset:
Theorem: SSAEnv.getT_set_ne
Proof state before:
case One
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ SSAScope.getT v (SSAScope.set v' τ val s) = SSAScope.getT v s
Tactic:
rw [SSAScope.getT_set_ne]
Proof state after:
case One.a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ v' ≠ v
Theorem: SSAEnv.getT_set_ne
Proof state before:
case One.a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ v' ≠ v
Tactic:
assumption
Proof state after:
no goals
Theorem: SSAEnv.getT_set_ne
Proof state before:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ getT v (set v' τ val (Cons head tail)) = getT v (Cons head tail)
Tactic:
simp [getT, set, HOrElse.hOrElse, OrElse.orElse, Option.orElse]
Proof state after:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ (match SSAScope.getT v (SSAScope.set v' τ val head), fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()) =
    match SSAScope.getT v head, fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()
Theorem: SSAEnv.getT_set_ne
Proof state before:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ (match SSAScope.getT v (SSAScope.set v' τ val head), fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()) =
    match SSAScope.getT v head, fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()
Tactic:
rw [SSAScope.getT_set_ne]
Proof state after:
case Cons.a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ v' ≠ v
Theorem: SSAEnv.getT_set_ne
Proof state before:
case Cons.a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ v' ≠ v
Tactic:
assumption
Proof state after:
no goals
Theorem: SSAEnv.getT_set_eq
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
env : SSAEnv δ
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v τ val env) = some { fst := τ, snd := val }
Tactic:
cases env with
| One s =>
  simp [getT, set]
  rw [SSAScope.getT_set_eq]
| Cons head tail =>
  simp [getT, set, HOrElse.hOrElse, OrElse.orElse, Option.orElse]
  simp [SSAScope.getT_set_eq]
Proof state after:
no goals
Theorem: SSAEnv.getT_set_eq
Proof state before:
case One
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ getT v (set v τ val (One s)) = some { fst := τ, snd := val }
Tactic:
simp [getT, set]
Proof state after:
case One
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ SSAScope.getT v (SSAScope.set v τ val s) = some { fst := τ, snd := val }
Theorem: SSAEnv.getT_set_eq
Proof state before:
case One
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ SSAScope.getT v (SSAScope.set v τ val s) = some { fst := τ, snd := val }
Tactic:
rw [SSAScope.getT_set_eq]
Proof state after:
no goals
Theorem: SSAEnv.getT_set_eq
Proof state before:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ getT v (set v τ val (Cons head tail)) = some { fst := τ, snd := val }
Tactic:
simp [getT, set, HOrElse.hOrElse, OrElse.orElse, Option.orElse]
Proof state after:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ (match SSAScope.getT v (SSAScope.set v τ val head), fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()) =
    some { fst := τ, snd := val }
Theorem: SSAEnv.getT_set_eq
Proof state before:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ (match SSAScope.getT v (SSAScope.set v τ val head), fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()) =
    some { fst := τ, snd := val }
Tactic:
simp [SSAScope.getT_set_eq]
Proof state after:
no goals
Theorem: SSAEnv.get_set_ne_val
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
⊢ v' ≠ v → ∀ ⦃env : SSAEnv δ⦄ ⦃τ τ' : MLIRType δ⦄ ⦃val : MLIRType.eval τ'⦄, get v τ (set v' τ' val env) = get v τ env
Tactic:
intros Hne env τ τ' val
Proof state after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ get v τ (set v' τ' val env) = get v τ env
Theorem: SSAEnv.get_set_ne_val
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ get v τ (set v' τ' val env) = get v τ env
Tactic:
simp [get]
Proof state after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ (match getT v (set v' τ' val env) with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none) =
    match getT v env with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none
Theorem: SSAEnv.get_set_ne_val
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ (match getT v (set v' τ' val env) with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none) =
    match getT v env with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none
Tactic:
rw [SSAEnv.getT_set_ne]
Proof state after:
case a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ v' ≠ v
Theorem: SSAEnv.get_set_ne_val
Proof state before:
case a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ v' ≠ v
Tactic:
assumption
Proof state after:
no goals
Theorem: SSAEnv.get_set_eq_val
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v : SSAVal
val : MLIRType.eval τ'
H' : τ' = τ
⊢ MLIRType.eval τ' = MLIRType.eval τ
Tactic:
simp [H']
Proof state after:
no goals
Theorem: SSAEnv.get_set_eq_val
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v : SSAVal
val : MLIRType.eval τ'
⊢ get v τ (set v τ' val env) =
    if H' : τ' = τ then
      some
        (cast
          (_ :
            (match τ' with
              | MLIRType.float a => Float
              | MLIRType.int signedness sz => FinInt sz
              | MLIRType.tensor1d => Tensor1D
              | MLIRType.tensor2d => Tensor2D
              | MLIRType.tensor4d => Tensor4D
              | MLIRType.index => ℤ
              | MLIRType.undefined a => Unit
              | MLIRType.extended σ => ε σ
              | MLIRType.erased => Unit) =
              match τ with
              | MLIRType.float a => Float
              | MLIRType.int signedness sz => FinInt sz
              | MLIRType.tensor1d => Tensor1D
              | MLIRType.tensor2d => Tensor2D
              | MLIRType.tensor4d => Tensor4D
              | MLIRType.index => ℤ
              | MLIRType.undefined a => Unit
              | MLIRType.extended σ => ε σ
              | MLIRType.erased => Unit)
          val)
    else none
Tactic:
simp [get, getT_set_eq]
Proof state after:
no goals
Theorem: SSAEnv.get_set
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : τ' = τ
⊢ MLIRType.eval τ' = MLIRType.eval τ
Tactic:
simp [H]
Proof state after:
no goals
Theorem: SSAEnv.get_set
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
⊢ get v τ (set v' τ' val env) =
    if v' = v then
      if H : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε σ
                | MLIRType.erased => Unit)
            val)
      else none
    else get v τ env
Tactic:
byCases H: v' = v
Proof state after:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v : SSAVal
val : MLIRType.eval τ'
⊢ get v τ (set v τ' val env) =
    if h : τ' = τ then
      some
        (cast
          (_ :
            (match τ' with
              | MLIRType.float a => Float
              | MLIRType.int signedness sz => FinInt sz
              | MLIRType.tensor1d => Tensor1D
              | MLIRType.tensor2d => Tensor2D
              | MLIRType.tensor4d => Tensor4D
              | MLIRType.index => ℤ
              | MLIRType.undefined a => Unit
              | MLIRType.extended σ => ε σ
              | MLIRType.erased => Unit) =
              match τ with
              | MLIRType.float a => Float
              | MLIRType.int signedness sz => FinInt sz
              | MLIRType.tensor1d => Tensor1D
              | MLIRType.tensor2d => Tensor2D
              | MLIRType.tensor4d => Tensor4D
              | MLIRType.index => ℤ
              | MLIRType.undefined a => Unit
              | MLIRType.extended σ => ε σ
              | MLIRType.erased => Unit)
          val)
    else none

case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : ¬v' = v
⊢ get v τ (set v' τ' val env) = get v τ env
Theorem: SSAEnv.get_set
Proof state before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v : SSAVal
val : MLIRType.eval τ'
⊢ get v τ (set v τ' val env) =
    if h : τ' = τ then
      some
        (cast
          (_ :
            (match τ' with
              | MLIRType.float a => Float
              | MLIRType.int signedness sz => FinInt sz
              | MLIRType.tensor1d => Tensor1D
              | MLIRType.tensor2d => Tensor2D
              | MLIRType.tensor4d => Tensor4D
              | MLIRType.index => ℤ
              | MLIRType.undefined a => Unit
              | MLIRType.extended σ => ε σ
              | MLIRType.erased => Unit) =
              match τ with
              | MLIRType.float a => Float
              | MLIRType.int signedness sz => FinInt sz
              | MLIRType.tensor1d => Tensor1D
              | MLIRType.tensor2d => Tensor2D
              | MLIRType.tensor4d => Tensor4D
              | MLIRType.index => ℤ
              | MLIRType.undefined a => Unit
              | MLIRType.extended σ => ε σ
              | MLIRType.erased => Unit)
          val)
    else none

case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : ¬v' = v
⊢ get v τ (set v' τ' val env) = get v τ env
Tactic:
. simp [get_set_eq_val]
Proof state after:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : ¬v' = v
⊢ get v τ (set v' τ' val env) = get v τ env
Theorem: SSAEnv.get_set
Proof state before:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : ¬v' = v
⊢ get v τ (set v' τ' val env) = get v τ env
Tactic:
. rw [get_set_ne_val]
  assumption
Proof state after:
no goals
Theorem: SSAEnv.get_set_eq
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
env : SSAEnv δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ get v τ (set v τ val env) = some val
Tactic:
simp [get, getT_set_eq]
Proof state after:
no goals
Theorem: SSAEnv.get_set_neq
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
NEQ : v' ≠ v
env : SSAEnv δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ get v τ (set v' τ val env) = get v τ env
Tactic:
simp[get]
Proof state after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
NEQ : v' ≠ v
env : SSAEnv δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ (match getT v (set v' τ val env) with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none) =
    match getT v env with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none
Theorem: SSAEnv.get_set_neq
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
NEQ : v' ≠ v
env : SSAEnv δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ (match getT v (set v' τ val env) with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none) =
    match getT v env with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none
Tactic:
rw[SSAEnv.getT_set_ne]
Proof state after:
case a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
NEQ : v' ≠ v
env : SSAEnv δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ v' ≠ v
Theorem: SSAEnv.get_set_neq
Proof state before:
case a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
NEQ : v' ≠ v
env : SSAEnv δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ v' ≠ v
Tactic:
try assumption;
Proof state after:
no goals
Theorem: SSAEnv.get_set_neq
Proof state before:
case a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
NEQ : v' ≠ v
env : SSAEnv δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ v' ≠ v
Tactic:
assumption
Proof state after:
no goals
Theorem: SSAEnv.equiv_set
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
⊢ equiv env₁ env₂ →
    ∀ ⦃name : SSAVal⦄ ⦃τ : MLIRType δ⦄ ⦃v : MLIRType.eval τ⦄, equiv (set name τ v env₁) (set name τ v env₂)
Tactic:
intros HEnv name τ v name' τ'
Proof state after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)