Add proof step verification

[Kripner]

Verify each proof step in tactic mode. Roughly, the idea for step (old :: ProofSnapshot, new :: ProofSnapshot) is to:

• (1) Look at all goals in old which no longer exist in new. For each one:
  • (2) Retrieve it's assignment in new. For each metavariable in the assignment:
    • (3) If it is a goal which exists in new, it's fine and we do nothing since we can assume it will be solved in future steps. In this case, we replace it with sorry in the assignment so that the expression can be sent to kernel.
    • (4) Otherwise, it's an error since there is a metavariable which won't be assigned in the future.
  • (5) Send the assignment with metavariables replaced by sorry to kernel for a type check.

Compared to #63, this approach could eliminate false negatives like https://github.com/leanprover-community/repl/blob/master/test/name_generator.in, where checking the whole proof term doesn't work since in a have branch we don't see the metavariable assignments from the main branch.

[Kripner]

@kim-em I think this feature is still important. It complements the proofStatus feature (#63) which checks the whole proof term in each branch and thus reports false errors any time the proof branches (e.g. due to have), even when the proof branch is in fact correct. This new stepVerification feature simply checks that no goals disappear during tactic application (i.e. each goal present in stateBefore and not present in stateAfter is correctly assigned). This is useful in automated theorem proving.

For e.g. this input:

{"cmd": "example : 1 = 1 := by sorry"}
{"tactic": "have : 2 = 2 := by sorry", "proofState": 0}
{"tactic": "rfl", "proofState": 1}
{"tactic": "rfl", "proofState": 2}

Notice proofStatus and stepVerification in the output:

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 1, "column": 22},
   "goal": "⊢ 1 = 1",
   "endPos": {"line": 1, "column": 27}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 7},
   "data": "declaration uses 'sorry'"}],
 "env": 0}

{"stepVerification": "OK",
 "sorries": [{"proofState": 1, "goal": "⊢ 2 = 2"}],
 "proofStatus": "Incomplete: open goals remain",
 "proofState": 2,
 "goals": ["this : 2 = 2\n⊢ 1 = 1"]}

{"stepVerification": "OK",
 "proofStatus": "Incomplete: contains metavariable(s)",
 "proofState": 3,
 "goals": []}

{"stepVerification": "OK",
 "proofStatus": "Incomplete: contains sorry",
 "proofState": 4,
 "goals": []}

proofStatus will never report completed because the proof branches using have. However, we can believe the proof due to the fact that each stepVerification is "OK" and goals is empty at the end.

For an example of an incorrect proof, consider this input:

{"cmd": "example : 1 = 0 := by sorry"}
{"tactic": "cases 1", "proofState": 0}
{"tactic": "rfl", "proofState": 1}
{"tactic": "apply ?succ", "proofState": 2}

In the last step, stepVerification correctly reports "Error: Goal _uniq.81.76 assignment is circular".