Theorem: denoteOpArgs_set_commutes (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
args : List (TypedSSAVal Δ)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ args env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all args fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ args (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
induction args
State after:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ [] env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)

case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head✝ : TypedSSAVal Δ
tail✝ : List (TypedSSAVal Δ)
tail_ih✝ :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail✝ env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail✝ fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail✝ (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ (head✝ :: tail✝) env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all (head✝ :: tail✝) fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ (head✝ :: tail✝) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ [] env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
case nil =>
  intros env r resEnv H
  simp [denoteOpArgs] at *
  simp_monad at *
  cases H; subst r env; simp
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ (head :: tail) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
case cons head tail HInd =>
  intros env r resEnv H name Hname τ v
  simp [denoteOpArgs]; simp [denoteOpArgs] at H
  have ⟨headName, headτ⟩ := head
  simp_monad at *
  cases Hhead: (TopM.get headτ headName env)
  case error _ =>
    rw [Hhead] at H; contradiction
  case ok headRes =>
    rw [Hhead] at H
    simp [List.all, List.foldr] at Hname
    have ⟨Hname_head, _⟩ := Hname
    rw [TopM.get_env_set_commutes Hhead Hname_head]
    simp at *
    split at H <;> try contradiction
    case h_2 rTail Htail =>
    have ⟨rTailRes, rTailEnv⟩ := rTail
    simp at H; have ⟨_, _⟩ := H; subst r resEnv
    simp [denoteOpArgs] at *
    simp [bind, StateT.bind, Except.bind, pure, StateT.pure, Except.pure] at HInd
    rw [HInd] <;> assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ [] env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
intros env r resEnv H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, resEnv)
⊢ ∀ ⦃name : SSAVal⦄,
    (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
      ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
        denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, resEnv)
⊢ ∀ ⦃name : SSAVal⦄,
    (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
      ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
        denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp [denoteOpArgs] at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : pure [] env = Except.ok (r, resEnv)
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    pure [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : pure [] env = Except.ok (r, resEnv)
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    pure [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : [] = r ∧ env = resEnv
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = r ∧ SSAEnv.set name τ v env = SSAEnv.set name τ v resEnv

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : [] = r ∧ env = resEnv
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = r ∧ SSAEnv.set name τ v env = SSAEnv.set name τ v resEnv
Tactic:
cases H
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
left✝ : [] = r
right✝ : env = resEnv
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = r ∧ SSAEnv.set name τ v env = SSAEnv.set name τ v resEnv

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
left✝ : [] = r
right✝ : env = resEnv
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = r ∧ SSAEnv.set name τ v env = SSAEnv.set name τ v resEnv
Tactic:
subst r env
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
resEnv : SSAEnv Δ
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = [] ∧ SSAEnv.set name τ v resEnv = SSAEnv.set name τ v resEnv

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
resEnv : SSAEnv Δ
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = [] ∧ SSAEnv.set name τ v resEnv = SSAEnv.set name τ v resEnv
Tactic:
simp
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ (head :: tail) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
intros env r resEnv H name Hname τ v
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv)
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
⊢ denoteOpArgs Δ (head :: tail) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv)
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
⊢ denoteOpArgs Δ (head :: tail) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp [denoteOpArgs]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv)
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
⊢ bind (TopM.get head.snd head.fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := head.snd, snd := x } :: __do_lift))
      (SSAEnv.set name τ v env) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv)
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
⊢ bind (TopM.get head.snd head.fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := head.snd, snd := x } :: __do_lift))
      (SSAEnv.set name τ v env) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp [denoteOpArgs] at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
H :
  bind (TopM.get head.snd head.fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := head.snd, snd := x } :: __do_lift))
      env =
    Except.ok (r, resEnv)
⊢ bind (TopM.get head.snd head.fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := head.snd, snd := x } :: __do_lift))
      (SSAEnv.set name τ v env) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
H :
  bind (TopM.get head.snd head.fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := head.snd, snd := x } :: __do_lift))
      env =
    Except.ok (r, resEnv)
⊢ bind (TopM.get head.snd head.fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := head.snd, snd := x } :: __do_lift))
      (SSAEnv.set name τ v env) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
have ⟨headName, headτ⟩ := head
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
Hname : (List.all ((headName, headτ) :: tail) fun arg => decide (name ≠ arg.fst)) = true
H :
  bind (TopM.get (headName, headτ).snd (headName, headτ).fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := (headName, headτ).snd, snd := x } :: __do_lift))
      env =
    Except.ok (r, resEnv)
⊢ bind (TopM.get (headName, headτ).snd (headName, headτ).fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := (headName, headτ).snd, snd := x } :: __do_lift))
      (SSAEnv.set name τ v env) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
Hname : (List.all ((headName, headτ) :: tail) fun arg => decide (name ≠ arg.fst)) = true
H :
  bind (TopM.get (headName, headτ).snd (headName, headτ).fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := (headName, headτ).snd, snd := x } :: __do_lift))
      env =
    Except.ok (r, resEnv)
⊢ bind (TopM.get (headName, headτ).snd (headName, headτ).fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := (headName, headτ).snd, snd := x } :: __do_lift))
      (SSAEnv.set name τ v env) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
cases Hhead: (TopM.get headτ headName env)
State after:
case error
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
a✝ : String × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.error a✝
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

case ok
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
a✝ : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok a✝
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
a✝ : String × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.error a✝
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
case error _ =>
  rw [Hhead] at H; contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
