Fix missing local context + valid proofs wrongfully rejected in tactic mode (#82)

* Fix missing local context + fvar when validating proofs

* Solve `exact?` self-application issue

* Fix remaining cases where access to future environment in initial commands was possible through ProofSnapshot

Author: augustepoiroux

REPL/Frontend.lean

@@ -28,20 +28,30 @@ If there is no existing environment, we parse the input for headers (e.g. import
 and create a new environment.
 Otherwise, we add to the existing environment.
 
-Returns the resulting command state, along with a list of messages and info trees.
+Returns:
+1. The header-only command state (only useful when cmdState? is none)
+2. The resulting command state after processing the entire input
+3. List of messages
+4. List of info trees
 -/
 def processInput (input : String) (cmdState? : Option Command.State)
     (opts : Options := {}) (fileName : Option String := none) :
-    IO (Command.State × List Message × List InfoTree) := unsafe do
+    IO (Command.State × Command.State × List Message × List InfoTree) := unsafe do
   Lean.initSearchPath (← Lean.findSysroot)
   enableInitializersExecution
   let fileName   := fileName.getD "<input>"
   let inputCtx   := Parser.mkInputContext input fileName
-  let (parserState, commandState) ← match cmdState? with
+
+  match cmdState? with
   | none => do
+    -- Split the processing into two phases to prevent self-reference in proofs in tactic mode
     let (header, parserState, messages) ← Parser.parseHeader inputCtx
     let (env, messages) ← processHeader header opts messages inputCtx
-    pure (parserState, (Command.mkState env messages opts))
-  | some cmdState => do
-    pure ({ : Parser.ModuleParserState }, cmdState)
-  processCommandsWithInfoTrees inputCtx parserState commandState
+    let headerOnlyState := Command.mkState env messages opts
+    let (cmdState, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState
+    return (headerOnlyState, cmdState, messages, trees)
+
+  | some cmdStateBefore => do
+    let parserState : Parser.ModuleParserState := {}
+    let (cmdStateAfter, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore
+    return (cmdStateBefore, cmdStateAfter, messages, trees)

REPL/Main.lean

@@ -102,11 +102,15 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
       fun ⟨ctx, g, pos, endPos⟩ => do
         let (goal, proofState) ← match g with
         | .tactic g => do
-           let s ← ProofSnapshot.create ctx none env? [g] rootGoals?
-           pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
+          let lctx ← ctx.runMetaM {} do
+              match ctx.mctx.findDecl? g with
+              | some decl => return decl.lctx
+              | none => throwError "unknown metavariable '{g}'"
+          let s ← ProofSnapshot.create ctx lctx 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? [] rootGoals? [t]
-           pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
+          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
         return Sorry.of goal pos endPos proofStateId
@@ -117,23 +121,55 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   catch _ =>
     pure "<failed to pretty print>"
 
-def tactics (trees : List InfoTree) : M m (List Tactic) :=
+def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tactic) :=
   trees.flatMap InfoTree.tactics |>.mapM
     fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do
-      let proofState := some (← ProofSnapshot.create ctx none none goals rootGoals)
+      let proofState := some (← ProofSnapshot.create ctx none env? 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
 
-def collectRootGoalsAsSorries (trees : List InfoTree) : M m (List Sorry) := do
+def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : 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 proofState := some (← ProofSnapshot.create ctx none env? goals goals)
       let goals := s!"{(← ctx.ppGoals goals)}".trim
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Sorry.of goals pos pos proofStateId
 
+
+private def collectFVarsAux : Expr → NameSet
+  | .fvar fvarId => NameSet.empty.insert fvarId.name
+  | .app fm arg => (collectFVarsAux fm).union $ collectFVarsAux arg
+  | .lam _ binderType body _ => (collectFVarsAux binderType).union $ collectFVarsAux body
+  | .forallE _ binderType body _ => (collectFVarsAux binderType).union $ collectFVarsAux body
+  | .letE _ type value body _ => ((collectFVarsAux type).union $ collectFVarsAux value).union $ collectFVarsAux body
+  | .mdata _ expr => collectFVarsAux expr
+  | .proj _ _ struct => collectFVarsAux struct
+  | _ => NameSet.empty
+
+/-- Collect all fvars in the expression, and return their names. -/
+private def collectFVars (e : Expr) : MetaM (Array Expr) := do
+  let names := collectFVarsAux e
+  let mut fvars := #[]
+  for ldecl in ← getLCtx do
+    if ldecl.isImplementationDetail then
+      continue
+    if names.contains ldecl.fvarId.name then
+      fvars := fvars.push $ .fvar ldecl.fvarId
+  return fvars
+
+
+private def abstractAllLambdaFVars (e : Expr) : MetaM Expr := do
+  let mut e' := e
+  while e'.hasFVar do
+    let fvars ← collectFVars e'
+    if fvars.isEmpty then
+      break
+    e' ← Meta.mkLambdaFVars fvars e'
+  return e'
+
 /--
 Evaluates the current status of a proof, returning a string description.
 Main states include:
@@ -153,25 +189,39 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
           | none => return "Error: Goal not assigned"
           | some pf => do
             let pf ← instantiateMVars pf
+
+            -- First check that the proof has the expected type
             let pft ← Meta.inferType pf >>= instantiateMVars
-            if pf.hasSorry then
-              return "Incomplete: contains sorry"
+            let expectedType ← Meta.inferType (mkMVar goalId) >>= instantiateMVars
+            unless (← Meta.isDefEq pft expectedType) do
+              return s!"Error: proof has type {pft} but root goal has type {expectedType}"
+
+            let pf ← goalId.withContext $ abstractAllLambdaFVars pf
+            let pft ← Meta.inferType pf >>= instantiateMVars
+
             if pf.hasExprMVar then
               return "Incomplete: contains metavariable(s)"
 
-            let decl := Declaration.defnDecl ({
+            -- Find all level parameters
+            let usedLevels := collectLevelParams {} pft
+            let usedLevels := collectLevelParams usedLevels pf
+
+            let decl := Declaration.defnDecl {
               name := Name.anonymous,
               type := pft,
               value := pf,
-              levelParams := (collectLevelParams {} pft).params.toList,
+              levelParams := usedLevels.params.toList,
               hints := ReducibilityHints.opaque,
               safety := DefinitionSafety.safe
-            })
+            }
 
             try
               let _ ← addDecl decl
             catch ex =>
               return s!"Error: kernel type check failed: {← ex.toMessageData.toString}"
+
+            if pf.hasSorry then
+              return "Incomplete: contains sorry"
             return "Completed"
 
         | _ => return "Not verified: more than one initial goal"
@@ -251,19 +301,19 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   if notFound then
     return .inr ⟨"Unknown environment."⟩
   let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
-  let (cmdState, messages, trees) ← try
+  let (initialCmdState, cmdState, messages, trees) ← try
     IO.processInput s.cmd initialCmdState?
   catch ex =>
     return .inr ⟨ex.toString⟩
   let messages ← messages.mapM fun m => Message.of m
   -- 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 ← sorries trees initialCmdState.env none
   let sorries ← match s.rootGoals with
-  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees))
+  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env))
   | _ => pure sorries
   let tactics ← match s.allTactics with
