Add Pantograph-like approach to tactic mode

[augustepoiroux]

This PR implements an approach similar to Pantograph: it transforms sorries introduced in tactic mode as new goals in the same proof state. This removes the branching problem, making possible to run kernel check of such proofs.

TODO:

• Adding tests
• Update the sorries method to instantiate a unique proofstate per declaration
• Adding an attribute to focus on goals / group of goals

Example

Input:

{"cmd": "example : 1 = 1 := by sorry"}

{"tactic": "have h : 2 = 2 := by sorry", "proofState": 0}

{"tactic": "rfl", "proofState": 1}

{"tactic": "rfl", "proofState": 2}

Previous 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}

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

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

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

New 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}

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

{"proofStatus": "Incomplete: open goals remain",
 "proofState": 2,
 "goals": ["⊢ 2 = 2"]}

{"proofStatus": "Completed", "proofState": 3, "goals": []}

[haoxiongliu]

Could you share the reason why we finally choose this goal ordering? The example provided corresponds to the lean file

example : 1 = 1 :=
  have h : 2 = 2 := by
    rfl
  rfl

so the first rfl solves the "⊢ 2 = 2" goal and the second one solves "h : 2 = 2\n⊢ 1 = 1". However, current goal ordering seems to be working otherwise.

[haoxiongliu]

Could you share the reason why we finally choose this goal ordering? The example provided corresponds to the lean file

example : 1 = 1 :=
  have h : 2 = 2 := by
    rfl
  rfl

so the first rfl solves the "⊢ 2 = 2" goal and the second one solves "h : 2 = 2\n⊢ 1 = 1". However, current goal ordering seems to be working otherwise.

I see your updation on goal ordering today! Thank you for the great efforts.

[augustepoiroux]

The goal ordering is not perfect at the moment. If you look at the example I shared in the zulip channel, you will notice that the order is slightly random. I will try to improve that, but no promise as I am not sure it is possible to recover sorry position in a file from an expr in tactic mode.

[haoxiongliu]

The goal ordering is not perfect at the moment. If you look at the example I shared in the zulip channel, you will notice that the order is slightly random. I will try to improve that, but no promise as I am not sure it is possible to recover sorry position in a file from an expr in tactic mode.

Thank you for the clarification. I see that the 4 goals in proofState 0 are quite random. Nevertheless, at least if we add by before the 2nd and the 3rd sorry, we can get it just in the order in the file content. So from my point of view the current implementation is already useful for sequential check. Thanks again!