Coq's Abort in Lean

Stream: general

[Kevin Sullivan]

What is Lean's equivalent of Abort in Coq?

[Mario Carneiro]

what does it do?

[Kevin Sullivan]

@Mario Carneiro Abort terminates (gives up on) a failing or incomplete proof (whereas Coq's "Admitted" gives up and accepts the proposition being proved as an axiom, like sorry in Lean).

[Mario Carneiro]

Lean doesn't have this. I guess it makes more sense with the line-based input approach to coq

[Mario Carneiro]

but in lean once you have written def you are committed to either finishing it or getting an error or warning

[Kevin Sullivan]

For pedagogical purposes in any case it'd be good to have, as one can then exhibit proof strategies that don't work out. Students can see how the tactic state evolves until one gets stuck and gives up.

[Mario Carneiro]

Usually we use sorry for that

[Kevin Sullivan]

Yes but sorry accepts the proposition axiomatically, which in general is not what one wants to do. E.g., when showing why P \or \not P isn't provable without em.

[Simon Hudon]

You can use run_cmd: it allows you to run tactics and failing to prove the goal has no consequences

[Sebastian Ullrich]

example may be more appropriate in that case

[Simon Hudon]

example has the down side that, if you use sorry, it still produces warnings.

[Mario Carneiro]

There is always the trick used in the tests: use sorry in a have subproof that doesn't get used

[Kevin Sullivan]

There is always the trick used in the tests: use sorry in a have subproof that doesn't get used

There are work-arounds, albeit with some compromises, but wouldn't it be cleaner to just provide an "abort" tactic. The context for this suggestion is not expert use of Lean but rather early undergraduate education, where every inelegant complexity causes additional pain and suffering amongst students.

[Sebastian Ullrich]

Note that Abort is not a tactic but a built-in command in Coq. We would need to change the begin...end syntax and parts of the elaborator for something similar.

[Rob Lewis]

From what (little) I know about Coq, Abort isn't a tactic, it's a top-level command. I don't think there's a way to implement it as a tactic in Lean 3, at least not in a way that mimics the usage of the Coq command. This seems like the kind of thing you might be able to do in Lean 4.

[Sebastian Ullrich]

Nice timing :)

[Rob Lewis]

Haha, good timing!

[Sebastian Ullrich]

:D

[Patrick Massot]

Amazing duo

[Rob Lewis]

To keep repeating Sebastian, I agree that using example is the Lean-style way to do this.

[Rob Lewis]

To show a failing proof attempt, start an example and don't finish it.

[Patrick Massot]

No, the Lean way is to finish the proof.

[Rob Lewis]

There's no problem leaving an attempt unfinished like there is in Coq, it doesn't stop the processing of future declarations.

[Patrick Massot]

Even if == suddenly appear in the proof

[Simon Hudon]

What if we treated abort like sorry except that, when it appears in an example, it doesn't produce warnings?

[Kevin Sullivan]

What if we treated abort like sorry except that, when it appears in an example, it doesn't produce warnings?

It would need both (1) to not produce warnings, and (2) to not accept the goal axiomatically.

And, yes, to Rob L. Abort is a command, not a tactic, in Coq.

By the way, Coq's command, analogous to Lean's sorry, is Admitted. It gives up on the current proof and accepts the goal axiomatically. By contrast, Abort gives up on the current proof but discards rather than accepts the current goal.

[Simon Hudon]

I think examples can't be invoked from other proofs so that part is already there.

[Rob Lewis]

I've only used Coq for simple things. Specifically, I don't know how Abort works in nested proofs like they describe in the manual. Here's something that very roughly approximates its behavior in the top-level case. If you use example, the environment will be the same before and after processing this, and there are no warnings.

constant {u} abort {α : Sort u} : α

open tactic
meta def tactic.interactive.abort : tactic unit :=
all_goals `[exact abort]

example : 0 < 0 ∧ 0 > 0 :=
begin
  split,
  abort
end

[Rob Lewis]

But I still think the Lean-style way to do this is to just leave the example unfinished.