Simulating proof branching in TermElabM

Stream: lean4

[Leni Aniva]

There are two ways to write this proof:

example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  cases h
  apply Or.inr
  assumption
  apply Or.inl
  assumption
example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  cases h
  . apply Or.inr
    assumption
  . apply Or.inl
    assumption

and I want to simulate this using TermElabM so the proof can be fed into the machine procedurally. My tactic execution function is this one (I have a MWE)

  let tac : Lean.Elab.Tactic.TacticM Unit := set state.tactic *> Lean.Elab.Tactic.evalTactic stx
  let mvarId := state.tactic.goals.get! goalId
  Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let unsolvedGoals ← Lean.Elab.Tactic.run mvarId tac
  if (← getThe Lean.Core.State).messages.hasErrors then
    let messages := (← getThe Lean.Core.State).messages |>.toList.toArray
    let errors ← (messages.map Lean.Message.data).mapM fun md => md.toString
    IO.println s!"{errors}"
    return state
  else
    unsolvedGoals.forM Lean.instantiateMVarDeclMVars
    let nextState : Lean.Elab.Tactic.SavedState := {
      term := (← Lean.Elab.Term.saveState),
      tactic := { goals := unsolvedGoals }
    }
    let goals ← unsolvedGoals.mapM fun g => do pure $ toString (← Lean.Meta.ppGoal g)
    IO.println s!"Tactic '{tactic}' succeeded."
    IO.println s!"{goals}"
    return nextState

Here goalId specifies which goal should the tactic be run on. However when I ran apply Or.inr on cases h's first goal, the other goal also shows up:

def proof: M IO Unit := do
  let context ← read
  let env := context.env
  let (_, _) ← execute_term_elab <| 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 0 "intro p q h"
    let branch ← execute_tactic env state 0 "cases h"
    -- First branch
    let state ← execute_tactic env branch 0 "apply Or.inr"
    let _ ← execute_tactic env state 0 "assumption"
    -- Second branch
    let state ← execute_tactic env branch 1 "apply Or.inl"
    let _ ← execute_tactic env state 0 "assumption"
  IO.println "Completed"

the line of Or.inr prints

Tactic 'apply Or.inr' succeeded.
[case inl.h
p q : Prop
h✝ : p
⊢ p, case inr
p q : Prop
h✝ : q
⊢ q ∨ p]

Is there a way to apply the tactic to only the first goal? Ideally after the assumption tactic the proof branch should be concluded with no more goals.

[Leni Aniva]

MWE: https://pastebin.com/wVGxLvsz

[Mario Carneiro]

Here's how I would set up the equivalent of your other MWE:

import Lean

open Lean Elab Term Meta

def start_tactic_state (goal : String)
    (x : Tactic.SavedState → Tactic.TacticM Unit) : CoreM Unit := do
  MetaM.run' <| TermElabM.run' <| do
  let .ok syn := Parser.runParserCategory (← getEnv) `term goal (fileName := "<stdin>") | failure
  let expr ← elabType syn
  synthesizeSyntheticMVarsNoPostponing
  let expr ← instantiateMVars expr
  let goals ← Tactic.run (← mkFreshExprMVar expr).mvarId! do
      IO.println "Tactic state started"
      x (← saveState)
  if goals.isEmpty then
    IO.println "goals accomplished"
  else
    let goals ← goals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
    IO.println s!"goals not solved: {goals}"

def execute_tactic (state : Tactic.SavedState) (tactic : String) :
    Tactic.TacticM Tactic.SavedState := do
  state.restore
  let .ok stx :=
    Parser.runParserCategory (← getEnv) `tactic tactic (fileName := "<stdin>") | failure
  try
    Tactic.evalTactic stx
  catch e =>
    IO.println s!"{← e.toMessageData.toString}"
    return state
  if (← getThe Core.State).messages.hasErrors then
    let messages := (← getThe Core.State).messages |>.toList.toArray
    let errors ← (messages.map Message.data).mapM fun md => md.toString
    IO.println s!"{errors}"
    return state
  let unsolvedGoals ← Tactic.getUnsolvedGoals
  let goals ← unsolvedGoals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
  IO.println s!"Tactic succeeded with goals {goals}"
  saveState

def proof_term_elab: CoreM Unit := do
  start_tactic_state "∀ (p q: Prop), p ∨ q → q ∨ p" fun state => do
    let state ← execute_tactic state "intro p q h"
    let state ← execute_tactic state "cases h"
    let _ ← execute_tactic state "apply Or.inr"

