internlm/Lean-Github huggingface dataset:
Theorem: denoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
⊢ ∀ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    denoteRegion Δ (Region.mk rName rArgs rOps) args env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂',
            SSAEnv.equiv env' env₂' ∧ denoteRegion Δ (Region.mk rName rArgs rOps) args env₂ = Except.ok (res, env₂')
Tactic:
intros args env res env' H env₂ Henv₂
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : denoteRegion Δ (Region.mk rName rArgs rOps) args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteRegion Δ (Region.mk rName rArgs rOps) args env₂ = Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : denoteRegion Δ (Region.mk rName rArgs rOps) args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteRegion Δ (Region.mk rName rArgs rOps) args env₂ = Except.ok (res, env₂')
Tactic:
simp [denoteRegion] at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : bind (denoteTypedArgs args (List.map Prod.fst rArgs)) (fun x => denoteOps Δ rOps) env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      bind (denoteTypedArgs args (List.map Prod.fst rArgs)) (fun x => denoteOps Δ rOps) env₂ = Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : bind (denoteTypedArgs args (List.map Prod.fst rArgs)) (fun x => denoteOps Δ rOps) env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      bind (denoteTypedArgs args (List.map Prod.fst rArgs)) (fun x => denoteOps Δ rOps) env₂ = Except.ok (res, env₂')
Tactic:
simp_monad at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match denoteTypedArgs args (List.map Prod.fst rArgs) env with
    | Except.error err => Except.error err
    | Except.ok v => denoteOps Δ rOps v.snd) =
    Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match denoteTypedArgs args (List.map Prod.fst rArgs) env with
    | Except.error err => Except.error err
    | Except.ok v => denoteOps Δ rOps v.snd) =
    Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Tactic:
(split at H <;> try contradiction)
Proof state after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
v✝ : Unit × SSAEnv Δ
heq✝ : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok v✝
H : denoteOps Δ rOps v✝.snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
v✝ : Unit × SSAEnv Δ
heq✝ : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok v✝
H : denoteOps Δ rOps v✝.snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Tactic:
rename_i argsR HargsR
Proof state after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok argsR
H : denoteOps Δ rOps argsR.snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok argsR
H : denoteOps Δ rOps argsR.snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Tactic:
have ⟨argsR, argsEnv⟩ := argsR
Proof state after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR✝ : Unit × SSAEnv Δ
argsR : Unit
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (argsR, argsEnv)
H : denoteOps Δ rOps (argsR, argsEnv).snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR✝ : Unit × SSAEnv Δ
argsR : Unit
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (argsR, argsEnv)
H : denoteOps Δ rOps (argsR, argsEnv).snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Tactic:
cases argsR
Proof state after:
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps (PUnit.unit, argsEnv).snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps (PUnit.unit, argsEnv).snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Tactic:
have ⟨argsEnv₂, HargsEnv₂, HdenoteArgs⟩ := denoteTypedArgs_equiv HargsR Henv₂
Proof state after:
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps (PUnit.unit, argsEnv).snd = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps (PUnit.unit, argsEnv).snd = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Tactic:
rw [HdenoteArgs]
Proof state after:
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps (PUnit.unit, argsEnv).snd = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match Except.ok (PUnit.unit, argsEnv₂) with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps (PUnit.unit, argsEnv).snd = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match Except.ok (PUnit.unit, argsEnv₂) with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Tactic:
simp at *
Proof state after:
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps argsEnv = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ rOps argsEnv₂ = Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps argsEnv = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ rOps argsEnv₂ = Except.ok (res, env₂')
Tactic:
apply denoteOps_equiv (by assumption) (by assumption)
Proof state after:
no goals
Theorem: denoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match denoteTypedArgs args (List.map Prod.fst rArgs) env with
    | Except.error err => Except.error err
    | Except.ok v => denoteOps Δ rOps v.snd) =
    Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Tactic:
split at H <;> try contradiction
Proof state after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
v✝ : Unit × SSAEnv Δ
heq✝ : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok v✝
H : denoteOps Δ rOps v✝.snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Theorem: denoteRegion_equiv
Proof state before:
case h_1
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
err✝ : String × SSAEnv Δ
heq✝ : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.error err✝
H : Except.error err✝ = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
Tactic:
contradiction
Proof state after:
no goals
Theorem: denoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps argsEnv = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ denoteOps Δ rOps ?m.1614925 = Except.ok (res, env')
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps argsEnv = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ SSAEnv.equiv argsEnv argsEnv₂
Tactic:
assumption
Proof state after:
no goals
Theorem: mapDenoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
⊢ denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions)
Tactic:
match REGIONS: regions with
| .nil =>
  intros region HregIn args env res env' H env₂ Henv₂
  contradiction
| .cons head tail =>
  intros region HregIn args env res env' H env₂ Henv₂
  simp [TopM.mapDenoteRegion] at HregIn
  cases HregIn
  case inl HXX =>
    subst HXX;
    sorry
    case inr HXX =>
    apply mapDenoteRegion_equiv <;> assumption
Proof state after:
no goals
Theorem: mapDenoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
REGIONS : regions = []
⊢ denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ [])
Tactic:
intros region HregIn args env res env' H env₂ Henv₂
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
REGIONS : regions = []
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
HregIn : region ∈ TopM.mapDenoteRegion Δ []
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Theorem: mapDenoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
REGIONS : regions = []
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
HregIn : region ∈ TopM.mapDenoteRegion Δ []
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
contradiction
Proof state after:
no goals