internlm/Lean-Github huggingface dataset:
Theorem: run_seq
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
out : Unit × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ (do
      let p ← Except.ok out
      StateT.run mb p.snd) =
    match Except.ok out with
    | Except.ok (PUnit.unit, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
simp[H, bind, Except.bind]
Proof state after:
no goals
Theorem: run_bind
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ run
      (do
        let a ← ma
        k a)
      env =
    match run ma env with
    | Except.ok (a, env') => run (k a) env'
    | Except.error e => Except.error e
Tactic:
simp[run]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ (do
      let p ← StateT.run ma env
      StateT.run (k p.fst) p.snd) =
    match StateT.run ma env with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Theorem: run_bind
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ (do
      let p ← StateT.run ma env
      StateT.run (k p.fst) p.snd) =
    match StateT.run ma env with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
cases H : StateT.run ma env
Proof state after:
case error
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
a✝ : String × SSAEnv Δ
H : StateT.run ma env = Except.error a✝
⊢ (do
      let p ← Except.error a✝
      StateT.run (k p.fst) p.snd) =
    match Except.error a✝ with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e

case ok
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
a✝ : a × SSAEnv Δ
H : StateT.run ma env = Except.ok a✝
⊢ (do
      let p ← Except.ok a✝
      StateT.run (k p.fst) p.snd) =
    match Except.ok a✝ with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Theorem: run_bind
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run (k p.fst) p.snd) =
    match Except.error err with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
case error err => {
  simp[H];
  simp[bind, Except.bind];
}
Proof state after:
no goals
Theorem: run_bind
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ (do
      let p ← Except.ok out
      StateT.run (k p.fst) p.snd) =
    match Except.ok out with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
case ok out => {
  simp[H, bind, Except.bind];
}
Proof state after:
no goals
Theorem: run_bind
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run (k p.fst) p.snd) =
    match Except.error err with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
simp[H]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run (k p.fst) p.snd) =
    Except.error err
Theorem: run_bind
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run (k p.fst) p.snd) =
    Except.error err
Tactic:
simp[bind, Except.bind]
Proof state after:
no goals
Theorem: run_bind
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ (do
      let p ← Except.ok out
      StateT.run (k p.fst) p.snd) =
    match Except.ok out with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
simp[H, bind, Except.bind]
Proof state after:
no goals
Theorem: run_bind2
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ run (StateT.bind ma k) env =
    match run ma env with
    | Except.ok (a, env') => run (k a) env'
    | Except.error e => Except.error e
Tactic:
simp[run, TopM.bind]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ StateT.run (StateT.bind ma k) env =
    match StateT.run ma env with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Theorem: run_bind2
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ StateT.run (StateT.bind ma k) env =
    match StateT.run ma env with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
cases H : StateT.run ma env
Proof state after:
case error
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
a✝ : String × SSAEnv Δ
H : StateT.run ma env = Except.error a✝
⊢ StateT.run (StateT.bind ma k) env =
    match Except.error a✝ with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e

case ok
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
a✝ : a × SSAEnv Δ
H : StateT.run ma env = Except.ok a✝
⊢ StateT.run (StateT.bind ma k) env =
    match Except.ok a✝ with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Theorem: run_bind2
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ StateT.run (StateT.bind ma k) env =
    match Except.error err with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
case error err => {
  simp[bind, Except.bind, StateT.bind, StateT.run] at *;
  simp[H];
}
Proof state after:
no goals
Theorem: run_bind2
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ StateT.run (StateT.bind ma k) env =
    match Except.ok out with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
case ok out => {
  simp[bind, Except.bind, StateT.bind, StateT.run] at *;
  simp[H];
}
Proof state after:
no goals
Theorem: run_bind2
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ StateT.run (StateT.bind ma k) env =
    match Except.error err with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
simp[bind, Except.bind, StateT.bind, StateT.run] at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : ma env = Except.error err
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => k v.fst v.snd) =
    Except.error err
Theorem: run_bind2
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : ma env = Except.error err
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => k v.fst v.snd) =
    Except.error err
Tactic:
simp[H]
Proof state after:
no goals
Theorem: run_bind2
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ StateT.run (StateT.bind ma k) env =
    match Except.ok out with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
simp[bind, Except.bind, StateT.bind, StateT.run] at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : ma env = Except.ok out
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => k v.fst v.snd) =
    k out.fst out.snd
Theorem: run_bind2
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : ma env = Except.ok out
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => k v.fst v.snd) =
    k out.fst out.snd
