proof mode: split out tactics into separate commands

Stream: general

[Mario Carneiro]

Mario Carneiro said:

But if lean had a proof mode like HOL light's e(...) steps broken out as separate lean commands then you would certainly get back the speed benefits you are seeing in HOL Light

Mario Carneiro said:

now I think I want to try to demo something like that in lean

Here's what I was talking about @D. J. Bernstein : This is a prototype implementation of a "proof mode" in which you can save the context of a proof in a by block by writing start_proof, and then you can start writing tactics in separate commands thereafter using ## before each tactic (or group of tactics). Because lean automatically snapshots between commands, you get the benefits of a line-by-line proof like in Coq or HOL light in terms of general responsiveness. This may be considered as an alternative to the save tactic, which tries to do something similar but without linearizing the AST structure.

[Mario Carneiro]

Mathlib.Tactic.ProofMode:

import Lean
open Lean

structure ProofState where
  tacCtx : Elab.Tactic.Context
  tacState : Elab.Tactic.State
  termCtx : Elab.Term.Context
  termState : Elab.Term.State
  metaCtx : Meta.Context
  metaState : Meta.State

def ProofState.get : Elab.Tactic.TacticM ProofState :=
  fun tacCtx tacState termCtx termState metaCtx metaState => do
    let tacState ← tacState.get
    let termState ← termState.get
    let metaState ← metaState.get
    return { tacCtx, tacState, termCtx, termState, metaCtx, metaState }

def ProofState.with : ProofState → Elab.Tactic.TacticM α → CoreM α :=
  fun { tacCtx, tacState, termCtx, termState, metaCtx, metaState } x => do
    let tacState ← IO.mkRef tacState
    let termState ← IO.mkRef termState
    let metaState ← IO.mkRef metaState
    x tacCtx tacState termCtx termState metaCtx metaState

initialize proofStateExt : EnvExtension (List ProofState) ← registerEnvExtension (pure [])

elab "start_proof" : tactic => do
  let state ← ProofState.get
  modifyEnv (proofStateExt.modifyState · (state :: ·))
  Elab.Tactic.evalTactic (← `(tactic| repeat sorry))

elab tk:"##" tac:(tacticSeq)? : command => do
  let state :: rest := proofStateExt.getState (← getEnv)
    | throwError "proof mode not started, use `start_proof`"
  Elab.Command.liftTermElabM do
    state.with do
      Elab.Tactic.withTacticInfoContext tk do
        if let some tac := tac then
          Elab.Tactic.evalTactic tac
      if (← Elab.Tactic.getUnsolvedGoals).isEmpty then
        logInfoAt tk "Goals accomplished 🎉"
        modifyEnv (proofStateExt.setState · rest)
      else
        modifyEnv (proofStateExt.setState · ((← ProofState.get) :: rest))

[Mario Carneiro]

test file:

import Mathlib.Tactic.ProofMode

theorem T : ∃ x, x < x + 1 := by
  constructor
  start_proof -- this pushes the current proof state (note, it doesn't work in `example`)

## -- cursor here to see proof state
## refine Nat.lt_succ_self ?_ -- you can write a tactic or tactic block here
## exact 1 -- when the goal is finished, it pops the proof state and reports "Goals accomplished 🎉"

[Mario Carneiro]

It would be nice to get some experience reports with this from people who like to write long tactic proofs and struggle to keep things responsive

[D. J. Bernstein]

Will try with my next Lean project, thanks!