[BUG] REPL accepts incorrect proofs

[amit9oct]

I found a peculiar bug in REPL, where it can accept any proof that applies the theorem itself.

Example:

{"cmd": "theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by sorry"}

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 1, "column": 62},
   "goal": "p q : Prop\nhp : p\nhq : q\n⊢ p ∧ q ∧ p",
   "endPos": {"line": 1, "column": 67}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 8},
   "endPos": {"line": 1, "column": 12},
   "data": "declaration uses 'sorry'"}],
 "env": 0}

{"tactic": "apply test", "proofState": 0}

{"proofState": 1,
 "goals":
 ["case hp\np q : Prop\nhp : p\nhq : q\n⊢ p",
  "case hq\np q : Prop\nhp : p\nhq : q\n⊢ q"]}

In the above example, we cannot complete the proof by applying itself. However, REPL does not raise any error messages. However, on VS Code IDE for Lean 4, we get the error message for the proof below:

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
    apply test
    exact hp
    exact hq

Expected Error message:

fail to show termination for
  Lean4Proj1.test
with errors
structural recursion cannot be used

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
          hp hq
1) 5:8-12  _  _
Please use `termination_by` to specify a decreasing measure.

[digama0]

Your two examples are not the same. Did you try attempting to complete the proof using exact hp; exact hq in the REPL?

It is expected that calling apply test does not result in an immediate error. This is a valid proof strategy for proofs by induction, and the termination check only runs once the definition or proof is complete.

[amit9oct]

I forgot to paste the full output

{"cmd": "theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by sorry"}

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 1, "column": 62},
   "goal": "p q : Prop\nhp : p\nhq : q\n⊢ p ∧ q ∧ p",
   "endPos": {"line": 1, "column": 67}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 8},
   "endPos": {"line": 1, "column": 12},
   "data": "declaration uses 'sorry'"}],
 "env": 0}

{"tactic": "apply test", "proofState": 0}

{"proofState": 1,
 "goals":
 ["case hp\np q : Prop\nhp : p\nhq : q\n⊢ p",
  "case hq\np q : Prop\nhp : p\nhq : q\n⊢ q"]}

{"tactic": "exact hp", "proofState": 1}

{"proofState": 2, "goals": ["case hq\np q : Prop\nhp : p\nhq : q\n⊢ q"]}

{"tactic": "exact hq", "proofState": 2}

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

As you can there is no error message here. Also NOTE: The VS Code IDE shows the error message as soon as we use apply test tactic.

[amit9oct]

Also exact hp; exact hq won't work in REPL because it doesn't support tactical (;)

[digama0]

Is this actually a complete proof though? I'm not super familiar with the REPL API but I would expect some kind of qed-equivalent to complete the proof once all the goals are finished. It may well be that this is a (design) bug in the REPL in that it has no way to express errors that occur when entering the definition into the environment.

PS: ; isn't a tactical, it is just a list of tactics. You have to pass them separately with the REPL API since it takes single tactics, or enclose it in parentheses like (exact hp; exact hq).

[amit9oct]

I just followed the example shown in the README (https://github.com/leanprover-community/repl/blob/master/README.md), I may be wrong, but it doesn't look like there is something like qed from the examples.

[digama0]

At present there is nothing you can do with a completed proof state: we would like to extend this so that you can replace the original sorry with your tactic script, and obtain the resulting Environment.

So apparently QED is not implemented yet. If it was, this is the step that would give the error.