case ok headRes =>
  rw [Hhead] at H
  simp [List.all, List.foldr] at Hname
  have ⟨Hname_head, _⟩ := Hname
  rw [TopM.get_env_set_commutes Hhead Hname_head]
  simp at *
  split at H <;> try contradiction
  case h_2 rTail Htail =>
  have ⟨rTailRes, rTailEnv⟩ := rTail
  simp at H; have ⟨_, _⟩ := H; subst r resEnv
  simp [denoteOpArgs] at *
  simp [bind, StateT.bind, Except.bind, pure, StateT.pure, Except.pure] at HInd
  rw [HInd] <;> assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
a✝ : String × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.error a✝
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
rw [Hhead] at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
a✝ : String × SSAEnv Δ
H :
  (match Except.error a✝ with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.error a✝
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
a✝ : String × SSAEnv Δ
H :
  (match Except.error a✝ with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.error a✝
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
rw [Hhead] at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
H :
  (match Except.ok headRes with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.ok headRes
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
H :
  (match Except.ok headRes with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.ok headRes
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
have ⟨Hname_head, _⟩ := Hname
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
H :
  (match Except.ok headRes with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
H :
  (match Except.ok headRes with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v env) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
rw [TopM.get_env_set_commutes Hhead Hname_head]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
H :
  (match Except.ok headRes with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
⊢ (match Except.ok (headRes.fst, SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
H :
  (match Except.ok headRes with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
⊢ (match Except.ok (headRes.fst, SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
H :
  (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail headRes.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
H :
  (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail headRes.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, resEnv)
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
split at H <;> try contradiction
State after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
v✝ : List (TypedArg Δ) × SSAEnv Δ
heq✝ :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok v✝
H : Except.ok ({ fst := headτ, snd := headRes.fst } :: v✝.fst, v✝.snd) = Except.ok (r, resEnv)
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok rTail
H : Except.ok ({ fst := headτ, snd := headRes.fst } :: rTail.fst, rTail.snd) = Except.ok (r, resEnv)
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
case h_2 rTail Htail =>
have ⟨rTailRes, rTailEnv⟩ := rTail
simp at H; have ⟨_, _⟩ := H; subst r resEnv
simp [denoteOpArgs] at *
simp [bind, StateT.bind, Except.bind, pure, StateT.pure, Except.pure] at HInd
rw [HInd] <;> assumption
State after:
no goals

State before:
case h_1
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
err✝ : String × SSAEnv Δ
heq✝ :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.error err✝
H : Except.error err✝ = Except.ok (r, resEnv)
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok rTail
H : Except.ok ({ fst := headτ, snd := headRes.fst } :: rTail.fst, rTail.snd) = Except.ok (r, resEnv)
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
have ⟨rTailRes, rTailEnv⟩ := rTail
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H :
  Except.ok ({ fst := headτ, snd := headRes.fst } :: (rTailRes, rTailEnv).fst, (rTailRes, rTailEnv).snd) =
    Except.ok (r, resEnv)
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H :
  Except.ok ({ fst := headτ, snd := headRes.fst } :: (rTailRes, rTailEnv).fst, (rTailRes, rTailEnv).snd) =
    Except.ok (r, resEnv)
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : { fst := headτ, snd := headRes.fst } :: rTailRes = r ∧ rTailEnv = resEnv
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : { fst := headτ, snd := headRes.fst } :: rTailRes = r ∧ rTailEnv = resEnv
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
have ⟨_, _⟩ := H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝¹ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : { fst := headτ, snd := headRes.fst } :: rTailRes = r ∧ rTailEnv = resEnv
left✝ : { fst := headτ, snd := headRes.fst } :: rTailRes = r
right✝ : rTailEnv = resEnv
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝¹ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : { fst := headτ, snd := headRes.fst } :: rTailRes = r ∧ rTailEnv = resEnv
left✝ : { fst := headτ, snd := headRes.fst } :: rTailRes = r
right✝ : rTailEnv = resEnv
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
subst r resEnv
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H :
  { fst := headτ, snd := headRes.fst } :: rTailRes = { fst := headτ, snd := headRes.fst } :: rTailRes ∧
    rTailEnv = rTailEnv
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headRes.fst } :: rTailRes, SSAEnv.set name τ v rTailEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H :
  { fst := headτ, snd := headRes.fst } :: rTailRes = { fst := headτ, snd := headRes.fst } :: rTailRes ∧
    rTailEnv = rTailEnv
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headRes.fst } :: rTailRes, SSAEnv.set name τ v rTailEnv)
Tactic:
simp [denoteOpArgs] at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            mapM
                (fun x => do
                  let __do_lift ← TopM.get x.snd x.fst
                  pure { fst := x.snd, snd := __do_lift })
                tail (SSAEnv.set name τ v env) =
              Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : True
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headRes.fst } :: rTailRes, SSAEnv.set name τ v rTailEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            mapM
                (fun x => do
                  let __do_lift ← TopM.get x.snd x.fst
                  pure { fst := x.snd, snd := __do_lift })
                tail (SSAEnv.set name τ v env) =
              Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : True
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headRes.fst } :: rTailRes, SSAEnv.set name τ v rTailEnv)
Tactic:
simp [bind, StateT.bind, Except.bind, pure, StateT.pure, Except.pure] at HInd
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail env =
        Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            mapM
                (fun x s =>
                  match TopM.get x.snd x.fst s with
                  | Except.error err => Except.error err
                  | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
                tail (SSAEnv.set name τ v env) =
              Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : True
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headRes.fst } :: rTailRes, SSAEnv.set name τ v rTailEnv)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail env =
        Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            mapM
                (fun x s =>
                  match TopM.get x.snd x.fst s with
                  | Except.error err => Except.error err
                  | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
                tail (SSAEnv.set name τ v env) =
              Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : True
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headRes.fst } :: rTailRes, SSAEnv.set name τ v rTailEnv)
Tactic:
rw [HInd] <;> assumption
State after:
no goals