internlm/Lean-Github huggingface dataset:
Theorem: TopM.set_unfold
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ set τ name v 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)
Tactic:
simp [TopM.set]
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some val => raiseUB "setting to SSA value twice!"
        | none => StateT.set (SSAEnv.set name τ v s))
      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)
Theorem: TopM.set_unfold
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some val => raiseUB "setting to SSA value twice!"
        | none => StateT.set (SSAEnv.set name τ v s))
      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)
Tactic:
simp_monad
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ (match SSAEnv.get name τ env with
      | some val => raiseUB "setting to SSA value twice!"
      | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
      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)
Theorem: TopM.set_unfold
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ (match SSAEnv.get name τ env with
      | some val => raiseUB "setting to SSA value twice!"
      | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
      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)
Tactic:
cases (env.get name τ) <;> rfl
Proof state after:
no goals
Theorem: TopM.set_ok
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ set τ name v env = Except.ok r → r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none
Tactic:
simp [set]
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ bind StateT.get
        (fun s =>
          match SSAEnv.get name τ s with
          | some val => raiseUB "setting to SSA value twice!"
          | none => StateT.set (SSAEnv.set name τ v s))
        env =
      Except.ok r →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none
Theorem: TopM.set_ok
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ bind StateT.get
        (fun s =>
          match SSAEnv.get name τ s with
          | some val => raiseUB "setting to SSA value twice!"
          | none => StateT.set (SSAEnv.set name τ v s))
        env =
      Except.ok r →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none
Tactic:
simp_monad
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
        env =
      Except.ok r →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none
Theorem: TopM.set_ok
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
        env =
      Except.ok r →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none
