Add a rootGoals option to instantiate synthetic sorries from declar…

…ations root goal

- Useful for people experimenting with automated provers. Example usage: run a lean file from the MiniF2F benchmark, and get sorries even if there already exist proofs. Similar to LeanDojo, but without having to trace the project.
- Fix: add rootGoals for proof states extracted by the `tactics` method

REPL/JSON.lean

@@ -13,6 +13,7 @@ namespace REPL
 
 structure CommandOptions where
   allTactics : Option Bool := none
+  rootGoals : Option Bool := none
   /--
   Should be "full", "tactics", "original", or "substantive".
   Anything else is ignored.

REPL/Lean/InfoTree.lean

@@ -160,16 +160,44 @@ partial def findAllInfo (t : InfoTree) (ctx? : Option ContextInfo) (p : Info →
     info ++ rest
   | _ => []
 
+/-- Analogue of `Lean.Elab.InfoTree.findAllInfo` but specialized to `TacticInfo` to return root goals. -/
+partial def findAllInfoTactics (t : InfoTree) (ctx? : Option ContextInfo) (rootGoals : List MVarId) :
+  List (Info × Option ContextInfo × List MVarId) :=
+  match t with
+  | .context ctx t => t.findAllInfoTactics (ctx.mergeIntoOuter? ctx?) rootGoals
+  | .node info ts =>
+    let tInfo := match info with
+    | .ofTacticInfo i =>
+      if info.isOriginal && i.isSubstantive then
+        let rootGoals := if rootGoals.isEmpty then i.goalsBefore else rootGoals
+        [(info, ctx?, rootGoals)]
+      else
+        []
+    | _ => []
+    tInfo ++ ts.toList.flatMap (fun t => t.findAllInfoTactics ctx? rootGoals)
+  | _ => []
+
 /-- Return all `TacticInfo` nodes in an `InfoTree` with "original" syntax,
 each equipped with its relevant `ContextInfo`. -/
-def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo) :=
-  let infos := t.findAllInfo none fun i => match i with
-  | .ofTacticInfo i' => i.isOriginal && i'.isSubstantive
-  | _ => false
+def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo × List MVarId) :=
+  let infos := t.findAllInfoTactics none []
   infos.filterMap fun p => match p with
-  | (.ofTacticInfo i, some ctx) => (i, ctx)
+  | (.ofTacticInfo i, some ctx, rootGoals) => (i, ctx, rootGoals)
   | _ => none
 
+partial def findRootGoals (t : InfoTree) (ctx? : Option ContextInfo := none) :
+  List (TacticInfo × ContextInfo × List MVarId) :=
+  match t with
+  | .context ctx t => t.findRootGoals (ctx.mergeIntoOuter? ctx?)
+  | .node info ts =>
+    match info with
+    | .ofTacticInfo i =>
+      match ctx? with
+      | some ctx => [(i, ctx, i.goalsBefore)]
+      | _ => []
+    | _ => ts.toList.flatMap (fun t => t.findRootGoals ctx?)
+  | _ => []
+
 /-- Return all `TacticInfo` nodes in an `InfoTree`
 corresponding to explicit invocations of the `sorry` tactic,
 each equipped with its relevant `ContextInfo`. -/
@@ -212,17 +240,24 @@ def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Posit
   (t.findSorryTermNodes.map fun ⟨i, ctx⟩ =>
     (ctx, .term i.lctx i.expectedType?, stxRange ctx.fileMap i.stx))
 
-def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × Position × Position × Array Name) :=
+def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × List MVarId × Position × Position × Array Name) :=
     -- HACK: creating a child ngen
-  t.findTacticNodes.map fun ⟨i, ctx⟩ => 
-    let range := stxRange ctx.fileMap i.stx 
-    ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, 
-      i.stx, 
-      i.goalsBefore, 
-      range.fst, 
-      range.snd, 
+  t.findTacticNodes.map fun ⟨i, ctx, rootGoals⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 },
+      i.stx,
+      rootGoals,
+      i.goalsBefore,
+      range.fst,
+      range.snd,
       i.getUsedConstantsAsSet.toArray )
 
+def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) :=
+  t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 },
+      rootGoals,
+      range.fst )
 
 end Lean.Elab.InfoTree
 
@@ -277,7 +312,7 @@ namespace Lean.Elab.InfoTree
 Finds all tactic invocations in an `InfoTree`,
 ignoring structuring tactics (e.g. `by`, `;`, multiline tactics, parenthesized tactics).
 -/
-def substantiveTactics (t : InfoTree) : List (TacticInfo × ContextInfo) :=
+def substantiveTactics (t : InfoTree) : List (TacticInfo × ContextInfo × List MVarId) :=
   t.findTacticNodes.filter fun i => i.1.isSubstantive
 
 end Lean.Elab.InfoTree

REPL/Main.lean

@@ -94,18 +94,18 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   modify fun s => { s with proofStates := s.proofStates.push proofState }
   return id
 
