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

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOps Δ [] env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ → ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ [] env₂ = Except.ok (res, env₂')
Tactic:
intros env res env' H env₂ Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : denoteOps Δ [] env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ [] env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : denoteOps Δ [] env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ [] env₂ = Except.ok (res, env₂')
Tactic:
simp [denoteOps] at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : pure [] env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ pure [] env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : pure [] env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ pure [] env₂ = Except.ok (res, env₂')
Tactic:
simp_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : [] = res ∧ env = env'
⊢ SSAEnv.equiv env' env₂ ∧ [] = res

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : [] = res ∧ env = env'
⊢ SSAEnv.equiv env' env₂ ∧ [] = res
Tactic:
cases H
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
left✝ : [] = res
right✝ : env = env'
⊢ SSAEnv.equiv env' env₂ ∧ [] = res

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
left✝ : [] = res
right✝ : env = env'
⊢ SSAEnv.equiv env' env₂ ∧ [] = res
Tactic:
subst res env
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env' env₂
⊢ SSAEnv.equiv env' env₂ ∧ [] = []

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env' env₂
⊢ SSAEnv.equiv env' env₂ ∧ [] = []
Tactic:
constructor <;> simp
State after:
case intro.left
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env' env₂
⊢ SSAEnv.equiv env' env₂

State before:
case intro.left
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env' env₂
⊢ SSAEnv.equiv env' env₂
Tactic:
try assumption
State after:
no goals

State before:
case intro.left
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env' env₂
⊢ SSAEnv.equiv env' env₂
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOps Δ (head :: tail) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head :: tail) env₂ = Except.ok (res, env₂')
Tactic:
intros env res env' H env₂ Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : denoteOps Δ (head :: tail) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head :: tail) env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : denoteOps Δ (head :: tail) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head :: tail) env₂ = Except.ok (res, env₂')
Tactic:
unfold denoteOps at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match head :: tail with
      | [] => pure []
      | [stmt] => denoteOp Δ stmt
      | stmt :: stmts' => do
        let __discr ← denoteOp Δ stmt
        let x : TypedArgs Δ := __discr
        denoteOps Δ stmts')
      env =
    Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head :: tail) env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match head :: tail with
      | [] => pure []
      | [stmt] => denoteOp Δ stmt
      | stmt :: stmts' => do
        let __discr ← denoteOp Δ stmt
        let x : TypedArgs Δ := __discr
        denoteOps Δ stmts')
      env =
    Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head :: tail) env₂ = Except.ok (res, env₂')
Tactic:
simp_monad at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match head :: tail with
      | [] => fun s => Except.ok ([], s)
      | [stmt] => denoteOp Δ stmt
      | stmt :: stmts' => fun s =>
        match denoteOp Δ stmt s with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ stmts' v.snd)
      env =
    Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head :: tail) env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match head :: tail with
      | [] => fun s => Except.ok ([], s)
      | [stmt] => denoteOp Δ stmt
      | stmt :: stmts' => fun s =>
        match denoteOp Δ stmt s with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ stmts' v.snd)
      env =
    Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head :: tail) env₂ = Except.ok (res, env₂')
Tactic:
match TAIL: tail with
| .nil =>
  apply denoteOp_equiv <;> assumption
| .cons head2 tail2 =>
  simp [denoteOps] at *; simp_monad at *
  split at H <;> try contradiction
  case h_2 headR HHeadR =>
  have ⟨headR, headEnv⟩ := headR; simp at *
  have ⟨envHead, HenvHead, HdenoteHead⟩ := denoteOp_equiv HHeadR Henv₂
  simp [HdenoteHead]
  rw [←TAIL] at H; rw [←TAIL]
  apply denoteOps_equiv H HenvHead
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match [head] with
      | [] => fun s => Except.ok ([], s)
      | [stmt] => denoteOp Δ stmt
      | stmt :: stmts' => fun s =>
        match denoteOp Δ stmt s with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ stmts' v.snd)
      env =
    Except.ok (res, env')
TAIL : tail = []
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ [head] env₂ = Except.ok (res, env₂')
Tactic:
apply denoteOp_equiv <;> assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
H :
  (match head :: head2 :: tail2 with
      | [] => fun s => Except.ok ([], s)
      | [stmt] => denoteOp Δ stmt
      | stmt :: stmts' => fun s =>
        match denoteOp Δ stmt s with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ stmts' v.snd)
      env =
    Except.ok (res, env')
TAIL : tail = head2 :: tail2
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head :: head2 :: tail2) env₂ = Except.ok (res, env₂')
Tactic:
simp [denoteOps] at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
H :
  (match denoteOp Δ head env with
    | Except.error err => Except.error err
    | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
    Except.ok (res, env')
TAIL : tail = head2 :: tail2
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      bind (denoteOp Δ head) (fun __discr => denoteOps Δ (head2 :: tail2)) env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
H :
  (match denoteOp Δ head env with
    | Except.error err => Except.error err
    | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
    Except.ok (res, env')
TAIL : tail = head2 :: tail2
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      bind (denoteOp Δ head) (fun __discr => denoteOps Δ (head2 :: tail2)) env₂ = Except.ok (res, env₂')
Tactic:
simp_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
H :
  (match denoteOp Δ head env with
    | Except.error err => Except.error err
    | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
    Except.ok (res, env')
TAIL : tail = head2 :: tail2
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
H :
  (match denoteOp Δ head env with
    | Except.error err => Except.error err
    | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
    Except.ok (res, env')
TAIL : tail = head2 :: tail2
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')
Tactic:
split at H <;> try contradiction
State after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
v✝ : List (TypedArg Δ) × SSAEnv Δ
heq✝ : denoteOp Δ head env = Except.ok v✝
H : denoteOps Δ (head2 :: tail2) v✝.snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR : List (TypedArg Δ) × SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok headR
H : denoteOps Δ (head2 :: tail2) headR.snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')
Tactic:
case h_2 headR HHeadR =>
have ⟨headR, headEnv⟩ := headR; simp at *
have ⟨envHead, HenvHead, HdenoteHead⟩ := denoteOp_equiv HHeadR Henv₂
simp [HdenoteHead]
rw [←TAIL] at H; rw [←TAIL]
apply denoteOps_equiv H HenvHead
State after:
no goals

State before:
case h_1
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
err✝ : String × SSAEnv Δ
heq✝ : denoteOp Δ head env = Except.error err✝
H : Except.error err✝ = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')
Tactic:
contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR : List (TypedArg Δ) × SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok headR
H : denoteOps Δ (head2 :: tail2) headR.snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')
Tactic:
have ⟨headR, headEnv⟩ := headR
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ (head2 :: tail2) (headR, headEnv).snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ (head2 :: tail2) (headR, headEnv).snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')
Tactic:
simp at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ (head2 :: tail2) headEnv = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ (head2 :: tail2) headEnv = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')
Tactic:
have ⟨envHead, HenvHead, HdenoteHead⟩ := denoteOp_equiv HHeadR Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ (head2 :: tail2) headEnv = Except.ok (res, env')
envHead : SSAEnv Δ
HenvHead : SSAEnv.equiv headEnv envHead
HdenoteHead : denoteOp Δ head env₂ = Except.ok (headR, envHead)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ (head2 :: tail2) headEnv = Except.ok (res, env')
envHead : SSAEnv Δ
HenvHead : SSAEnv.equiv headEnv envHead
HdenoteHead : denoteOp Δ head env₂ = Except.ok (headR, envHead)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')
Tactic:
simp [HdenoteHead]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ (head2 :: tail2) headEnv = Except.ok (res, env')
envHead : SSAEnv Δ
HenvHead : SSAEnv.equiv headEnv envHead
HdenoteHead : denoteOp Δ head env₂ = Except.ok (headR, envHead)
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head2 :: tail2) envHead = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ (head2 :: tail2) headEnv = Except.ok (res, env')
envHead : SSAEnv Δ
HenvHead : SSAEnv.equiv headEnv envHead
HdenoteHead : denoteOp Δ head env₂ = Except.ok (headR, envHead)
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head2 :: tail2) envHead = Except.ok (res, env₂')
Tactic:
rw [←TAIL] at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ tail headEnv = Except.ok (res, env')
envHead : SSAEnv Δ
HenvHead : SSAEnv.equiv headEnv envHead
HdenoteHead : denoteOp Δ head env₂ = Except.ok (headR, envHead)
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head2 :: tail2) envHead = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ tail headEnv = Except.ok (res, env')
envHead : SSAEnv Δ
HenvHead : SSAEnv.equiv headEnv envHead
HdenoteHead : denoteOp Δ head env₂ = Except.ok (headR, envHead)
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head2 :: tail2) envHead = Except.ok (res, env₂')
Tactic:
rw [←TAIL]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ tail headEnv = Except.ok (res, env')
envHead : SSAEnv Δ
HenvHead : SSAEnv.equiv headEnv envHead
HdenoteHead : denoteOp Δ head env₂ = Except.ok (headR, envHead)
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ tail envHead = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR✝ : List (TypedArg Δ) × SSAEnv Δ
headR : List (TypedArg Δ)
headEnv : SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok (headR, headEnv)
H : denoteOps Δ tail headEnv = Except.ok (res, env')
envHead : SSAEnv Δ
HenvHead : SSAEnv.equiv headEnv envHead
HdenoteHead : denoteOp Δ head env₂ = Except.ok (headR, envHead)
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ tail envHead = Except.ok (res, env₂')
Tactic:
apply denoteOps_equiv H HenvHead
State after:
no goals