#eval do
  let env ← importModules
    (imports := [{ module := Name.str .anonymous "Init", runtimeOnly := false }])
    (opts := {})
    (trustLevel := 1)
  let coreContext : Core.Context := {
    currNamespace := Name.anonymous,
    openDecls := [],     -- No 'open' directives needed
    fileName := "<onion>",
    fileMap := { source := "", positions := #[0], lines := #[1] }
  }
  discard <| proof_term_elab.toIO coreContext { env := env }

[Mario Carneiro]

@Leni V. Aniva said:

def proof: M IO Unit := do
  let context ← read
  let env := context.env
  let (_, _) ← execute_term_elab <| 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 0 "intro p q h"
    let branch ← execute_tactic env state 0 "cases h"
    -- First branch
    let state ← execute_tactic env branch 0 "apply Or.inr"
    let _ ← execute_tactic env state 0 "assumption"
    -- Second branch
    let state ← execute_tactic env branch 1 "apply Or.inl"
    let _ ← execute_tactic env state 0 "assumption"
  IO.println "Completed"

This code seems to indicate a misunderstanding regarding what state is. What you are doing here is attempting to apply Or.inr and assumption, then undoing and trying Or.inl and assumption instead. Both versions apply to the first goal

[Mario Carneiro]

If you want to work on multiple subgoals (without undoing tactics after e.g. a failure or incorrect choice), you need to manipulate the goals array. You may or may not want to expose it as an argument to execute_tactic

[Leni Aniva]

Mario Carneiro said:

If you want to work on multiple subgoals (without undoing tactics after e.g. a failure or incorrect choice), you need to manipulate the goals array. You may or may not want to expose it as an argument to execute_tactic

That would be even more convenient. Thanks! I can look into this

[Mario Carneiro]

Tactics in MetaM generally explicitly pass subgoals around (they accept a MVarId as input and return a List MVarId), while tactics in TacticM generally don't (they get and set the goals stored in the monad state)

[Leni Aniva]

Mario Carneiro said:

Tactics in MetaM generally explicitly pass subgoals around (they accept a MVarId as input and return a List MVarId), while tactics in TacticM generally don't (they get and set the goals stored in the monad state)

Can TacticM be directly lifted to CoreM?

[Mario Carneiro]

you really should not do that, see the code I posted

[Mario Carneiro]

the start_tactic_state code lifts a TacticM to CoreM, but importantly it scopes over the entire proof

[Mario Carneiro]

if you do fine grained lifting of each tactic separately you will lose track of important state

[Leni Aniva]

Mario Carneiro said:

if you do fine grained lifting of each tactic separately you will lose track of important state

is that state stored in CoreM or TacticM only?

[Mario Carneiro]

TacticM is a monad stack on top of TermElabM on MetaM on CoreM and all of them add more state

[Mario Carneiro]

you can probably get by with MetaM for the overall proof state, although some minor things won't persist across commands, but anything below that will cause metavariables to be forgotten and other bad things

[Leni Aniva]

Mario Carneiro said:

you can probably get by with MetaM for the overall proof state, although some minor things won't persist across commands, but anything below that will cause metavariables to be forgotten and other bad things

It seems like I just need the Lean.Core.State in CoreM for metavariables in the simpler example to not be forgotten. Is there anything else to watch out for in the states of TermElabM and MetaM?

[Mario Carneiro]

Is there a reason you need to do this? These are implementation details of lean and if you depend on them your code will break frequently

[Leni Aniva]

Mario Carneiro said:

Is there a reason you need to do this? These are implementation details of lean and if you depend on them your code will break frequently

I want to be able to backtrack to an earlier state in the proof and if the overall program state carries the same monad as it backtracks it may produce different behaviour

[Mario Carneiro]

The usual mechanisms for backtracking have the desired behavior already. You will not get an airtight guarantee regardless because tactics can use IO refs or other shenanigans, but tactics should basically be reproducible if you use saveState and restore to roll back the state

[Mario Carneiro]

There are some things like the name generator that are never reset

[Leni Aniva]

Mario Carneiro said:

The usual mechanisms for backtracking have the desired behavior already. You will not get an airtight guarantee regardless because tactics can use IO refs or other shenanigans, but tactics should basically be reproducible if you use saveState and restore to roll back the state

Thanks! I'll try this

[Leni Aniva]

If I use the same TacticM monad everywhere would it still be possible to add more definitions into the environment on the fly?

[Mario Carneiro]

you can get and set the environment explicitly

[Mario Carneiro]

if you want to add a definition, just call addDecl, if you want to undo the addition use getEnv beforehand and setEnv afterward

[Leni Aniva]

Mario Carneiro said:

Here's how I would set up the equivalent of your other MWE:

import Lean

open Lean Elab Term Meta

def start_tactic_state (goal : String)
    (x : Tactic.SavedState → Tactic.TacticM Unit) : CoreM Unit := do
  MetaM.run' <| TermElabM.run' <| do
  let .ok syn := Parser.runParserCategory (← getEnv) `term goal (fileName := "<stdin>") | failure
  let expr ← elabType syn
  synthesizeSyntheticMVarsNoPostponing
  let expr ← instantiateMVars expr
  let goals ← Tactic.run (← mkFreshExprMVar expr).mvarId! do
      IO.println "Tactic state started"
      x (← saveState)
  if goals.isEmpty then
    IO.println "goals accomplished"
  else
    let goals ← goals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
    IO.println s!"goals not solved: {goals}"

def execute_tactic (state : Tactic.SavedState) (tactic : String) :
    Tactic.TacticM Tactic.SavedState := do
  state.restore
  let .ok stx :=
    Parser.runParserCategory (← getEnv) `tactic tactic (fileName := "<stdin>") | failure
  try
    Tactic.evalTactic stx
  catch e =>
    IO.println s!"{← e.toMessageData.toString}"
    return state
  if (← getThe Core.State).messages.hasErrors then
    let messages := (← getThe Core.State).messages |>.toList.toArray
    let errors ← (messages.map Message.data).mapM fun md => md.toString
    IO.println s!"{errors}"
    return state
  let unsolvedGoals ← Tactic.getUnsolvedGoals
  let goals ← unsolvedGoals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
  IO.println s!"Tactic succeeded with goals {goals}"
  saveState

def proof_term_elab: CoreM Unit := do
  start_tactic_state "∀ (p q: Prop), p ∨ q → q ∨ p" fun state => do
    let state ← execute_tactic state "intro p q h"
    let state ← execute_tactic state "cases h"
    let _ ← execute_tactic state "apply Or.inr"

#eval do
  let env ← importModules
    (imports := [{ module := Name.str .anonymous "Init", runtimeOnly := false }])
    (opts := {})
    (trustLevel := 1)
  let coreContext : Core.Context := {
    currNamespace := Name.anonymous,
    openDecls := [],     -- No 'open' directives needed
    fileName := "<onion>",
    fileMap := { source := "", positions := #[0], lines := #[1] }
  }
  discard <| proof_term_elab.toIO coreContext { env := env }

When I ran this script for some reason it still shows 2 goals in the apply Or.inr branch? I added

def proof_term_elab: CoreM Unit := do
  start_tactic_state "∀ (p q: Prop), p ∨ q → q ∨ p" fun state => do
    let state ← execute_tactic state "intro p q h"
    let state ← execute_tactic state "cases h"
    let state ← execute_tactic state "apply Or.inr"
    let state ← execute_tactic state "assumption"

and the assumption should finish the Or.inr branch but it doesn't:

Tactic state started
Tactic succeeded with goals [p q : Prop
h : p ∨ q
⊢ q ∨ p]
Tactic succeeded with goals [case inl
p q : Prop
h✝ : p
⊢ q ∨ p, case inr
p q : Prop
h✝ : q
⊢ q ∨ p]
Tactic succeeded with goals [case inl.h
p q : Prop
h✝ : p
⊢ p, case inr
p q : Prop
h✝ : q
⊢ q ∨ p]
Tactic succeeded with goals [case inr
p q : Prop
h✝ : q
⊢ q ∨ p]
goals not solved: [case inr
p q : Prop
h✝ : q
⊢ q ∨ p]

am I missing something here?

[Mario Carneiro]

I don't see an issue here. You just wrote the equivalent of:

example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  cases h
  apply Or.inr
  assumption

and there is one goal remaining at the end

[Leni Aniva]

Mario Carneiro said:

I don't see an issue here. You just wrote the equivalent of:

example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  cases h
  apply Or.inr
  assumption

and there is one goal remaining at the end

I want the second version since it has proof branching

  intro p q h
  cases h
  . apply Or.inr
    assumption
  . apply Or.inl
    assumption

[Mario Carneiro]

That code has proof branching

[Mario Carneiro]

it just isn't using . for focusing on subgoals (i.e. "structured proofs")

[Mario Carneiro]

you can finish the proof if you do

example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  cases h
  apply Or.inr
  assumption
  apply Or.inl
  assumption

[Leni Aniva]

How can I simulate . then?

[Mario Carneiro]

what interface do you want for that? . isn't a tactic, it is a tactic combinator and you have to put something after it

[Leni Aniva]

Mario Carneiro said:

what interface do you want for that? . isn't a tactic, it is a tactic combinator and you have to put something after it

I just want to be able to do something like this

    let expr ← parse_expr env "∀ (p q: Prop), p ∨ q → q ∨ p"
    let state ← start_tactic_state expr
    let state ← execute_tactic env state 0 "intro p q h"
    let branch ← execute_tactic env state 0 "cases h"
    -- First branch
    let state ← execute_tactic env branch 0 "apply Or.inr"
    let _ ← execute_tactic env state 0 "assumption" -- state has no goals
    -- Second branch
    let state ← execute_tactic env branch 1 "apply Or.inl"
    let _ ← execute_tactic env state 0 "assumption" -- state has no goals

[Mario Carneiro]

How about this:

def start_tactic_state (goal : String)
    (x : Tactic.SavedState → MVarId → Tactic.TacticM Unit) : CoreM Unit := do
  MetaM.run' <| TermElabM.run' <| do
  let .ok syn := Parser.runParserCategory (← getEnv) `term goal (fileName := "<stdin>") | failure
  let expr ← elabType syn
  synthesizeSyntheticMVarsNoPostponing
  let expr ← instantiateMVars expr
  let g := (← mkFreshExprMVar expr).mvarId!
  let goals ← Tactic.run g do
      IO.println "Tactic state started"
      x (← saveState) g
  if goals.isEmpty then
    IO.println "goals accomplished"
  else
    let goals ← goals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
    IO.println s!"goals not solved: {goals}"

def execute_tactic (state : Tactic.SavedState) (g : MVarId) (tactic : String) :
    Tactic.TacticM (Tactic.SavedState × List MVarId) := do
  state.restore
  Tactic.setGoals [g]
  let .ok stx :=
    Parser.runParserCategory (← getEnv) `tactic tactic (fileName := "<stdin>") | failure
  try
    Tactic.evalTactic stx
  catch e =>
    IO.println s!"{← e.toMessageData.toString}"
    return (state, [g])
  if (← getThe Core.State).messages.hasErrors then
    let messages := (← getThe Core.State).messages |>.toList.toArray
    let errors ← (messages.map Message.data).mapM fun md => md.toString
    IO.println s!"{errors}"
    return (state, [g])
  let unsolvedGoals ← Tactic.getUnsolvedGoals
  let goals ← unsolvedGoals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
  IO.println s!"Tactic succeeded with goals {goals}"
  return (← saveState, unsolvedGoals)

def proof_term_elab: CoreM Unit := do
  start_tactic_state "∀ (p q: Prop), p ∨ q → q ∨ p" fun state g => do
    let (state, [g]) ← execute_tactic state g "intro p q h" | failure
    let (state, [g1, g2]) ← execute_tactic state g "cases h" | failure
    let (state, [g1]) ← execute_tactic state g1 "apply Or.inr" | failure
    let (state, []) ← execute_tactic state g1 "assumption" | failure
    let (state, [g2]) ← execute_tactic state g2 "apply Or.inl" | failure
    let (_, []) ← execute_tactic state g2 "assumption" | failure

[Mario Carneiro]

oh you could also do indexes

[Leni Aniva]

set goals would be cool

[Leni Aniva]

what is the purpose of passing down the state here if the goals already represent the proof state?

[Mario Carneiro]

you aren't doing any backtracking in this proof but you could use it to do so

[Mario Carneiro]

backtracking meaning applying things that are wrong and then going back to an earlier point in the proof, which is distinct from working on separate subgoals

[Leni Aniva]

Mario Carneiro said:

backtracking meaning applying things that are wrong and then going back to an earlier point in the proof, which is distinct from working on separate subgoals

do you have an example of backtracking (just in normal lean not TacticM)

[Mario Carneiro]

that would not normally end up in a completed user proof unless they are using try or repeat, but it could certainly appear in a proof search

[Mario Carneiro]

example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  cases h
  all_goals
    first
    | apply Or.inl
      assumption
    | apply Or.inr
      assumption

[Mario Carneiro]

there is backtracking in this proof, because for the first subgoal we will first try apply Or.inl which succeeds but results in an unprovable goal, then assumption which fails, and then first will try the other branch from the original state, doing apply Or.inr and assumption

[Leni Aniva]

Thanks! That was very helpful

[Leni Aniva]

Also is there anything that I should watch out for if I abandon a proof while inside a TacticM construct to start on another proof?

[Mario Carneiro]

Here's the equivalent of that proof using the strings version:

def proof_term_elab: CoreM Unit := do
  start_tactic_state "∀ (p q: Prop), p ∨ q → q ∨ p" fun state g => do
    let (state, [g]) ← execute_tactic state g "intro p q h" | failure
    let (state, [g1, g2]) ← execute_tactic state g "cases h" | failure
    let tryIt state g := do
      try
        let (state, [g]) ← execute_tactic state g "apply Or.inl" | failure
        let (state, []) ← execute_tactic state g "assumption" | failure
        pure state
      catch _ =>
        let (state, [g]) ← execute_tactic state g "apply Or.inr" | failure
        let (state, []) ← execute_tactic state g "assumption" | failure
        pure state
    let state ← tryIt state g1
    let _ ← tryIt state g2

[Mario Carneiro]

Leni V. Aniva said:

Also is there anything that I should watch out for if I abandon a proof while inside a TacticM construct to start on another proof?

I don't think so

[Daniel Donnelly]

(deleted)