-  | some true => tactics trees
+  | some true => tactics trees initialCmdState.env
   | _ => pure []
   let cmdSnapshot :=
   { cmdState

test/assumption_proof.expected.out

@@ -0,0 +1,14 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 49},
+   "goal": "x : Nat\nh1 : x = 2\n⊢ x = 2",
+   "endPos": {"line": 1, "column": 54}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 10},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
+

test/assumption_proof.in

@@ -0,0 +1,3 @@
+{"cmd": "theorem aa (x : Nat) (h1 : x  = 2) : x = 2 := by sorry"}
+
+{"tactic": "assumption", "proofState": 0}

test/name_generator.expected.out

@@ -43,7 +43,7 @@
  "proofState": 7,
  "goals": []}
 
-{"proofStatus": "Incomplete: contains sorry",
+{"proofStatus": "Incomplete: contains metavariable(s)",
  "proofState": 8,
  "messages":
  [{"severity": "error",
@@ -52,7 +52,7 @@
    "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}],
  "goals": []}
 
-{"proofStatus": "Incomplete: contains sorry",
+{"proofStatus": "Incomplete: contains metavariable(s)",
  "proofState": 9,
  "messages":
  [{"severity": "error",

test/proof_branching.expected.out

@@ -0,0 +1,28 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 75},
+   "goal": "p q r : Prop\nh1 : p ∧ q\nh2 : q → r\n⊢ p ∧ r",
+   "endPos": {"line": 1, "column": 80}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 19},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals":
+ ["case left\np q r : Prop\nh1 : p ∧ q\nh2 : q → r\n⊢ p",
+  "case right\np q r : Prop\nh1 : p ∧ q\nh2 : q → r\n⊢ r"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["case right\np q r : Prop\nh1 : p ∧ q\nh2 : q → r\n⊢ r"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "goals": ["case right\np q r : Prop\nh1 : p ∧ q\nh2 : q → r\n⊢ q"]}
+
+{"proofStatus": "Completed", "proofState": 4, "goals": []}
+

test/proof_branching.in

@@ -0,0 +1,10 @@
+{"cmd": "theorem complex_and (p q r : Prop) (h1 : p ∧ q) (h2 : q → r) : p ∧ r := by sorry"}
+
+{"tactic": "apply And.intro", "proofState": 0}
+
+{"tactic": "exact h1.left", "proofState": 1}
+
+{"tactic": "apply h2", "proofState": 2}
+
+{"tactic": "exact h1.right", "proofState": 3}
+

test/proof_branching2.expected.out

@@ -0,0 +1,36 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 43},
+   "goal": "p q : Prop\n⊢ p ∧ q → q ∧ p",
+   "endPos": {"line": 1, "column": 48}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["p q : Prop\nh : p ∧ q\n⊢ q ∧ p"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["p q : Prop\nh : p ∧ q\nhp : p\n⊢ q ∧ p"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "goals": ["p q : Prop\nh : p ∧ q\nhp : p\nhq : q\n⊢ q ∧ p"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 4,
+ "goals":
+ ["case left\np q : Prop\nh : p ∧ q\nhp : p\nhq : q\n⊢ q",
+  "case right\np q : Prop\nh : p ∧ q\nhp : p\nhq : q\n⊢ p"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 5,
+ "goals": ["case right\np q : Prop\nh : p ∧ q\nhp : p\nhq : q\n⊢ p"]}
+
+{"proofStatus": "Completed", "proofState": 6, "goals": []}
+

test/proof_branching2.in

@@ -0,0 +1,14 @@
+{"cmd": "example (p q : Prop) : p ∧ q → q ∧ p := by sorry"}
+
+{"tactic": "intro h", "proofState": 0}
+
+{"tactic": "have hp : p := h.left", "proofState": 1}
+
+{"tactic": "have hq : q := h.right", "proofState": 2}
+
+{"tactic": "apply And.intro", "proofState": 3}
+
+{"tactic": "exact hq", "proofState": 4}
+
+{"tactic": "exact hp", "proofState": 5}
+

test/proof_transitivity.expected.out

@@ -0,0 +1,28 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 62},
+   "goal": "x y z : Nat\nh1 : x = y\nh2 : y = z\n⊢ x = z",
+   "endPos": {"line": 1, "column": 67}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
+
+{"sorries":
+ [{"proofState": 2,
+   "pos": {"line": 1, "column": 64},
+   "goal": "f : Nat → Nat\nn : Nat\nh : n = 3\n⊢ f n = f 3",
+   "endPos": {"line": 1, "column": 69}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofStatus": "Completed", "proofState": 3, "goals": []}
+