internlm/Lean-Github huggingface dataset:
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 Δ
⊢ (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:
cases Hhead: TopM.get headτ headName env <;> simp <;> intros H <;> try contradiction
Proof state after:
case ok
α₁ σ₁ : 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 Δ
a✝ : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok a✝
H :
  (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 a✝.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := a✝.fst } :: v.fst, v.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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok r
H :
  (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 r.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := r.fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
⊢ env' = env
Tactic:
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 Δ
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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok r
H :
  (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 r.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := r.fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
⊢ env' = env
Tactic:
rw [TopM.get_unfold] at Hhead
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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
Hhead :
  Except.ok
      (match SSAEnv.get headName headτ env with
        | some v => v
        | none => default,
        env) =
    Except.ok r
H :
  (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 r.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := r.fst } :: v.fst, v.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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
Hhead :
  Except.ok
      (match SSAEnv.get headName headτ env with
        | some v => v
        | none => default,
        env) =
    Except.ok r
H :
  (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 r.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := r.fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
⊢ env' = env
Tactic:
have ⟨rRes, rEnv⟩ := r
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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
rEnv : SSAEnv Δ
Hhead :
  Except.ok
      (match SSAEnv.get headName headτ env with
        | some v => v
        | none => default,
        env) =
    Except.ok (rRes, rEnv)
H :
  (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 (rRes, rEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, rEnv).fst } :: v.fst, v.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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
rEnv : SSAEnv Δ
Hhead :
  Except.ok
      (match SSAEnv.get headName headτ env with
        | some v => v
        | none => default,
        env) =
    Except.ok (rRes, rEnv)
H :
  (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 (rRes, rEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, rEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
⊢ env' = env
Tactic:
simp at Hhead
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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
rEnv : SSAEnv Δ
H :
  (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 (rRes, rEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, rEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
Hhead :
  (match SSAEnv.get headName headτ env with
      | some v => v
      | none => default) =
      rRes ∧
    env = rEnv
⊢ 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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
rEnv : SSAEnv Δ
H :
  (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 (rRes, rEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, rEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
Hhead :
  (match SSAEnv.get headName headτ env with
      | some v => v
      | none => default) =
      rRes ∧
    env = rEnv
⊢ env' = env
Tactic:
cases Hhead
Proof state after:
case intro
α₁ σ₁ : 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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
rEnv : SSAEnv Δ
H :
  (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 (rRes, rEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, rEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
right✝ : env = rEnv
⊢ env' = env
Theorem: denoteOpArgs_res
Proof state before:
case intro
α₁ σ₁ : 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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
rEnv : SSAEnv Δ
H :
  (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 (rRes, rEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, rEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
right✝ : env = rEnv
⊢ env' = env
Tactic:
subst rEnv
Proof state after:
case intro
α₁ σ₁ : 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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
H :
  (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 (rRes, env).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
⊢ env' = env
Theorem: denoteOpArgs_res
Proof state before:
case intro
α₁ σ₁ : 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 Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
H :
  (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 (rRes, env).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
⊢ env' = env
Tactic:
simp [denoteOpArgs] at HInd
Proof state after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
H :
  (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 (rRes, env).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
⊢ env' = env
Theorem: denoteOpArgs_res
Proof state before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
H :
  (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 (rRes, env).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: v.fst, v.snd)) =
    Except.ok (r✝, env')
⊢ env' = env
Tactic:
split at H <;> try contradiction
Proof state after:
case intro.h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
v✝ : List (TypedArg Δ) × 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 (rRes, env).snd =
    Except.ok v✝
H : Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: v✝.fst, v✝.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 Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
HTailR :
  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 (rRes, env).snd =
    Except.ok tailR
H : Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: tailR.fst, tailR.snd) = Except.ok (r✝, env')
⊢ env' = env
Tactic:
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:
case intro.h_1
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
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 (rRes, env).snd =
    Except.error err✝
H : Except.error err✝ = Except.ok (r✝, env')
⊢ env' = env
Tactic:
contradiction
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 Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
HTailR :
  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 (rRes, env).snd =
    Except.ok tailR
H : Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: tailR.fst, tailR.snd) = Except.ok (r✝, env')
⊢ env' = env
Tactic:
have ⟨tailRes, tailEnv⟩ := tailR
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 Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, env') →
      env' = env
env : SSAEnv Δ
r✝ : List (TypedArg Δ)
env' : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
r : MLIRType.eval headτ × SSAEnv Δ
rRes : MLIRType.eval headτ
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    rRes
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × SSAEnv Δ
tailRes : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 (rRes, env).snd =
    Except.ok (tailRes, tailEnv)
H :
  Except.ok ({ fst := headτ, snd := (rRes, env).fst } :: (tailRes, tailEnv).fst, (tailRes, tailEnv).snd) =
    Except.ok (r✝, env')
⊢ env' = env