Tactic:
simp[H]
Proof state after:
no goals
Theorem: run_bind3
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ run (StateT.bind ma fun x => k x) env =
    match run ma env with
    | Except.ok (a, env') => run (k a) env'
    | Except.error e => Except.error e
Tactic:
simp[run, TopM.bind]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ StateT.run (StateT.bind ma fun x => k x) env =
    match StateT.run ma env with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Theorem: run_bind3
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ StateT.run (StateT.bind ma fun x => k x) env =
    match StateT.run ma env with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
cases H : StateT.run ma env
Proof state after:
case error
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
a✝ : String × SSAEnv Δ
H : StateT.run ma env = Except.error a✝
⊢ StateT.run (StateT.bind ma fun x => k x) env =
    match Except.error a✝ with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e

case ok
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
a✝ : a × SSAEnv Δ
H : StateT.run ma env = Except.ok a✝
⊢ StateT.run (StateT.bind ma fun x => k x) env =
    match Except.ok a✝ with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Theorem: run_bind3
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ StateT.run (StateT.bind ma fun x => k x) env =
    match Except.error err with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
case error err => {
  simp[bind, Except.bind, StateT.bind, StateT.run] at *;
  simp[H];
}
Proof state after:
no goals
Theorem: run_bind3
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ StateT.run (StateT.bind ma fun x => k x) env =
    match Except.ok out with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
case ok out => {
  simp[bind, Except.bind, StateT.bind, StateT.run] at *;
  simp[H];
}
Proof state after:
no goals
Theorem: run_bind3
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ StateT.run (StateT.bind ma fun x => k x) env =
    match Except.error err with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
simp[bind, Except.bind, StateT.bind, StateT.run] at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : ma env = Except.error err
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => k v.fst v.snd) =
    Except.error err
Theorem: run_bind3
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : ma env = Except.error err
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => k v.fst v.snd) =
    Except.error err
Tactic:
simp[H]
Proof state after:
no goals
Theorem: run_bind3
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ StateT.run (StateT.bind ma fun x => k x) env =
    match Except.ok out with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
Tactic:
simp[bind, Except.bind, StateT.bind, StateT.run] at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : ma env = Except.ok out
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => k v.fst v.snd) =
    k out.fst out.snd
Theorem: run_bind3
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : ma env = Except.ok out
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => k v.fst v.snd) =
    k out.fst out.snd
Tactic:
simp[H]
Proof state after:
no goals
Theorem: run_bind_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
⊢ run
      (do
        let __discr ← ma
        let x : a := __discr
        mb)
      env =
    match run ma env with
    | Except.ok (a_, env') => run mb env'
    | Except.error e => Except.error e
Tactic:
simp[run]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
⊢ (do
      let p ← StateT.run ma env
      StateT.run mb p.snd) =
    match StateT.run ma env with
    | Except.ok (a_, env') => StateT.run mb env'
    | Except.error e => Except.error e
Theorem: run_bind_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
⊢ (do
      let p ← StateT.run ma env
      StateT.run mb p.snd) =
    match StateT.run ma env with
    | Except.ok (a_, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
cases H : StateT.run ma env
Proof state after:
case error
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
a✝ : String × SSAEnv Δ
H : StateT.run ma env = Except.error a✝
⊢ (do
      let p ← Except.error a✝
      StateT.run mb p.snd) =
    match Except.error a✝ with
    | Except.ok (a_, env') => StateT.run mb env'
    | Except.error e => Except.error e

case ok
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
a✝ : a × SSAEnv Δ
H : StateT.run ma env = Except.ok a✝
⊢ (do
      let p ← Except.ok a✝
      StateT.run mb p.snd) =
    match Except.ok a✝ with
    | Except.ok (a_, env') => StateT.run mb env'
    | Except.error e => Except.error e
Theorem: run_bind_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run mb p.snd) =
    match Except.error err with
    | Except.ok (a_, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
case error err => {
  simp[H];
  simp[bind, Except.bind];
}
Proof state after:
no goals
Theorem: run_bind_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ (do
      let p ← Except.ok out
      StateT.run mb p.snd) =
    match Except.ok out with
    | Except.ok (a_, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
case ok out => {
  simp[H, bind, Except.bind];
}
Proof state after:
no goals
Theorem: run_bind_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run mb p.snd) =
    match Except.error err with
    | Except.ok (a_, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
simp[H]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run mb p.snd) =
    Except.error err
Theorem: run_bind_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run mb p.snd) =
    Except.error err
Tactic:
simp[bind, Except.bind]
Proof state after:
no goals
Theorem: run_bind_
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
mb : TopM Δ b
env : SSAEnv Δ
out : a × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ (do
      let p ← Except.ok out
      StateT.run mb p.snd) =
    match Except.ok out with
    | Except.ok (a_, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
simp[H, bind, Except.bind]
Proof state after:
no goals
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 (ma >>= a2mb) env = run (a2mb va) env'
Tactic:
simp[bind, StateT.bind, Except.bind]
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')
⊢ 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'