internlm/Lean-Github huggingface dataset:
Theorem: run_bind_success
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
S : Semantics Δ
ma : TopM Δ a
a2mb : a → TopM Δ b
env : SSAEnv Δ
va : a
env' : SSAEnv Δ
MA : ma env = Except.ok (va, env')
⊢ run
      (fun s =>
        match ma s with
        | Except.error err => Except.error err
        | Except.ok v => a2mb v.fst v.snd)
      env =
    run (a2mb va) env'
Tactic:
simp[run, StateT.run] at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
S : Semantics Δ
ma : TopM Δ a
a2mb : a → TopM Δ b
env : SSAEnv Δ
va : a
env' : SSAEnv Δ
MA : ma env = Except.ok (va, env')
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => a2mb v.fst v.snd) =
    a2mb va env'
Theorem: run_bind_success
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
S : Semantics Δ
ma : TopM Δ a
a2mb : a → TopM Δ b
env : SSAEnv Δ
va : a
env' : SSAEnv Δ
MA : ma env = Except.ok (va, env')
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => a2mb v.fst v.snd) =
    a2mb va env'
Tactic:
simp[MA]
Proof state after:
no goals
Theorem: run_denoteRegion
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
args : TypedArgs Δ
env : SSAEnv Δ
name : String
formals : List (TypedSSAVal Δ)
ops : List (Op Δ)
⊢ run (denoteRegion Δ (Region.mk name formals ops) args) env =
    run
      (do
        denoteTypedArgs args (List.map Prod.fst formals)
        denoteOps Δ ops)
      env
Tactic:
simp[denoteRegion]
Proof state after:
no goals
Theorem: run_denoteTypedArgs_nil
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
⊢ run (denoteTypedArgs [] []) env = Except.ok ((), env)
Tactic:
simp[denoteTypedArgs, pure, run, StateT.run, StateT.pure, Except.pure]
Proof state after:
no goals
Theorem: run_denoteOps_nil
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
⊢ run (denoteOps Δ []) env = Except.ok ([], env)
Tactic:
simp[denoteOps]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
⊢ run (pure []) env = Except.ok ([], env)
Theorem: run_denoteOps_nil
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
⊢ run (pure []) env = Except.ok ([], env)
Tactic:
simp [pure, StateT.pure, run, StateT.run, Except.pure]
Proof state after:
no goals
Theorem: run_denoteOps_cons
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
op op' : Op Δ
ops : List (Op Δ)
⊢ run (denoteOps Δ (op :: op' :: ops)) env =
    run
      (do
        let __discr ← denoteOp Δ op
        let x : TypedArgs Δ := __discr
        denoteOps Δ (op' :: ops))
      env
Tactic:
simp[denoteOps]
Proof state after:
no goals
Theorem: run_denoteOps_singleton
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
op : Op Δ
⊢ run (denoteOps Δ [op]) env = run (denoteOp Δ op) env
Tactic:
simp[denoteOps]
Proof state after:
no goals
Theorem: run_denoteOp
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
name : String
res args : List (TypedSSAVal Δ)
regions : List (Region Δ)
attrs : AttrDict Δ
⊢ run (denoteOp Δ (Op.mk name res args regions attrs)) env =
    run
      (do
        let args ← denoteOpArgs Δ args
        let ret ←
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
              (Semantics.semantics_op (IOp.mk name (List.map Prod.snd res) args (OpM.denoteRegions regions 0) attrs))
        match res with
          | [] => pure ret
          | [res] =>
            match ret with
            | [{ fst := τ, snd := v }] => do
              TopM.set τ res.fst v
              pure ret
            | x => do
              TopM.raiseUB (toString "denoteOp: expected 1 return value, got '" ++ toString ret ++ toString "'")
              pure ret
          | x => do
            TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString res ++ toString "'")
            pure ret)
      env
Tactic:
simp [denoteOp]
Proof state after:
no goals
Theorem: run_denoteOpArgs_cons_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
name : SSAVal
ty : MLIRType Δ
args : List (TypedSSAVal Δ)
⊢ run (denoteOpArgs Δ ((name, ty) :: args)) env =
    run
      (do
        let x ← TopM.get ty name
        let xs ← denoteOpArgs Δ args
        pure ({ fst := ty, snd := x } :: xs))
      env
Tactic:
simp[denoteOpArgs]
Proof state after:
no goals
Theorem: run_TopM_get_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env : SSAEnv Δ
ty : MLIRType Δ
name : SSAVal
⊢ run (TopM.get ty name) env =
    Except.ok
      (match SSAEnv.get name ty env with
        | some v => v
        | none => default,
        env)
Tactic:
simp[TopM.get, run, StateT.run, StateT.get, bind, StateT.bind, Except.bind, pure,
Except.pure, StateT.pure]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env : SSAEnv Δ
ty : MLIRType Δ
name : SSAVal
⊢ (match SSAEnv.get name ty env with
      | some v => fun s => Except.ok (v, s)
      | none => fun s => Except.ok (default, s))
      env =
    Except.ok
      (match SSAEnv.get name ty env with
        | some v => v
        | none => default,
        env)
Theorem: run_TopM_get_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env : SSAEnv Δ
ty : MLIRType Δ
name : SSAVal
⊢ (match SSAEnv.get name ty env with
      | some v => fun s => Except.ok (v, s)
      | none => fun s => Except.ok (default, s))
      env =
    Except.ok
      (match SSAEnv.get name ty env with
        | some v => v
        | none => default,
        env)
Tactic:
cases H:SSAEnv.get name ty env <;> simp
Proof state after:
no goals
Theorem: run_TopM_get_success
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
⊢ run (TopM.get ty name) env = Except.ok (v, env)
Tactic:
simp[run_TopM_get_, ENV]
Proof state after:
no goals
Theorem: run_denoteOpArgs_cons_success
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ run (denoteOpArgs Δ ((name, ty) :: args)) env =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Tactic:
simp[run_denoteOpArgs_cons_]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ run
      (do
        let x ← TopM.get ty name
        let xs ← denoteOpArgs Δ args
        pure ({ fst := ty, snd := x } :: xs))
      env =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Theorem: run_denoteOpArgs_cons_success
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ run
      (do
        let x ← TopM.get ty name
        let xs ← denoteOpArgs Δ args
        pure ({ fst := ty, snd := x } :: xs))
      env =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Tactic:
simp [run_bind]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match run (TopM.get ty name) env with
    | Except.ok (a, env') =>
      match run (denoteOpArgs Δ args) env' with
      | Except.ok (a_1, env') => run (pure ({ fst := ty, snd := a } :: a_1)) env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Theorem: run_denoteOpArgs_cons_success
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match run (TopM.get ty name) env with
    | Except.ok (a, env') =>
      match run (denoteOpArgs Δ args) env' with
      | Except.ok (a_1, env') => run (pure ({ fst := ty, snd := a } :: a_1)) env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Tactic:
simp[run_TopM_get_success (ENV := ENV)]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match run (denoteOpArgs Δ args) env with
    | Except.ok (a, env') => run (pure ({ fst := ty, snd := v } :: a)) env'
    | Except.error e => Except.error e) =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Theorem: run_denoteOpArgs_cons_success
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match run (denoteOpArgs Δ args) env with
    | Except.ok (a, env') => run (pure ({ fst := ty, snd := v } :: a)) env'
    | Except.error e => Except.error e) =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Tactic:
simp[pure, StateT.pure, run, StateT.run, Except.pure]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match denoteOpArgs Δ args env with
    | Except.ok (a, env') => Except.ok ({ fst := ty, snd := v } :: a, env')
    | Except.error e => Except.error e) =
    match denoteOpArgs Δ args env with
    | Except.ok (a, env') => Except.ok ({ fst := ty, snd := v } :: a, env')
    | Except.error e => Except.error e
Theorem: run_denoteOpArgs_cons_success
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match denoteOpArgs Δ args env with
    | Except.ok (a, env') => Except.ok ({ fst := ty, snd := v } :: a, env')
    | Except.error e => Except.error e) =
    match denoteOpArgs Δ args env with
    | Except.ok (a, env') => Except.ok ({ fst := ty, snd := v } :: a, env')
    | Except.error e => Except.error e
Tactic:
cases denoteOpArgs Δ args env <;> simp
Proof state after:
no goals
Theorem: run_denoteOpArgs_nil
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
⊢ run (denoteOpArgs Δ []) env = Except.ok ([], env)
Tactic:
simp[denoteOpArgs]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
⊢ run (pure []) env = Except.ok ([], env)
Theorem: run_denoteOpArgs_nil
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
⊢ run (pure []) env = Except.ok ([], env)
Tactic:
simp[run, pure, StateT.run, StateT.pure, Except.pure]
Proof state after:
no goals
Theorem: run_pure
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a : Type
Δ : Dialect α σ ε
env : SSAEnv Δ
v : a
⊢ run (pure v) env = Except.ok (v, env)
Tactic:
simp[run, pure, StateT.run, StateT.pure, Except.pure]
Proof state after:
no goals
Theorem: OpM_toTopM_denoteRegion
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
ix : ℕ
Δ : Dialect α σ ε
args : TypedArgs Δ
r : Region Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ OpM.toTopM rs (OpM.denoteRegion r ix args) = TopM.denoteRegionsByIx rs ix args
Tactic:
simp[OpM.denoteRegion]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
ix : ℕ
Δ : Dialect α σ ε
args : TypedArgs Δ
r : Region Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ OpM.toTopM rs (OpM.RunRegion ix args fun retvals => OpM.Ret retvals) = TopM.denoteRegionsByIx rs ix args
Theorem: OpM_toTopM_denoteRegion
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
ix : ℕ
Δ : Dialect α σ ε
args : TypedArgs Δ
r : Region Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ OpM.toTopM rs (OpM.RunRegion ix args fun retvals => OpM.Ret retvals) = TopM.denoteRegionsByIx rs ix args
Tactic:
simp[OpM.toTopM]
Proof state after:
no goals
Theorem: run_OpM_toTopM_denoteRegion
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
ix : ℕ
Δ : Dialect α σ ε
args : TypedArgs Δ
r : Region Δ
env : SSAEnv Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ run (OpM.toTopM rs (OpM.denoteRegion r ix args)) env = run (TopM.denoteRegionsByIx rs ix args) env
Tactic:
simp[OpM.denoteRegion]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
ix : ℕ
Δ : Dialect α σ ε
args : TypedArgs Δ
r : Region Δ
env : SSAEnv Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ run (OpM.toTopM rs (OpM.RunRegion ix args fun retvals => OpM.Ret retvals)) env =
    run (TopM.denoteRegionsByIx rs ix args) env
Theorem: run_OpM_toTopM_denoteRegion
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
ix : ℕ
Δ : Dialect α σ ε
args : TypedArgs Δ
r : Region Δ
env : SSAEnv Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ run (OpM.toTopM rs (OpM.RunRegion ix args fun retvals => OpM.Ret retvals)) env =
    run (TopM.denoteRegionsByIx rs ix args) env
Tactic:
simp[OpM.toTopM]
Proof state after:
no goals
Theorem: run_OpM_toTopM_Ret
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env : SSAEnv Δ
v : TypedArgs Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ run (OpM.toTopM rs (OpM.Ret v)) env = Except.ok (v, env)
Tactic:
simp[OpM.toTopM]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env : SSAEnv Δ
v : TypedArgs Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ run (pure v) env = Except.ok (v, env)
Theorem: run_OpM_toTopM_Ret
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env : SSAEnv Δ
v : TypedArgs Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ run (pure v) env = Except.ok (v, env)
Tactic:
simp[run_pure]
Proof state after:
no goals
Theorem: TopM_mapDenoteRegion_cons
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
r : Region Δ
rs : List (Region Δ)
⊢ TopM.mapDenoteRegion Δ (r :: rs) = TopM.scoped ∘ denoteRegion Δ r :: TopM.mapDenoteRegion Δ rs
Tactic:
simp[TopM.mapDenoteRegion]
Proof state after:
no goals
Theorem: TopM_mapDenoteRegion_nil
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
⊢ TopM.mapDenoteRegion Δ [] = []
Tactic:
simp[TopM.mapDenoteRegion]
Proof state after:
no goals
Theorem: OpM_denoteRegions_cons
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
r : Region Δ
rs : List (Region Δ)
ix : ℕ
⊢ OpM.denoteRegions (r :: rs) ix = OpM.denoteRegion r ix :: OpM.denoteRegions rs (ix + 1)
Tactic:
simp[OpM.denoteRegions]
Proof state after:
no goals
Theorem: OpM_denoteRegions_nil
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
ix : ℕ
⊢ OpM.denoteRegions [] ix = []
Tactic:
simp[OpM.denoteRegions]
Proof state after:
no goals
Theorem: run_TopM_denoteRegionsByIx_cons
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
ix : ℕ
r : TypedArgs Δ → TopM Δ (TypedArgs Δ)
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
args : TypedArgs Δ
env : SSAEnv Δ
⊢ run (TopM.denoteRegionsByIx (r :: rs) ix args) env =
    run
      (match ix with
      | 0 => r args
      | Nat.succ ix' => TopM.denoteRegionsByIx rs ix' args)
      env
Tactic:
simp[TopM.denoteRegionsByIx]
Proof state after:
no goals
Theorem: Fitree.bind_ret'
Proof state before:
E✝ : Type → Type
R✝ : Type
t : Fitree E✝ R✝
⊢ (bind t fun r => ret r) = t
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.bind_ret'
Proof state before:
case Ret
E✝ : Type → Type
R✝ : Type
r✝ : R✝
⊢ (bind (Ret r✝) fun r => ret r) = Ret r✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Fitree.bind_ret'
Proof state before:
case Vis
E✝ : Type → Type
R✝ T✝ : Type
e✝ : E✝ T✝
k✝ : T✝ → Fitree E✝ R✝
ih : ∀ (a : T✝), (bind (k✝ a) fun r => ret r) = k✝ a
⊢ (bind (Vis e✝ k✝) fun r => ret r) = Vis e✝ k✝
Tactic:
simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.bind_Ret'
Proof state before:
E✝ : Type → Type
R✝ : Type
t : Fitree E✝ R✝
⊢ (bind t fun r => Ret r) = t
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.bind_Ret'
Proof state before:
case Ret
E✝ : Type → Type
R✝ : Type
r✝ : R✝
⊢ (bind (Ret r✝) fun r => Ret r) = Ret r✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Fitree.bind_Ret'
Proof state before:
case Vis
E✝ : Type → Type
R✝ T✝ : Type
e✝ : E✝ T✝
k✝ : T✝ → Fitree E✝ R✝
ih : ∀ (a : T✝), (bind (k✝ a) fun r => Ret r) = k✝ a
⊢ (bind (Vis e✝ k✝) fun r => Ret r) = Vis e✝ k✝
Tactic:
simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.bind_bind
Proof state before:
E✝ : Type → Type
R✝² : Type
t : Fitree E✝ R✝²
R✝¹ : Type
k : R✝² → Fitree E✝ R✝¹
R✝ : Type
k' : R✝¹ → Fitree E✝ R✝
⊢ bind (bind t k) k' = bind t fun x => bind (k x) k'
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.bind_bind
Proof state before:
case Ret
E✝ : Type → Type
R✝² R✝¹ : Type
k : R✝² → Fitree E✝ R✝¹
R✝ : Type
k' : R✝¹ → Fitree E✝ R✝
r✝ : R✝²
⊢ bind (bind (Ret r✝) k) k' = bind (Ret r✝) fun x => bind (k x) k'
Tactic:
rfl
Proof state after:
no goals
Theorem: Fitree.bind_bind
Proof state before:
case Vis
E✝ : Type → Type
R✝² R✝¹ : Type
k : R✝² → Fitree E✝ R✝¹
R✝ : Type
k' : R✝¹ → Fitree E✝ R✝
T✝ : Type
e✝ : E✝ T✝
k✝ : T✝ → Fitree E✝ R✝²
ih : ∀ (a : T✝), bind (bind (k✝ a) k) k' = bind (k✝ a) fun x => bind (k x) k'
⊢ bind (bind (Vis e✝ k✝) k) k' = bind (Vis e✝ k✝) fun x => bind (k x) k'
Tactic:
simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.interp_bind
Proof state before:
E✝¹ E✝ : Type → Type
h : E✝¹ ~> Fitree E✝
R✝¹ : Type
t : Fitree E✝¹ R✝¹
R✝ : Type
k : R✝¹ → Fitree E✝¹ R✝
⊢ interp h (bind t k) = bind (interp h t) fun x => interp h (k x)
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.interp_bind
Proof state before:
case Ret
E✝¹ E✝ : Type → Type
h : E✝¹ ~> Fitree E✝
R✝¹ R✝ : Type
k : R✝¹ → Fitree E✝¹ R✝
r✝ : R✝¹
⊢ interp h (bind (Ret r✝) k) = bind (interp h (Ret r✝)) fun x => interp h (k x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Fitree.interp_bind
Proof state before:
case Vis
E✝¹ E✝ : Type → Type
h : E✝¹ ~> Fitree E✝
R✝¹ R✝ : Type
k : R✝¹ → Fitree E✝¹ R✝
T✝ : Type
e✝ : E✝¹ T✝
k✝ : T✝ → Fitree E✝¹ R✝¹
ih : ∀ (a : T✝), interp h (bind (k✝ a) k) = bind (interp h (k✝ a)) fun x => interp h (k x)
⊢ interp h (bind (Vis e✝ k✝) k) = bind (interp h (Vis e✝ k✝)) fun x => interp h (k x)
Tactic:
simp [bind, ih]
Proof state after:
no goals
Theorem: Fitree.interp'_bind
Proof state before:
E✝ : Type → Type
h : E✝ ~> Fitree Void1
F✝ : Type → Type
R✝¹ : Type
t : Fitree (E✝ +' F✝) R✝¹
R✝ : Type
k : R✝¹ → Fitree (E✝ +' F✝) R✝
⊢ interp' h (bind t k) = bind (interp' h t) fun x => interp' h (k x)
Tactic:
simp [interp', interp_bind]
Proof state after:
no goals