-def sorries (trees : List InfoTree) (env? : Option Environment) (initGoals? : Option (List MVarId))
+def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId))
 : M m (List Sorry) :=
   trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with
     | .term _ none => false
     | _ => true ) |>.mapM
       fun ⟨ctx, g, pos, endPos⟩ => do
         let (goal, proofState) ← match g with
         | .tactic g => do
-           let s ← ProofSnapshot.create ctx none env? [g] initGoals?
+           let s ← ProofSnapshot.create ctx none env? [g] rootGoals?
            pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term lctx (some t) => do
-           let s ← ProofSnapshot.create ctx lctx env? [] initGoals? [t]
+           let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t]
            pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term _ none => unreachable!
         let proofStateId ← proofState.mapM recordProofSnapshot
@@ -119,19 +119,27 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
 
 def tactics (trees : List InfoTree) : M m (List Tactic) :=
   trees.flatMap InfoTree.tactics |>.mapM
-    fun ⟨ctx, stx, goals, pos, endPos, ns⟩ => do
-      let proofState := some (← ProofSnapshot.create ctx none none goals)
+    fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do
+      let proofState := some (← ProofSnapshot.create ctx none none goals rootGoals)
       let goals := s!"{(← ctx.ppGoals goals)}".trim
       let tactic := Format.pretty (← ppTactic ctx stx)
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Tactic.of goals tactic pos endPos proofStateId ns
 
-/-- Inspired from LeanDojo REPL. -/
+def rootGoals (trees : List InfoTree) : M m (List Sorry) := do
+  trees.flatMap InfoTree.rootGoals |>.mapM
+    fun ⟨ctx, goals, pos⟩ => do
+      let proofState := some (← ProofSnapshot.create ctx none none goals goals)
+      let goals := s!"{(← ctx.ppGoals goals)}".trim
+      let proofStateId ← proofState.mapM recordProofSnapshot
+      return Sorry.of goals pos pos proofStateId
+
+/-- Get the status of the whole proof up to this point. Inspired from LeanDojo REPL. -/
 def getProofStatus (proofState : ProofSnapshot) : M m String := do
   match proofState.tacticState.goals with
     | [] =>
       let res := proofState.runMetaM do
-        match proofState.initialGoals with
+        match proofState.rootGoals with
         | [goalId] =>
           match proofState.metaState.mctx.getExprAssignmentCore? goalId with
           | none => return "Error: Goal not assigned"
@@ -147,7 +155,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
               name := Name.anonymous,
               type := pft,
               value := pf,
-              levelParams := [],
+              levelParams := (collectLevelParams {} pft).params.toList,
               hints := ReducibilityHints.opaque,
               safety := DefinitionSafety.safe
             })
@@ -178,7 +186,7 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
   | none => pure trees
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees none (some proofState.initialGoals)
+  let sorries ← sorries trees none (some proofState.rootGoals)
   let id ← recordProofSnapshot proofState
   return {
     proofState := id
@@ -243,6 +251,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
   let sorries ← sorries trees (initialCmdState?.map (·.env)) none
+  let sorries ← match s.rootGoals with
+  | some true => pure (sorries ++ (← rootGoals trees))
+  | _ => pure sorries
   let tactics ← match s.allTactics with
   | some true => tactics trees
   | _ => pure []

REPL/Snapshots.lean

@@ -108,7 +108,7 @@ structure ProofSnapshot where
   termContext   : Term.Context
   tacticState   : Tactic.State
   tacticContext : Tactic.Context
-  initialGoals  : List MVarId
+  rootGoals     : List MVarId
 
 namespace ProofSnapshot
 
@@ -192,7 +192,7 @@ For convenience, we also allow a list of `Expr`s, and these are appended to the
 as fresh metavariables with the given types.
 -/
 def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
-    (goals : List MVarId) (initGoals? : Option (List MVarId)) (types : List Expr := [])
+    (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := [])
     : IO ProofSnapshot := do
   ctx.runMetaM (lctx?.getD {}) do
     let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
@@ -209,7 +209,7 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi
       termContext := {}
       tacticState := { goals }
       tacticContext := { elaborator := .anonymous }
-      initialGoals := match initGoals? with
+      rootGoals := match rootGoals? with
         | none => goals
         | some gs => gs }
 
@@ -275,15 +275,15 @@ def pickle (p : ProofSnapshot) (path : FilePath) : IO Unit := do
      ({ p'.termContext with } : CompactableTermContext),
      p'.tacticState,
      p'.tacticContext,
-     p'.initialGoals)
+     p'.rootGoals)
 
 /--
 Unpickle a `ProofSnapshot`.
 -/
 def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) :
     IO (ProofSnapshot × CompactedRegion) := unsafe do
   let ((imports, map₂, coreState, coreContext, metaState, metaContext, termState, termContext,
-    tacticState, tacticContext, initialGoals), region) ←
+    tacticState, tacticContext, rootGoals), region) ←
     _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCoreState ×
       Core.Context × Meta.State × CompactableMetaContext × Term.State × CompactableTermContext ×
       Tactic.State × Tactic.Context × List MVarId) path
