internlm/Lean-Github huggingface dataset:
Theorem: denoteOpArgs_res
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 Δ⦄,
    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, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (rRes, env).snd =
    Except.ok (tailRes, tailEnv)
H :
  Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: (tailRes, tailEnv).fst, (tailRes, tailEnv).snd) =
    Except.ok (r✝, env')
⊢ env' = env
Tactic:
simp at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : 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, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (tailRes, tailEnv)
H : { fst := headτ, snd := rRes } :: tailRes = r✝ ∧ tailEnv = env'
⊢ env' = env
Theorem: denoteOpArgs_res
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 Δ⦄,
    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, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (tailRes, tailEnv)
H : { fst := headτ, snd := rRes } :: tailRes = r✝ ∧ tailEnv = env'
⊢ env' = env
Tactic:
specialize HInd HTailR
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (tailRes, tailEnv)
H : { fst := headτ, snd := rRes } :: tailRes = r✝ ∧ tailEnv = env'
HInd : tailEnv = env
⊢ env' = env
Theorem: denoteOpArgs_res
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (tailRes, tailEnv)
H : { fst := headτ, snd := rRes } :: tailRes = r✝ ∧ tailEnv = env'
HInd : tailEnv = env
⊢ env' = env
Tactic:
cases H
Proof state after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝¹ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (tailRes, tailEnv)
HInd : tailEnv = env
left✝ : { fst := headτ, snd := rRes } :: tailRes = r✝
right✝ : tailEnv = env'
⊢ env' = env
Theorem: denoteOpArgs_res
Proof state before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝¹ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (tailRes, tailEnv)
HInd : tailEnv = env
left✝ : { fst := headτ, snd := rRes } :: tailRes = r✝
right✝ : tailEnv = env'
⊢ env' = env
Tactic:
subst env'
Proof state after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝¹ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (tailRes, tailEnv)
HInd : tailEnv = env
left✝ : { fst := headτ, snd := rRes } :: tailRes = r✝
⊢ tailEnv = env
Theorem: denoteOpArgs_res
Proof state before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝¹ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (tailRes, tailEnv)
HInd : tailEnv = env
left✝ : { fst := headτ, snd := rRes } :: tailRes = r✝
⊢ tailEnv = env
Tactic:
assumption
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 δ
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
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof 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')
Theorem: denoteTypedArgs_cons_args
Proof 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
Proof 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')
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
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]
Proof state after:
no goals
Theorem: denoteTypedArgs_cons_args
Proof 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
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
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
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
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')
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
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
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
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')
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
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 *
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
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')
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
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
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
⊢ (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')