Add Coq-like "abort" tactic

[kevinsullivan]

Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Lean lacks a tactic, the analog of Abort in Coq, that gives up on the current proof script and leaves the goal unproved.

Steps to Reproduce

NA

Expected behavior: [What you expect to happen]

NA

Actual behavior: [What actually happens]

NA

Reproduces how often: [What percentage of the time does it reproduce?]

NA

Versions

All

Additional Information

Having an abort tactic would be beneficial for pedagogy using Lean. One could then present attempts at proofs that don't work out. Students could see the evolving tactic state until a dead end is hit, at which point the attempt could be aborted. I'm not sure if there's a technical reason not to include such a tactic in Lean.

[digama0]

Lean 3 is EOL, so this issue is not likely to be addressed for a possibly very long time.

[kim-em]

What would this do that sorry doesn't already achieve?

[cipher1024]

sorry creates a warning and in trust level 0, it creates an error. Additionally, when you use sorry, you can use the definition / lemma after but with abort, the definition / lemma is not available after it is aborted and doesn't produce a warning or error.

[cipher1024]

One way I have been producing a similar effect is with:

example : true :=
begin
  suffices : /- some formula -/, trivial,
  /- a proof that you can end with an admit without warning -/
end