Theorem: SSAScope.set_commutes
Proof 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']
Proof 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