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

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
vals : List SSAVal
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
⊢ denoteTypedArgs (argsHead :: argsTail) vals env = Except.ok (res, env') →
    ∃ valHead valTail,
      vals = valHead :: valTail ∧
        TopM.set argsHead.fst valHead argsHead.snd env =
            Except.ok ((), SSAEnv.set valHead argsHead.fst argsHead.snd env) ∧
          denoteTypedArgs argsTail valTail (SSAEnv.set valHead argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
intros H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
vals : List SSAVal
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
H : denoteTypedArgs (argsHead :: argsTail) vals env = Except.ok (res, env')
⊢ ∃ valHead valTail,
    vals = valHead :: valTail ∧
      TopM.set argsHead.fst valHead argsHead.snd env =
          Except.ok ((), SSAEnv.set valHead argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set valHead argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
vals : List SSAVal
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
H : denoteTypedArgs (argsHead :: argsTail) vals env = Except.ok (res, env')
⊢ ∃ valHead valTail,
    vals = valHead :: valTail ∧
      TopM.set argsHead.fst valHead argsHead.snd env =
          Except.ok ((), SSAEnv.set valHead argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set valHead argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
simp [denoteTypedArgs] at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
vals : List SSAVal
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
H :
  (match vals with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ ∃ valHead valTail,
    vals = valHead :: valTail ∧
      TopM.set argsHead.fst valHead argsHead.snd env =
          Except.ok ((), SSAEnv.set valHead argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set valHead argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
vals : List SSAVal
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
H :
  (match vals with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ ∃ valHead valTail,
    vals = valHead :: valTail ∧
      TopM.set argsHead.fst valHead argsHead.snd env =
          Except.ok ((), SSAEnv.set valHead argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set valHead argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
cases vals <;> try contradiction
State after:
case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
head✝ : SSAVal
tail✝ : List SSAVal
H :
  (match head✝ :: tail✝ with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ ∃ valHead valTail,
    head✝ :: tail✝ = valHead :: valTail ∧
      TopM.set argsHead.fst valHead argsHead.snd env =
          Except.ok ((), SSAEnv.set valHead argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set valHead argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
H :
  (match headVal :: tailVal with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ ∃ valHead valTail,
    headVal :: tailVal = valHead :: valTail ∧
      TopM.set argsHead.fst valHead argsHead.snd env =
          Except.ok ((), SSAEnv.set valHead argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set valHead argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
case cons headVal tailVal =>
exists headVal
exists tailVal
simp_monad at *
revert H
split <;> intros H <;> try contradiction
case h_2 v Hv =>
have ⟨fst, snd⟩ := v; cases fst
case unit =>
simp_semantics_monad at *
revert Hv; split <;> intros Hv <;> try contradiction
simp at Hv; subst snd
simp [H]
State after:
no goals

State before:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
H :
  (match [] with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ ∃ valHead valTail,
    [] = valHead :: valTail ∧
      TopM.set argsHead.fst valHead argsHead.snd env =
          Except.ok ((), SSAEnv.set valHead argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set valHead argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
H :
  (match headVal :: tailVal with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ ∃ valHead valTail,
    headVal :: tailVal = valHead :: valTail ∧
      TopM.set argsHead.fst valHead argsHead.snd env =
          Except.ok ((), SSAEnv.set valHead argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set valHead argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
exists headVal
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
H :
  (match headVal :: tailVal with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ ∃ valTail,
    headVal :: tailVal = headVal :: valTail ∧
      TopM.set argsHead.fst headVal argsHead.snd env =
          Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
H :
  (match headVal :: tailVal with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ ∃ valTail,
    headVal :: tailVal = headVal :: valTail ∧
      TopM.set argsHead.fst headVal argsHead.snd env =
          Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
        denoteTypedArgs argsTail valTail (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
exists tailVal
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
H :
  (match headVal :: tailVal with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ headVal :: tailVal = headVal :: tailVal ∧
    TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
      denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
H :
  (match headVal :: tailVal with
      | [] => TopM.raiseUB "not enough names in denoteTypedArgs"
      | name :: names => do
        TopM.set argsHead.fst name argsHead.snd
        denoteTypedArgs argsTail names)
      env =
    Except.ok (res, env')
⊢ headVal :: tailVal = headVal :: tailVal ∧
    TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
      denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
simp_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
H :
  (match TopM.set argsHead.fst headVal argsHead.snd env with
    | Except.error err => Except.error err
    | Except.ok v => denoteTypedArgs argsTail tailVal v.snd) =
    Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
H :
  (match TopM.set argsHead.fst headVal argsHead.snd env with
    | Except.error err => Except.error err
    | Except.ok v => denoteTypedArgs argsTail tailVal v.snd) =
    Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
revert H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
⊢ (match TopM.set argsHead.fst headVal argsHead.snd env with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail tailVal v.snd) =
      Except.ok (res, env') →
    TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
      denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
⊢ (match TopM.set argsHead.fst headVal argsHead.snd env with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail tailVal v.snd) =
      Except.ok (res, env') →
    TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
      denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
split <;> intros H <;> try contradiction
State after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v✝ : Unit × SSAEnv δ
heq✝ : TopM.set argsHead.fst headVal argsHead.snd env = Except.ok v✝
H : denoteTypedArgs argsTail tailVal v✝.snd = Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
Hv : TopM.set argsHead.fst headVal argsHead.snd env = Except.ok v
H : denoteTypedArgs argsTail tailVal v.snd = Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
case h_2 v Hv =>
have ⟨fst, snd⟩ := v; cases fst
case unit =>
simp_semantics_monad at *
revert Hv; split <;> intros Hv <;> try contradiction
simp at Hv; subst snd
simp [H]
State after:
no goals

State before:
case h_1
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
err✝ : String × SSAEnv δ
heq✝ : TopM.set argsHead.fst headVal argsHead.snd env = Except.error err✝
H : Except.error err✝ = Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
Hv : TopM.set argsHead.fst headVal argsHead.snd env = Except.ok v
H : denoteTypedArgs argsTail tailVal v.snd = Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
have ⟨fst, snd⟩ := v
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
fst : Unit
snd : SSAEnv δ
Hv : TopM.set argsHead.fst headVal argsHead.snd env = Except.ok (fst, snd)
H : denoteTypedArgs argsTail tailVal (fst, snd).snd = Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
fst : Unit
snd : SSAEnv δ
Hv : TopM.set argsHead.fst headVal argsHead.snd env = Except.ok (fst, snd)
H : denoteTypedArgs argsTail tailVal (fst, snd).snd = Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
cases fst
State after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
Hv : TopM.set argsHead.fst headVal argsHead.snd env = Except.ok (PUnit.unit, snd)
H : denoteTypedArgs argsTail tailVal (PUnit.unit, snd).snd = Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
Hv : TopM.set argsHead.fst headVal argsHead.snd env = Except.ok (PUnit.unit, snd)
H : denoteTypedArgs argsTail tailVal (PUnit.unit, snd).snd = Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
case unit =>
simp_semantics_monad at *
revert Hv; split <;> intros Hv <;> try contradiction
simp at Hv; subst snd
simp [H]
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
Hv : TopM.set argsHead.fst headVal argsHead.snd env = Except.ok (PUnit.unit, snd)
H : denoteTypedArgs argsTail tailVal (PUnit.unit, snd).snd = Except.ok (res, env')
⊢ TopM.set argsHead.fst headVal argsHead.snd env = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
simp_semantics_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
Hv :
  (match SSAEnv.get headVal argsHead.fst env with
    | some val => Except.error ("setting to SSA value twice!", env)
    | none => Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env)) =
    Except.ok (PUnit.unit, snd)
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
⊢ (match SSAEnv.get headVal argsHead.fst env with
      | some val => Except.error ("setting to SSA value twice!", env)
      | none => Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env)) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
Hv :
  (match SSAEnv.get headVal argsHead.fst env with
    | some val => Except.error ("setting to SSA value twice!", env)
    | none => Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env)) =
    Except.ok (PUnit.unit, snd)
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
⊢ (match SSAEnv.get headVal argsHead.fst env with
      | some val => Except.error ("setting to SSA value twice!", env)
      | none => Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env)) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
revert Hv
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
⊢ (match SSAEnv.get headVal argsHead.fst env with
      | some val => Except.error ("setting to SSA value twice!", env)
      | none => Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env)) =
      Except.ok (PUnit.unit, snd) →
    (match SSAEnv.get headVal argsHead.fst env with
        | some val => Except.error ("setting to SSA value twice!", env)
        | none => Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env)) =
        Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
      denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
⊢ (match SSAEnv.get headVal argsHead.fst env with
      | some val => Except.error ("setting to SSA value twice!", env)
      | none => Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env)) =
      Except.ok (PUnit.unit, snd) →
    (match SSAEnv.get headVal argsHead.fst env with
        | some val => Except.error ("setting to SSA value twice!", env)
        | none => Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env)) =
        Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
      denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
split <;> intros Hv <;> try contradiction
State after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝¹ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
x✝ : Option (MLIRType.eval argsHead.fst)
heq✝ : SSAEnv.get headVal argsHead.fst env = none
Hv : Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok (PUnit.unit, snd)
⊢ Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝¹ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
x✝ : Option (MLIRType.eval argsHead.fst)
heq✝ : SSAEnv.get headVal argsHead.fst env = none
Hv : Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok (PUnit.unit, snd)
⊢ Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
simp at Hv
State after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝¹ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
x✝ : Option (MLIRType.eval argsHead.fst)
heq✝ : SSAEnv.get headVal argsHead.fst env = none
Hv : SSAEnv.set headVal argsHead.fst argsHead.snd env = snd
⊢ Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝¹ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
x✝ : Option (MLIRType.eval argsHead.fst)
heq✝ : SSAEnv.get headVal argsHead.fst env = none
Hv : SSAEnv.set headVal argsHead.fst argsHead.snd env = snd
⊢ Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
subst snd
State after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝¹ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
x✝ : Option (MLIRType.eval argsHead.fst)
heq✝ : SSAEnv.get headVal argsHead.fst env = none
H : denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok (res, env')
⊢ Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')

State before:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝¹ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
x✝ : Option (MLIRType.eval argsHead.fst)
heq✝ : SSAEnv.get headVal argsHead.fst env = none
H : denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok (res, env')
⊢ Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
simp [H]
State after:
no goals

State before:
case h_1
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝¹ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
x✝ : Option (MLIRType.eval argsHead.fst)
v✝ : MLIRType.eval argsHead.fst
heq✝ : SSAEnv.get headVal argsHead.fst env = some v✝
Hv : Except.error ("setting to SSA value twice!", env) = Except.ok (PUnit.unit, snd)
⊢ Except.error ("setting to SSA value twice!", env) = Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
Tactic:
contradiction
State after:
no goals