internlm/Lean-Github huggingface dataset:
Theorem: TopM.set_env_set_commutes
Proof state before:
case none.a
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ name ≠ name'
Tactic:
simp [Ne.symm Hname]
Proof state after:
no goals
Theorem: TopM.set_env_set_commutes
Proof state before:
case some
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
val✝ : MLIRType.eval τ
Hget : SSAEnv.get name τ env = some val✝
H : raiseUB "setting to SSA value twice!" env = Except.ok (r, env')
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
Tactic:
contradiction
Proof state after:
no goals
Theorem: TopM.get_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃env₁ env₂ : SSAEnv Δ⦄,
    SSAEnv.equiv env₁ env₂ →
      ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃r : MLIRType.eval τ⦄ ⦃env₁' : SSAEnv Δ⦄,
        get τ name env₁ = Except.ok (r, env₁') → get τ name env₂ = Except.ok (r, env₂)
Tactic:
intros env₁ env₂ Hequiv τ name r env₁'
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ get τ name env₁ = Except.ok (r, env₁') → get τ name env₂ = Except.ok (r, env₂)
Theorem: TopM.get_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ get τ name env₁ = Except.ok (r, env₁') → get τ name env₂ = Except.ok (r, env₂)
Tactic:
repeat rw [TopM.get_unfold]
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₁ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)
Theorem: TopM.get_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₁ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)
Tactic:
rw [Hequiv]
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)
Theorem: TopM.get_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)
Tactic:
simp_monad
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₂ with
      | some v => v
      | none => default) =
      r →
    env₁ = env₁' →
      (match SSAEnv.get name τ env₂ with
        | some v => v
        | none => default) =
        r
Theorem: TopM.get_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₂ with
      | some v => v
      | none => default) =
      r →
    env₁ = env₁' →
      (match SSAEnv.get name τ env₂ with
        | some v => v
        | none => default) =
        r
Tactic:
intros H _
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
H :
  (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r
a✝ : env₁ = env₁'
⊢ (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r
Theorem: TopM.get_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
H :
  (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r
a✝ : env₁ = env₁'
⊢ (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r
Tactic:
rw [H]
Proof state after:
no goals
Theorem: TopM.get_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₁ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    get τ name env₂ = Except.ok (r, env₂)
Tactic:
rw [TopM.get_unfold]
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₁ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)
Theorem: TopM.set_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃env₁ env₂ : SSAEnv Δ⦄,
    SSAEnv.equiv env₁ env₂ →
      ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃v : MLIRType.eval τ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
        set τ name v env₁ = Except.ok (r, env₁') → set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
intros env₁ env₂ Hequiv τ name v r env₁'
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ set τ name v env₁ = Except.ok (r, env₁') → set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)
Theorem: TopM.set_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ set τ name v env₁ = Except.ok (r, env₁') → set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
repeat rw [TopM.set_unfold]
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, env₁') →
    (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₂)
      | none => Except.ok ((), SSAEnv.set name τ v env₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)
Theorem: TopM.set_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, env₁') →
    (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₂)
      | none => Except.ok ((), SSAEnv.set name τ v env₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
rw [Hequiv]
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, env₁') →
    (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₂)
      | none => Except.ok ((), SSAEnv.set name τ v env₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)
Theorem: TopM.set_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, env₁') →
    (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₂)
      | none => Except.ok ((), SSAEnv.set name τ v env₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
cases (SSAEnv.get name τ env₂) <;> simp
Proof state after:
no goals
Theorem: TopM.set_equiv
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, env₁') →
    set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
rw [TopM.set_unfold]
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, env₁') →
    (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₂)
      | none => Except.ok ((), SSAEnv.set name τ v env₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)
Theorem: denoteOpArgs_res
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' = 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' = 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' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head✝ :: tail✝) env = Except.ok (r, env')
⊢ env' = env
Theorem: denoteOpArgs_res
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' = env
Tactic:
case nil =>
  simp [denoteOpArgs] at *
  simp_monad at *
  cases H; subst r env
  simp
Proof state after:
no goals
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 Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
⊢ env' = env
Tactic:
case cons head tail HInd =>
  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 r =>
  rw [TopM.get_unfold] at Hhead
  have ⟨rRes, rEnv⟩ := r; simp at Hhead; cases Hhead; subst rEnv
  simp [denoteOpArgs] at HInd
  split at H <;> try contradiction
  case h_2 tailR HTailR =>
  have ⟨tailRes, tailEnv⟩ := tailR
  simp at *
  specialize HInd HTailR
  cases H; subst env'
  assumption
Proof state after:
no goals
Theorem: denoteOpArgs_res
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' = 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' = env
Theorem: denoteOpArgs_res
Proof state before:
α₁ σ₁ : 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' = env
Tactic:
simp_monad at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : [] = r ∧ env = env'
⊢ env' = env
Theorem: denoteOpArgs_res
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : [] = r ∧ env = env'
⊢ env' = env
Tactic:
cases H
Proof state after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
left✝ : [] = r
right✝ : env = env'
⊢ env' = env
Theorem: denoteOpArgs_res
Proof state before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
left✝ : [] = r
right✝ : env = env'
⊢ env' = env
Tactic:
subst r env
Proof state after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env' : SSAEnv Δ
⊢ env' = env'
Theorem: denoteOpArgs_res
Proof state before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env' : SSAEnv Δ
⊢ env' = env'
Tactic:
simp
Proof state after:
no goals
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 Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
⊢ env' = env
Tactic:
simp [denoteOpArgs] at H
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 Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H :
  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))
      env =
    Except.ok (r, 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 Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H :
  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))
      env =
    Except.ok (r, env')
⊢ env' = env
Tactic:
have ⟨headName, headτ⟩ := head
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 Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
H :
  bind (TopM.get (headName, headτ).snd (headName, 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 := (headName, headτ).snd, snd := x } :: __do_lift))
      env =
    Except.ok (r, 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 Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
H :
  bind (TopM.get (headName, headτ).snd (headName, 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 := (headName, headτ).snd, snd := x } :: __do_lift))
      env =
    Except.ok (r, env')
⊢ env' = env
Tactic:
simp_monad 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 Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, 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 Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env')
⊢ env' = env
Tactic:
revert H
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 Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') → env' = env
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
⊢ (match TopM.get headτ headName env with
      | Except.error err => Except.error err
      | Except.ok v =>
        match
          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 v.snd with
        | Except.error err => Except.error err
        | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
      Except.ok (r, env') →
    env' = env