internlm/Lean-Github huggingface dataset:
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 τ
⊢ 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)
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 Δ)⦄ ⦃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 Δ
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
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, resEnv)
⊢ 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)
Theorem: denoteOpArgs_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
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, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
a✝ : String × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.error a✝
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v 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, SSAEnv.set name τ v resEnv)
Tactic:
case error _ =>
  rw [Hhead] at H; contradiction
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 Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
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, resEnv)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v 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, SSAEnv.set name τ v resEnv)
Tactic:
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 Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
a✝ : String × SSAEnv Δ
H :
  (match Except.error a✝ 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, resEnv)
Hhead : TopM.get headτ headName env = Except.error a✝
⊢ (match TopM.get headτ headName (SSAEnv.set name τ v 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, SSAEnv.set name τ v resEnv)
Tactic:
contradiction
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 Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
Htail :
  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 headRes.snd =
    Except.ok rTail
H : Except.ok ({ fst := headτ, snd := headRes.fst } :: rTail.fst, rTail.snd) = Except.ok (r, resEnv)
⊢ (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 (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
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:
case h_1
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
err✝ : String × SSAEnv Δ
heq✝ :
  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 headRes.snd =
    Except.error err✝
H : Except.error err✝ = Except.ok (r, resEnv)
⊢ (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 (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
contradiction
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 Δ)
env : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail env =
        Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            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 (SSAEnv.set name τ v env) =
              Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  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 headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : True
⊢ (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 (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headRes.fst } :: rTailRes, SSAEnv.set name τ v rTailEnv)
Tactic:
rw [HInd] <;> assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ denoteRegionsSetCommutesInvariant name τ v regions →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx regions idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx regions idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
induction regions <;> intros H idx args env res env' Hrun <;> try contradiction
Proof state after:
case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head✝ : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail✝ : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
tail_ih✝ :
  denoteRegionsSetCommutesInvariant name τ v tail✝ →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail✝ idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail✝ idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head✝ :: tail✝)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head✝ :: tail✝) idx args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head✝ :: tail✝) idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) idx args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
case cons head tail HInd =>
  cases idx
  case zero =>
    simp at *
    specialize (H (by constructor) (by assumption))
    assumption
  case succ idx' =>
    specialize (HInd (by
      intros region Hregions args env res env' Hrun
      specialize (H (.tail _ Hregions) (by assumption))
      assumption
    ))
    simp at Hrun
    apply (HInd Hrun)
Proof state after:
no goals
Theorem: denoteRegionByIx_set_commutes
Proof state before:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
H : denoteRegionsSetCommutesInvariant name τ v []
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx [] idx args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx [] idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
contradiction
Proof state after:
no goals
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) Nat.zero args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) Nat.zero args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
case zero =>
  simp at *
  specialize (H (by constructor) (by assumption))
  assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
case succ idx' =>
  specialize (HInd (by
    intros region Hregions args env res env' Hrun
    specialize (H (.tail _ Hregions) (by assumption))
    assumption
  ))
  simp at Hrun
  apply (HInd Hrun)
Proof state after:
no goals