Zulip Chat Archive

Stream: general

Topic: Coq's Abort in Lean


view this post on Zulip Kevin Sullivan (Oct 08 2018 at 14:22):

What is Lean's equivalent of Abort in Coq?

view this post on Zulip Mario Carneiro (Oct 08 2018 at 14:23):

what does it do?

view this post on Zulip Kevin Sullivan (Oct 08 2018 at 14:25):

@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).

view this post on Zulip Mario Carneiro (Oct 08 2018 at 14:26):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 14:26):

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

view this post on Zulip Kevin Sullivan (Oct 08 2018 at 14:38):

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.

view this post on Zulip Mario Carneiro (Oct 08 2018 at 14:39):

Usually we use sorry for that

view this post on Zulip Kevin Sullivan (Oct 08 2018 at 17:44):

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.

view this post on Zulip Simon Hudon (Oct 08 2018 at 17:45):

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

view this post on Zulip Sebastian Ullrich (Oct 08 2018 at 17:49):

example may be more appropriate in that case

view this post on Zulip Simon Hudon (Oct 08 2018 at 17:51):

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

view this post on Zulip Mario Carneiro (Oct 08 2018 at 17:56):

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

view this post on Zulip Kevin Sullivan (Oct 09 2018 at 15:37):

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.

view this post on Zulip Sebastian Ullrich (Oct 09 2018 at 15:59):

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.

view this post on Zulip Rob Lewis (Oct 09 2018 at 15:59):

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.

view this post on Zulip Sebastian Ullrich (Oct 09 2018 at 15:59):

Nice timing :)

view this post on Zulip Rob Lewis (Oct 09 2018 at 15:59):

Haha, good timing!

view this post on Zulip Sebastian Ullrich (Oct 09 2018 at 15:59):

:D

view this post on Zulip Patrick Massot (Oct 09 2018 at 15:59):

Amazing duo

view this post on Zulip Rob Lewis (Oct 09 2018 at 16:00):

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

view this post on Zulip Rob Lewis (Oct 09 2018 at 16:00):

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

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:01):

No, the Lean way is to finish the proof.

view this post on Zulip Rob Lewis (Oct 09 2018 at 16:01):

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

view this post on Zulip Patrick Massot (Oct 09 2018 at 16:01):

Even if == suddenly appear in the proof

view this post on Zulip Simon Hudon (Oct 09 2018 at 19:52):

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

view this post on Zulip Kevin Sullivan (Oct 10 2018 at 03:27):

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.

view this post on Zulip Simon Hudon (Oct 10 2018 at 03:29):

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

view this post on Zulip Rob Lewis (Oct 10 2018 at 08:58):

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

view this post on Zulip Rob Lewis (Oct 10 2018 at 08:59):

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


Last updated: May 18 2021 at 16:25 UTC