internlm/Lean-Github huggingface dataset:
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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]
Proof state after:
no goals
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof state after:
no goals
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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]
Proof state after:
no goals
Theorem: denoteTypedArgs_cons_args
Proof 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 *
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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]
Proof state after:
no goals
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof state after:
no goals
Theorem: denoteTypedArgs_cons_unfold
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
headVal : SSAVal
tailVal : List SSAVal
headArgs : TypedArg Δ
tailArgs : List (TypedArg Δ)
env : SSAEnv Δ
⊢ denoteTypedArgs (headArgs :: tailArgs) (headVal :: tailVal) env =
    bind (TopM.set headArgs.fst headVal headArgs.snd) (fun x => denoteTypedArgs tailArgs tailVal) env
Tactic:
simp [denoteTypedArgs]
Proof state after:
no goals
Theorem: denoteOpArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
args : List (TypedSSAVal Δ)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ args env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ args env₂ = Except.ok (r, env₂)
Tactic:
induction args <;> intros env r env' H
Proof state after:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ [] env₂ = Except.ok (r, env₂)

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 Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail✝ env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail✝ env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head✝ :: tail✝) env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ (head✝ :: tail✝) env₂ = Except.ok (r, env₂)
Theorem: denoteOpArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ [] env₂ = Except.ok (r, env₂)
Tactic:
case nil =>
  simp [denoteOpArgs] at *
  simp_monad at *
  cases H; subst r env
  simp
Proof state after:
no goals
Theorem: denoteOpArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ (head :: tail) env₂ = Except.ok (r, env₂)
Tactic:
case cons head tail HInd =>
  intros env₂ Henv₂
  simp [denoteOpArgs]; simp [denoteOpArgs] at H
  have ⟨headName, headτ⟩ := head
  simp_monad at *
  revert H
  cases Hhead: TopM.get headτ headName env <;> simp <;> intros H <;> try contradiction
  case ok headR =>
  have ⟨headR, headEnv⟩ := headR
  simp [TopM.get_equiv Henv₂ Hhead]
  split at H <;> try contradiction
  case h_2 tailR HTailR =>
  simp at H; cases H; subst env' r
  have ⟨tailR, tailEnv⟩ := tailR; simp at HTailR
  have AOEU := HInd HTailR
  rw [TopM.get_unfold] at Hhead; simp at Hhead; cases Hhead; subst env
  specialize HInd HTailR Henv₂
  simp [denoteOpArgs] at HInd
  simp_monad at *
  simp [HInd]
Proof state after:
no goals
Theorem: denoteOpArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ [] env₂ = Except.ok (r, env₂)
Tactic:
simp [denoteOpArgs] at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : pure [] env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → pure [] env₂ = Except.ok (r, env₂)