Theorem: SSAScope.set_commutes (MLIR/Semantics/SSAEnv.lean)

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
⊢ v' ≠ v →
    ∀ ⦃scope : SSAScope δ⦄ ⦃τ τ' : MLIRType δ⦄ ⦃val : MLIRType.eval τ⦄ ⦃val' : MLIRType.eval τ'⦄,
      equiv (set v τ val (set v' τ' val' scope)) (set v' τ' val' (set v τ val scope))
Tactic:
intros Hne scope τ τ' val val'
State after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv (set v τ val (set v' τ' val' scope)) (set v' τ' val' (set v τ val scope))

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv (set v τ val (set v' τ' val' scope)) (set v' τ' val' (set v τ val scope))
Tactic:
induction scope with
| nil =>
  simp; simp [Hne, Hne.symm]
  simp [equiv]; intros name τ''
  byCases Hv: v' = name
  byCases Hτ: τ' = τ'' <;> simp [Hne.symm]
| cons head tail Hind =>
  simp [equiv] at *
  intros name; specialize Hind name
  simp at *
  byCases Hv': head.fst = v' <;> simp [Hne]
  byCases Hv: head.fst = v <;> simp [Hv']
  byCases Hname: head.fst = name <;> assumption
State after:
no goals

State before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv (set v τ val (set v' τ' val' [])) (set v' τ' val' (set v τ val []))
Tactic:
simp
State after:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv
    (if v' = v then [(v', { fst := τ, snd := val })]
    else [(v', { fst := τ', snd := val' }), (v, { fst := τ, snd := val })])
    (if v = v' then [(v, { fst := τ', snd := val' })]
    else [(v, { fst := τ, snd := val }), (v', { fst := τ', snd := val' })])

State before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv
    (if v' = v then [(v', { fst := τ, snd := val })]
    else [(v', { fst := τ', snd := val' }), (v, { fst := τ, snd := val })])
    (if v = v' then [(v, { fst := τ', snd := val' })]
    else [(v, { fst := τ, snd := val }), (v', { fst := τ', snd := val' })])
Tactic:
simp [Hne, Hne.symm]
State after:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv [(v', { fst := τ', snd := val' }), (v, { fst := τ, snd := val })]
    [(v, { fst := τ, snd := val }), (v', { fst := τ', snd := val' })]

State before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv [(v', { fst := τ', snd := val' }), (v, { fst := τ, snd := val })]
    [(v, { fst := τ, snd := val }), (v', { fst := τ', snd := val' })]
Tactic:
simp [equiv]
State after:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ ∀ (name : SSAVal) (τ_1 : MLIRType δ),
    (if v' = name then
        if h : τ' = τ_1 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 τ_1 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
        if v = name then
          if h : τ = τ_1 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 τ_1 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 none) =
      if v = name then
        if h : τ = τ_1 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 τ_1 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
        if v' = name then
          if h : τ' = τ_1 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 τ_1 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 none

State before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ ∀ (name : SSAVal) (τ_1 : MLIRType δ),
    (if v' = name then
        if h : τ' = τ_1 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 τ_1 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
        if v = name then
          if h : τ = τ_1 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 τ_1 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 none) =
      if v = name then
        if h : τ = τ_1 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 τ_1 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
        if v' = name then
          if h : τ' = τ_1 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 τ_1 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 none
Tactic:
intros name τ''
State after:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
name : SSAVal
τ'' : MLIRType δ
⊢ (if v' = name 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
      if v = name 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 none) =
    if v = name 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
      if v' = name 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 none

State before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
name : SSAVal
τ'' : MLIRType δ
⊢ (if v' = name 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
      if v = name 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 none) =
    if v = name 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
      if v' = name 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 none
Tactic:
byCases Hv: v' = name
State after:
case nil.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
name : SSAVal
τ'' : MLIRType δ
Hne : name ≠ 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)
          val')
    else none) =
    if v = name 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
      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

State before:
case nil.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
name : SSAVal
τ'' : MLIRType δ
Hne : name ≠ 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)
          val')
    else none) =
    if v = name 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
      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:
byCases Hτ: τ' = τ'' <;> simp [Hne.symm]
State after:
no goals

State before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind : equiv (set v τ val (set v' τ' val' tail)) (set v' τ' val' (set v τ val tail))
⊢ equiv (set v τ val (set v' τ' val' (head :: tail))) (set v' τ' val' (set v τ val (head :: tail)))
Tactic:
simp [equiv] at *
State after:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind :
  ∀ (name : SSAVal) (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
⊢ ∀ (name : SSAVal) (τ_1 : MLIRType δ),
    get name
        (set v τ val
          (if head.fst = v' then (head.fst, { fst := τ', snd := val' }) :: tail else head :: set v' τ' val' tail))
        τ_1 =
      get name
        (set v' τ' val'
          (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail))
        τ_1

State before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind :
  ∀ (name : SSAVal) (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
⊢ ∀ (name : SSAVal) (τ_1 : MLIRType δ),
    get name
        (set v τ val
          (if head.fst = v' then (head.fst, { fst := τ', snd := val' }) :: tail else head :: set v' τ' val' tail))
        τ_1 =
      get name
        (set v' τ' val'
          (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail))
        τ_1
Tactic:
intros name
State after:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind :
  ∀ (name : SSAVal) (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
name : SSAVal
⊢ ∀ (τ_1 : MLIRType δ),
    get name
        (set v τ val
          (if head.fst = v' then (head.fst, { fst := τ', snd := val' }) :: tail else head :: set v' τ' val' tail))
        τ_1 =
      get name
        (set v' τ' val'
          (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail))
        τ_1

State before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind :
  ∀ (name : SSAVal) (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
name : SSAVal
⊢ ∀ (τ_1 : MLIRType δ),
    get name
        (set v τ val
          (if head.fst = v' then (head.fst, { fst := τ', snd := val' }) :: tail else head :: set v' τ' val' tail))
        τ_1 =
      get name
        (set v' τ' val'
          (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail))
        τ_1
Tactic:
specialize Hind name
State after:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
name : SSAVal
Hind :
  ∀ (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
⊢ ∀ (τ_1 : MLIRType δ),
    get name
        (set v τ val
          (if head.fst = v' then (head.fst, { fst := τ', snd := val' }) :: tail else head :: set v' τ' val' tail))
        τ_1 =
      get name
        (set v' τ' val'
          (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail))
        τ_1

State before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
name : SSAVal
Hind :
  ∀ (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
⊢ ∀ (τ_1 : MLIRType δ),
    get name
        (set v τ val
          (if head.fst = v' then (head.fst, { fst := τ', snd := val' }) :: tail else head :: set v' τ' val' tail))
        τ_1 =
      get name
        (set v' τ' val'
          (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail))
        τ_1
Tactic:
byCases Hv': head.fst = v' <;> simp [Hne]
State after:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
name : SSAVal
Hind :
  ∀ (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
Hv' : ¬head.fst = v'
⊢ ∀ (τ_1 : MLIRType δ),
    get name
        (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: set v' τ' val' tail
        else head :: set v τ val (set v' τ' val' tail))
        τ_1 =
      get name
        (set v' τ' val'
          (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail))
        τ_1

State before:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
name : SSAVal
Hind :
  ∀ (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
Hv' : ¬head.fst = v'
⊢ ∀ (τ_1 : MLIRType δ),
    get name
        (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: set v' τ' val' tail
        else head :: set v τ val (set v' τ' val' tail))
        τ_1 =
      get name
        (set v' τ' val'
          (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail))
        τ_1
Tactic:
byCases Hv: head.fst = v <;> simp [Hv']
State after:
case cons.h2.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
name : SSAVal
Hind :
  ∀ (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
Hv' : ¬head.fst = v'
Hv : ¬head.fst = v
⊢ ∀ (τ_1 : MLIRType δ),
    (if head.fst = name then
        if h : head.2.fst = τ_1 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 τ_1 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 (set v τ val (set v' τ' val' tail)) τ_1) =
      if head.fst = name then
        if h : head.2.fst = τ_1 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 τ_1 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 (set v' τ' val' (set v τ val tail)) τ_1

State before:
case cons.h2.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : ¬v' = v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
name : SSAVal
Hind :
  ∀ (τ_1 : MLIRType δ),
    get name (set v τ val (set v' τ' val' tail)) τ_1 = get name (set v' τ' val' (set v τ val tail)) τ_1
Hv' : ¬head.fst = v'
Hv : ¬head.fst = v
⊢ ∀ (τ_1 : MLIRType δ),
    (if head.fst = name then
        if h : head.2.fst = τ_1 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 τ_1 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 (set v τ val (set v' τ' val' tail)) τ_1) =
      if head.fst = name then
        if h : head.2.fst = τ_1 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 τ_1 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 (set v' τ' val' (set v τ val tail)) τ_1
Tactic:
byCases Hname: head.fst = name <;> assumption
State after:
no goals