@@ -302,7 +302,7 @@ def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) :
     termContext := { termContext with }
     tacticState
     tacticContext
-    initialGoals }
+    rootGoals }
   let (_, p'') ← p'.runCoreM do
     for o in ← getOpenDecls do
       if let .simple ns _ := o then

test/root_goals.expected.out

@@ -0,0 +1,20 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 17},
+   "goal": "⊢ 1 = 1",
+   "endPos": {"line": 1, "column": 17}},
+  {"proofState": 1,
+   "pos": {"line": 5, "column": 22},
+   "goal": "⊢ 1 + 1 = 2",
+   "endPos": {"line": 5, "column": 22}}],
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 3, "column": 2},
+   "endPos": {"line": 3, "column": 8},
+   "data": "Try this: exact rfl"}],
+ "env": 0}
+
+{"proofStatus": "Completed", "proofState": 2, "goals": []}
+
+{"proofStatus": "Completed", "proofState": 3, "goals": []}
+

test/root_goals.in

@@ -0,0 +1,6 @@
+{"cmd": "example : 1=1 := by\n  skip\n  exact?\n\ntheorem bb : 1+1=2 := by rfl", "rootGoals": true}
+
+{"proofState" : 0, "tactic": "rfl"}
+
+{"proofState" : 1, "tactic": "exact rfl"}
+

test/self_proof_apply_check.expected.out

@@ -0,0 +1,25 @@
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 10},
+   "data":
+   "fail to show termination for\n  ex\nwith errors\nfailed to infer structural recursion:\nno parameters suitable for structural recursion\n\nwell-founded recursion cannot be used, 'ex' does not take any (non-fixed) arguments"}],
+ "env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 22},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 27}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 10},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofStatus":
+ "Error: kernel type check failed: (kernel) declaration has free variables '[anonymous]'",
+ "proofState": 1,
+ "goals": []}
+

test/self_proof_apply_check.in

@@ -0,0 +1,5 @@
+{"cmd": "theorem ex : False := by apply ex"}
+
+{"cmd": "theorem ex : False := sorry"}
+
+{"proofState": 0, "tactic": "apply ex"}

test/self_proof_check.expected.out

@@ -1,9 +1,9 @@
 {"messages":
  [{"severity": "error",
-   "pos": {"line": 1, "column": 8},
-   "endPos": {"line": 1, "column": 10},
+   "pos": {"line": 1, "column": 25},
+   "endPos": {"line": 1, "column": 31},
    "data":
-   "fail to show termination for\n  ex\nwith errors\nfailed to infer structural recursion:\nno parameters suitable for structural recursion\n\nwell-founded recursion cannot be used, 'ex' does not take any (non-fixed) arguments"}],
+   "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}],
  "env": 0}
 
 {"sorries":
@@ -18,8 +18,12 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofStatus":
- "Error: kernel type check failed: (kernel) declaration has free variables '[anonymous]'",
+{"proofStatus": "Incomplete: contains sorry",
  "proofState": 1,
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}],
  "goals": []}
 

test/self_proof_check.in

@@ -1,5 +1,6 @@
-{"cmd": "theorem ex : False := by exact ex"}
+{"cmd": "theorem ex : False := by exact?"}
 
 {"cmd": "theorem ex : False := sorry"}
 
-{"proofState": 0, "tactic": "exact ex"}
+{"proofState": 0, "tactic": "exact?"}
+

test/self_proof_exact_check.expected.out

@@ -1,9 +1,9 @@
 {"messages":
  [{"severity": "error",
-   "pos": {"line": 1, "column": 25},
-   "endPos": {"line": 1, "column": 31},
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 10},
    "data":
-   "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}],
+   "fail to show termination for\n  ex\nwith errors\nfailed to infer structural recursion:\nno parameters suitable for structural recursion\n\nwell-founded recursion cannot be used, 'ex' does not take any (non-fixed) arguments"}],
  "env": 0}
 
 {"sorries":
@@ -18,12 +18,8 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofStatus": "Incomplete: contains sorry",
+{"proofStatus":
+ "Error: kernel type check failed: (kernel) declaration has free variables '[anonymous]'",
  "proofState": 1,
- "messages":
- [{"severity": "info",
-   "pos": {"line": 0, "column": 0},
-   "endPos": {"line": 0, "column": 0},
-   "data": "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}],
  "goals": []}
 

test/self_proof_exact_check.in

@@ -1,6 +1,5 @@
-{"cmd": "theorem ex : False := by exact?"}
+{"cmd": "theorem ex : False := by exact ex"}
 
 {"cmd": "theorem ex : False := sorry"}
 
-{"proofState": 0, "tactic": "exact?"}
-
+{"proofState": 0, "tactic": "exact ex"}