internlm/Lean-Github huggingface dataset:
Theorem: SSAScope.getT_some_get
Proof state before:
case h1.refl
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
headName : SSAVal
HInd : getT headName tail = some { fst := τ, snd := v } → get headName tail τ = some v
headVal : MLIRType.eval τ
⊢ HEq headVal v →
    (if h : τ = τ then
        some
          (cast
            (_ :
              (match (headName, { fst := τ, snd := headVal }).2.fst 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)
            headVal)
      else none) =
      some v
Tactic:
simp
Proof state after:
no goals
Theorem: SSAScope.getT_some_get
Proof state before:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : getT name tail = some { fst := τ, snd := v } → get name tail τ = some v
Hname : ¬head.fst = name
⊢ getT name tail = some { fst := τ, snd := v } → get name tail τ = some v
Tactic:
assumption
Proof state after:
no goals
Theorem: SSAScope.get_none_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
⊢ (∀ (τ : MLIRType δ), get name scope τ = none) → getT name scope = none
Tactic:
induction scope <;> simp
Proof state after:
case cons
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head✝ : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail✝ : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : (∀ (τ : MLIRType δ), get name tail✝ τ = none) → getT name tail✝ = none
⊢ (∀ (τ : MLIRType δ),
      (if head✝.fst = name then
          if h : head✝.2.fst = τ then
            some
              (cast
                (_ :
                  (match head✝.2.fst 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)
                head✝.2.snd)
          else none
        else get name tail✝ τ) =
        none) →
    (if head✝.fst = name then some head✝.2 else getT name tail✝) = none
Theorem: SSAScope.get_none_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : (∀ (τ : MLIRType δ), get name tail τ = none) → getT name tail = none
⊢ (∀ (τ : MLIRType δ),
      (if head.fst = name then
          if h : head.2.fst = τ then
            some
              (cast
                (_ :
                  (match head.2.fst 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)
                head.2.snd)
          else none
        else get name tail τ) =
        none) →
    (if head.fst = name then some head.2 else getT name tail) = none
Tactic:
case cons head tail HInd =>
byCases Hname: head.fst = name <;> try assumption
Proof state after:
no goals
Theorem: SSAScope.get_none_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : (∀ (τ : MLIRType δ), get name tail τ = none) → getT name tail = none
⊢ (∀ (τ : MLIRType δ),
      (if head.fst = name then
          if h : head.2.fst = τ then
            some
              (cast
                (_ :
                  (match head.2.fst 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)
                head.2.snd)
          else none
        else get name tail τ) =
        none) →
    (if head.fst = name then some head.2 else getT name tail) = none
Tactic:
byCases Hname: head.fst = name <;> try assumption
Proof state after:
no goals
Theorem: SSAScope.get_none_getT
Proof state before:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : (∀ (τ : MLIRType δ), get name tail τ = none) → getT name tail = none
Hname : ¬head.fst = name
⊢ (∀ (τ : MLIRType δ), get name tail τ = none) → getT name tail = none
Tactic:
assumption
Proof state after:
no goals
Theorem: SSAScope.getT_set_ne
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
⊢ v' ≠ v → ∀ ⦃scope : SSAScope δ⦄ ⦃τ : MLIRType δ⦄ ⦃val : MLIRType.eval τ⦄, getT v (set v' τ val scope) = getT v scope
Tactic:
intros Hne scope τ val
Proof state after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v' τ val scope) = getT v scope
Theorem: SSAScope.getT_set_ne
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v' τ val scope) = getT v scope
Tactic:
induction scope with
| nil => simp [Hne]
| cons head tail =>
  simp
  byCases H: head.fst = v'
  . simp [Hne]
  . byCases H2: head.fst = v
    assumption
Proof state after:
no goals
Theorem: SSAScope.getT_set_ne
Proof state before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v' τ val []) = getT v []
Tactic:
simp [Hne]
Proof state after:
no goals
Theorem: SSAScope.getT_set_ne
Proof state before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
⊢ getT v (set v' τ val (head :: tail)) = getT v (head :: tail)
Tactic:
simp
Proof state after:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
⊢ getT v (if head.fst = v' then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v' τ val tail) =
    if head.fst = v then some head.2 else getT v tail
Theorem: SSAScope.getT_set_ne
Proof state before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
⊢ getT v (if head.fst = v' then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v' τ val tail) =
    if head.fst = v then some head.2 else getT v tail
Tactic:
byCases H: head.fst = v'
Proof state after:
case cons.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hne : head.fst ≠ v
tail_ih✝ : getT v (set head.fst τ val tail) = getT v tail
⊢ (if head.fst = v then some { fst := τ, snd := val } else getT v tail) =
    if head.fst = v then some head.2 else getT v tail

case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
H : ¬head.fst = v'
⊢ (if head.fst = v then some head.2 else getT v (set v' τ val tail)) = if head.fst = v then some head.2 else getT v tail
Theorem: SSAScope.getT_set_ne
Proof state before:
case cons.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hne : head.fst ≠ v
tail_ih✝ : getT v (set head.fst τ val tail) = getT v tail
⊢ (if head.fst = v then some { fst := τ, snd := val } else getT v tail) =
    if head.fst = v then some head.2 else getT v tail

case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
H : ¬head.fst = v'
⊢ (if head.fst = v then some head.2 else getT v (set v' τ val tail)) = if head.fst = v then some head.2 else getT v tail
Tactic:
. simp [Hne]
Proof state after:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
H : ¬head.fst = v'
⊢ (if head.fst = v then some head.2 else getT v (set v' τ val tail)) = if head.fst = v then some head.2 else getT v tail
Theorem: SSAScope.getT_set_ne
Proof state before:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
H : ¬head.fst = v'
⊢ (if head.fst = v then some head.2 else getT v (set v' τ val tail)) = if head.fst = v then some head.2 else getT v tail
Tactic:
. byCases H2: head.fst = v
  assumption
Proof state after:
no goals
Theorem: SSAScope.getT_set_eq
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
scope : SSAScope δ
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v τ val scope) = some { fst := τ, snd := val }
Tactic:
induction scope with
| nil => simp
| cons head tail =>
  simp
  byCases H: head.fst = v
  assumption
Proof state after:
no goals
Theorem: SSAScope.getT_set_eq
Proof state before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v τ val []) = some { fst := τ, snd := val }
Tactic:
simp
Proof state after:
no goals
Theorem: SSAScope.getT_set_eq
Proof state before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v τ val tail) = some { fst := τ, snd := val }
⊢ getT v (set v τ val (head :: tail)) = some { fst := τ, snd := val }
Tactic:
simp
Proof state after:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v τ val tail) = some { fst := τ, snd := val }
⊢ getT v (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail) =
    some { fst := τ, snd := val }
Theorem: SSAScope.getT_set_eq
Proof state before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v τ val tail) = some { fst := τ, snd := val }
⊢ getT v (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail) =
    some { fst := τ, snd := val }
Tactic:
byCases H: head.fst = v
Proof state after:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v τ val tail) = some { fst := τ, snd := val }
H : ¬head.fst = v
⊢ getT v (set v τ val tail) = some { fst := τ, snd := val }
Theorem: SSAScope.getT_set_eq
Proof state before:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v τ val tail) = some { fst := τ, snd := val }
H : ¬head.fst = v
⊢ getT v (set v τ val tail) = some { fst := τ, snd := val }
Tactic:
assumption
Proof state after:
no goals
Theorem: SSAScope.get_set_ne_val
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
⊢ v' ≠ v →
    ∀ ⦃scope : SSAScope δ⦄ ⦃τ τ' : MLIRType δ⦄ ⦃val : MLIRType.eval τ⦄, get v (set v' τ val scope) τ' = get v scope τ'
Tactic:
intros Hne scope τ τ' val
Proof state after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ τ' : MLIRType δ
val : MLIRType.eval τ
⊢ get v (set v' τ val scope) τ' = get v scope τ'
Theorem: SSAScope.get_set_ne_val
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ τ' : MLIRType δ
val : MLIRType.eval τ
⊢ get v (set v' τ val scope) τ' = get v scope τ'
Tactic:
induction scope with
| nil => simp [Hne]
| cons head nil =>
  simp
  byCases H: head.fst = v'
  . simp [Hne]
  . byCases H2: head.fst = v <;> try assumption
Proof state after:
no goals
Theorem: SSAScope.get_set_ne_val
Proof state before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
⊢ get v (set v' τ val []) τ' = get v [] τ'
Tactic:
simp [Hne]
Proof state after:
no goals
Theorem: SSAScope.get_set_ne_val
Proof state before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : get v (set v' τ val nil) τ' = get v nil τ'
⊢ get v (set v' τ val (head :: nil)) τ' = get v (head :: nil) τ'
Tactic:
simp
Proof state after:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : get v (set v' τ val nil) τ' = get v nil τ'
⊢ get v (if head.fst = v' then (head.fst, { fst := τ, snd := val }) :: nil else head :: set v' τ val nil) τ' =
    if head.fst = v then
      if h : head.2.fst = τ' then
        some
          (cast
            (_ :
              (match head.2.fst 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)
            head.2.snd)
      else none
    else get v nil τ'
Theorem: SSAScope.get_set_ne_val
Proof state before:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : get v (set v' τ val nil) τ' = get v nil τ'
H : ¬head.fst = v'
⊢ (if head.fst = v then
      if h : head.2.fst = τ' then
        some
          (cast
            (_ :
              (match head.2.fst 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)
            head.2.snd)
      else none
    else get v (set v' τ val nil) τ') =
    if head.fst = v then
      if h : head.2.fst = τ' then
        some
          (cast
            (_ :
              (match head.2.fst 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)
            head.2.snd)
      else none
    else get v nil τ'
Tactic:
. byCases H2: head.fst = v <;> try assumption
Proof state after:
no goals
Theorem: SSAScope.get_set_ne_val
Proof state before:
case cons.h2.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : get v (set v' τ val nil) τ' = get v nil τ'
H : ¬head.fst = v'
H2 : ¬head.fst = v
⊢ get v (set v' τ val nil) τ' = get v nil τ'
Tactic:
assumption
Proof state after:
no goals
Theorem: SSAScope.get_set_ne_type
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
⊢ τ' ≠ τ → ∀ ⦃scope : SSAScope δ⦄ ⦃v : SSAVal⦄ ⦃val : MLIRType.eval τ'⦄, get v (set v τ' val scope) τ = none
Tactic:
intros Hne scope v val
Proof state after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
scope : SSAScope δ
v : SSAVal
val : MLIRType.eval τ'
⊢ get v (set v τ' val scope) τ = none
Theorem: SSAScope.get_set_ne_type
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
scope : SSAScope δ
v : SSAVal
val : MLIRType.eval τ'
⊢ get v (set v τ' val scope) τ = none
Tactic:
induction scope with
| nil => simp [Hne]
| cons head tail Hind =>
  simp
  byCases H: head.fst = v
  . simp [Hne]
  . byCases H2: head.fst = v <;> try assumption
Proof state after:
no goals
Theorem: SSAScope.get_set_ne_type
Proof state before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
v : SSAVal
val : MLIRType.eval τ'
⊢ get v (set v τ' val []) τ = none
Tactic:
simp [Hne]
Proof state after:
no goals