Tactic:
cases (env.get name τ) <;> simp <;> intros H <;> try contradiction
Proof state after:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
H : (PUnit.unit, SSAEnv.set name τ v env) = r
⊢ r = ((), SSAEnv.set name τ v env)
Theorem: TopM.set_ok
Proof state before:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
H : (PUnit.unit, SSAEnv.set name τ v env) = r
⊢ r = ((), SSAEnv.set name τ v env)
Tactic:
rw [H]
Proof state after:
no goals
Theorem: TopM.set_ok
Proof state before:
case some
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
val✝ : MLIRType.eval τ
H : raiseUB "setting to SSA value twice!" env = Except.ok r
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: TopM.get_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃env : SSAEnv Δ⦄ ⦃r : MLIRType.eval τ⦄ ⦃env' : SSAEnv Δ⦄,
    get τ name env = Except.ok (r, env') →
      ∀ ⦃name' : SSAVal⦄,
        name' ≠ name →
          ∀ ⦃τ' : MLIRType Δ⦄ ⦃v' : MLIRType.eval τ'⦄,
            get τ name (SSAEnv.set name' τ' v' env) = Except.ok (r, SSAEnv.set name' τ' v' env')
Tactic:
intros τ name env r env' H name' Hne τ' v'
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H : get τ name env = Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ get τ name (SSAEnv.set name' τ' v' env) = Except.ok (r, SSAEnv.set name' τ' v' env')
Theorem: TopM.get_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H : get τ name env = Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ get τ name (SSAEnv.set name' τ' v' env) = Except.ok (r, SSAEnv.set name' τ' v' env')
Tactic:
rw [TopM.get_unfold] at *
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H :
  Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env) =
    Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ Except.ok
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
        | some v => v
        | none => default,
        SSAEnv.set name' τ' v' env) =
    Except.ok (r, SSAEnv.set name' τ' v' env')
Theorem: TopM.get_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H :
  Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env) =
    Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ Except.ok
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
        | some v => v
        | none => default,
        SSAEnv.set name' τ' v' env) =
    Except.ok (r, SSAEnv.set name' τ' v' env')
Tactic:
simp_monad at *
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
H :
  (match SSAEnv.get name τ env with
      | some v => v
      | none => default) =
      r ∧
    env = env'
⊢ (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
      | some v => v
      | none => default) =
      r ∧
    SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
Theorem: TopM.get_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
H :
  (match SSAEnv.get name τ env with
      | some v => v
      | none => default) =
      r ∧
    env = env'
⊢ (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
      | some v => v
      | none => default) =
      r ∧
    SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
Tactic:
simp_ssaenv at *
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
H :
  (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 ∧
    SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
Theorem: TopM.get_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
H :
  (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 ∧
    SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
Tactic:
revert H
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ (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 ∧
      SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
Theorem: TopM.get_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ (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 ∧
      SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
Tactic:
cases (env.get name τ) <;> simp at * <;> intros H1 H2 <;> subst r <;> subst env <;> simp
Proof state after:
no goals
Theorem: TopM.set_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃v : MLIRType.eval τ⦄ ⦃env : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env' : SSAEnv Δ⦄,
    set τ name v env = Except.ok (r, env') →
      ∀ ⦃name' : SSAVal⦄,
        name' ≠ name →
          ∀ (τ' : MLIRType Δ) (v' : MLIRType.eval τ'),
            ∃ env'',
              SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
                set τ name v (SSAEnv.set name' τ' v' env) = Except.ok (r, env'')
Tactic:
intros τ name v env r env' H name' Hname τ' v'
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H : set τ name v env = Except.ok (r, env')
name' : SSAVal
Hname : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧ set τ name v (SSAEnv.set name' τ' v' env) = Except.ok (r, env'')
Theorem: TopM.set_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H : set τ name v env = Except.ok (r, env')
name' : SSAVal
Hname : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧ set τ name v (SSAEnv.set name' τ' v' env) = Except.ok (r, env'')
Tactic:
simp [set] at *
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H :
  bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some val => raiseUB "setting to SSA value twice!"
        | none => StateT.set (SSAEnv.set name τ v s))
      env =
    Except.ok (r, env')
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      bind StateT.get
          (fun s =>
            match SSAEnv.get name τ s with
            | some val => raiseUB "setting to SSA value twice!"
            | none => StateT.set (SSAEnv.set name τ v s))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
Theorem: TopM.set_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H :
  bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some val => raiseUB "setting to SSA value twice!"
        | none => StateT.set (SSAEnv.set name τ v s))
      env =
    Except.ok (r, env')
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      bind StateT.get
          (fun s =>
            match SSAEnv.get name τ s with
            | some val => raiseUB "setting to SSA value twice!"
            | none => StateT.set (SSAEnv.set name τ v s))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
Tactic:
simp_monad at *
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H :
  (match SSAEnv.get name τ env with
      | some val => raiseUB "setting to SSA value twice!"
      | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
      env =
    Except.ok (r, env')
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ 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'')
Theorem: TopM.set_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H :
  (match SSAEnv.get name τ env with
      | some val => raiseUB "setting to SSA value twice!"
      | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
      env =
    Except.ok (r, env')
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ 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:
revert H
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
        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'')
Theorem: TopM.set_env_set_commutes
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
        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:
cases Hget: (env.get name τ) <;> simp <;> intros H <;> try contradiction
Proof state after:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
H : SSAEnv.set name τ v env = 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'')
Theorem: TopM.set_env_set_commutes
Proof state before:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
H : SSAEnv.set name τ v env = 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:
simp_ssaenv
Proof state after:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
H : SSAEnv.set name τ v env = env'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ 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'')
Theorem: TopM.set_env_set_commutes
Proof state before:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
H : SSAEnv.set name τ v env = env'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ 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:
subst env'
Proof state after:
case none
α σ : 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
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) env'' ∧
      (match SSAEnv.get name τ 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'')
Theorem: TopM.set_env_set_commutes
Proof state before:
case none
α σ : 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
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) env'' ∧
      (match SSAEnv.get name τ 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:
exists (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))
Proof state after:
case none
α σ : 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
⊢ SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)) ∧
    (match SSAEnv.get name τ 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, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))
Theorem: TopM.set_env_set_commutes
Proof state before:
case none
α σ : 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
⊢ SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)) ∧
    (match SSAEnv.get name τ 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, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))
Tactic:
simp[Hget]
Proof state after:
case none
α σ : 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
⊢ SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))
Theorem: TopM.set_env_set_commutes
Proof state before:
case none
α σ : 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
⊢ SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))
Tactic:
apply SSAEnv.set_commutes
Proof state after:
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'