internlm/Lean-Github huggingface dataset:
Theorem: mapDenoteRegion_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
⊢ denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ (head :: tail))
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 Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
HregIn : region ∈ TopM.mapDenoteRegion Δ (head :: tail)
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 Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
HregIn : region ∈ TopM.mapDenoteRegion Δ (head :: tail)
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:
simp [TopM.mapDenoteRegion] at HregIn
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HregIn : region = TopM.scoped ∘ denoteRegion Δ head ∨ region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ 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 Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HregIn : region = TopM.scoped ∘ denoteRegion Δ head ∨ region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
cases HregIn
Proof state after:
case inl
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
h✝ : region = TopM.scoped ∘ denoteRegion Δ head
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')

case inr
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
h✝ : region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ 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 Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HXX : region = TopM.scoped ∘ denoteRegion Δ head
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
case inl HXX =>
  subst HXX;
  sorry
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 Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HXX : region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
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 Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HXX : region = TopM.scoped ∘ denoteRegion Δ head
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
subst HXX
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : Function.comp TopM.scoped (denoteRegion Δ head) args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ Function.comp TopM.scoped (denoteRegion Δ head) 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 Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : Function.comp TopM.scoped (denoteRegion Δ head) args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ Function.comp TopM.scoped (denoteRegion Δ head) args env₂ = Except.ok (res, env₂')
Tactic:
sorry
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 Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HXX : region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
apply mapDenoteRegion_equiv <;> assumption
Proof state after:
no goals
Theorem: denoteOpArgs_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
args : List (TypedSSAVal Δ)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ args env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all args fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ args (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
induction args
Proof state after:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ [] env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)

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 Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail✝ env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail✝ fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail✝ (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ (head✝ :: tail✝) env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all (head✝ :: tail✝) fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ (head✝ :: tail✝) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Theorem: denoteOpArgs_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ [] env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
case nil =>
  intros env r resEnv H
  simp [denoteOpArgs] at *
  simp_monad at *
  cases H; subst r env; simp
Proof state after:
no goals
Theorem: denoteOpArgs_set_commutes
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 Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ (head :: tail) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
case cons head tail HInd =>
  intros env r resEnv H name Hname τ v
  simp [denoteOpArgs]; simp [denoteOpArgs] at H
  have ⟨headName, headτ⟩ := head
  simp_monad at *
  cases Hhead: (TopM.get headτ headName env)
  case error _ =>
    rw [Hhead] at H; contradiction
  case ok headRes =>
    rw [Hhead] at H
    simp [List.all, List.foldr] at Hname
    have ⟨Hname_head, _⟩ := Hname
    rw [TopM.get_env_set_commutes Hhead Hname_head]
    simp at *
    split at H <;> try contradiction
    case h_2 rTail Htail =>
    have ⟨rTailRes, rTailEnv⟩ := rTail
    simp at H; have ⟨_, _⟩ := H; subst r resEnv
    simp [denoteOpArgs] at *
    simp [bind, StateT.bind, Except.bind, pure, StateT.pure, Except.pure] at HInd
    rw [HInd] <;> assumption
Proof state after:
no goals
Theorem: denoteOpArgs_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ [] env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
intros env r resEnv H
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, resEnv)
⊢ ∀ ⦃name : SSAVal⦄,
    (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
      ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
        denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Theorem: denoteOpArgs_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, resEnv)
⊢ ∀ ⦃name : SSAVal⦄,
    (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
      ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
        denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp [denoteOpArgs] at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : pure [] env = Except.ok (r, resEnv)
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    pure [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Theorem: denoteOpArgs_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : pure [] env = Except.ok (r, resEnv)
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    pure [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp_monad at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : [] = r ∧ env = resEnv
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = r ∧ SSAEnv.set name τ v env = SSAEnv.set name τ v resEnv
Theorem: denoteOpArgs_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : [] = r ∧ env = resEnv
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = r ∧ SSAEnv.set name τ v env = SSAEnv.set name τ v resEnv
Tactic:
cases H
Proof state after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
left✝ : [] = r
right✝ : env = resEnv
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = r ∧ SSAEnv.set name τ v env = SSAEnv.set name τ v resEnv
Theorem: denoteOpArgs_set_commutes
Proof state before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
left✝ : [] = r
right✝ : env = resEnv
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = r ∧ SSAEnv.set name τ v env = SSAEnv.set name τ v resEnv
Tactic:
subst r env
Proof state after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
resEnv : SSAEnv Δ
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = [] ∧ SSAEnv.set name τ v resEnv = SSAEnv.set name τ v resEnv
Theorem: denoteOpArgs_set_commutes
Proof state before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
resEnv : SSAEnv Δ
⊢ ∀ ⦃name : SSAVal⦄ (τ : MLIRType Δ) (v : MLIRType.eval τ),
    [] = [] ∧ SSAEnv.set name τ v resEnv = SSAEnv.set name τ v resEnv
Tactic:
simp
Proof state after:
no goals
Theorem: denoteOpArgs_set_commutes
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 Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ (head :: tail) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
intros env r resEnv H name Hname τ v
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 Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv)
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
⊢ denoteOpArgs Δ (head :: tail) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Theorem: denoteOpArgs_set_commutes
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 Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv)
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
⊢ denoteOpArgs Δ (head :: tail) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
simp [denoteOpArgs]
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 Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv)
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
⊢ bind (TopM.get head.snd head.fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := head.snd, snd := x } :: __do_lift))
      (SSAEnv.set name τ v env) =
    Except.ok (r, SSAEnv.set name τ v resEnv)