Resume proof in IO monad

Stream: lean4

[Leni Aniva]

This is a curious thing I found out about CoreM vs IO monads. I'm executing a proof procedurally using a mechanism similar to LeanGym's TermElabM:

def proof_term_elab: M IO Unit := do
  let context ← read
  let env := context.env
  let (_, _) ← term_elab_layer <| do
    let expr ← parse_expr env "∀ (p q: Prop), p ∨ q → q ∨ p"
    let state ← start_tactic_state expr
    let state ← execute_tactic env state "intro p q h"
    let state ← execute_tactic env state "cases h"
    let _ ← execute_tactic env state "apply Or.inr"
  IO.println "Completed"

Here the states are just Lean.Elab.Tactic.States and

def start_tactic_state (expr: Lean.Expr): Lean.Elab.TermElabM Lean.Elab.Tactic.SavedState
def execute_tactic (env: Lean.Environment) (state: Lean.Elab.Tactic.SavedState) (tactic: String): Lean.Elab.TermElabM Lean.Elab.Tactic.SavedState

This works well. Then I tried to execute the state monads until I got to IO:

def Context.to_io (context: Context) (termElabM: Lean.Elab.TermElabM α): IO α := do
  let metaM : Lean.MetaM α := termElabM.run' (ctx := context.elabContext)
  let coreM : Lean.CoreM α := metaM.run'
  let coreState : Lean.Core.State := { env := context.env }
  let (ret, _) <- coreM.toIO context.coreContext coreState
  return ret

def proof_io: M IO Unit := do
  let context ← read
  let env := context.env
  let expr ← context.to_io <| parse_expr env "∀ (p q: Prop), p ∨ q → q ∨ p"
  let state ← context.to_io <| start_tactic_state expr
  let state ← context.to_io <| execute_tactic env state "intro p q h"
  let state ← context.to_io <| execute_tactic env state "cases h"
  let _ ← context.to_io <| execute_tactic env state "apply Or.inr"
  IO.println "Completed"

Now the same proof doesn't work anymore and it fails at the last step with the message

tactic 'apply' failed, failed to unify
  ?a ∨ ?b
with
  q ∨ p
case inl
p q : Prop
h✝ : p
⊢ q ∨ p

It seems like coreState saves some information that makes this unification possible. What information is being stored here?

[Mario Carneiro]

yes, you should not discard the core state, this will definitely not work

[Mario Carneiro]

it should be part of the "state"

[Mario Carneiro]

do you have a #mwe?

[Leni Aniva]

Mario Carneiro said:

do you have a #mwe?

Yes. https://pastebin.com/tEN0MnMp (the coreM/IO cases I have described are at the bottom of the file)

[Mario Carneiro]

the example doesn't seem to have any errors

[Mario Carneiro]

this code seems to be a bit lower level than it should be, if you set up all of these states from scratch there is a high probability you will break some invariants

[Leni Aniva]

Mario Carneiro said:

the example doesn't seem to have any errors

yeah but if you replace proof_term_elab with proof_io it errors

[Leni Aniva]

I just tested if the Lean.Core.State is saved after coreM.toIO run then the error goes away, but I want to know what is causing the error

[Mario Carneiro]

you are discarding the state, this stores the result of e.g. the mvar assignments performed by previous steps

[Leni Aniva]

Mario Carneiro said:

you are discarding the state, this stores the result of e.g. the mvar assignments performed by previous steps

Thanks! That answered my question