Stream: Coq users

Topic: Multi-statement abstract


view this post on Zulip Arnoud van der Leer (Apr 24 2023 at 06:10):

Maybe this is in the wrong channel. If so, please relocate :-)
Usually, when doing computer math, types consist of a "data" part and a "properties" part. The properties are usually proof-irrelevant, and to speed up computation, we (some people) usually want those to be opaque. There are two main ways of achieving that: declaring them in a lemma that is closed with Qed. or, if we want to avoid proliferation of lemmas, putting the proofs of properties inside an abstract block. For example, this code that I am currently working on. However, an abstract block can only contain one "tactic element"/statement. This becomes (nigh) impossible and very unpractical when writing longer proofs.
Is there a way of doing abstract (...) but with multiple steps/statements in the proof? I.e. is there a way to communicate to coq "please save the following as an opaque lemma."? Or are there good reasons why there is not such a tactic? I.e. is it incompatible with the way coq is designed, or is has it just not yet been implemented?

view this post on Zulip Guillaume Melquiond (Apr 24 2023 at 06:32):

Actually, it was implemented, and then it got disabled, because it interacted badly with user interfaces. You can reenable it with Set Nested Proofs Allowed, but I wouldn't be surprised if it is completely bitrot nowadays.

view this post on Zulip Arnoud van der Leer (Apr 24 2023 at 06:37):

User interfaces being proof general and such?

view this post on Zulip Arnoud van der Leer (Apr 24 2023 at 06:38):

So you type Set Nested Proofs Allowed and then something like

abstract.
{
  split.
  - ...
  - ...
}

Or what is the syntax?

view this post on Zulip Guillaume Melquiond (Apr 24 2023 at 06:39):

Yes. Though Proof General being line-oriented, it never had any issue with the feature.

view this post on Zulip Guillaume Melquiond (Apr 24 2023 at 06:39):

No, you just type Lemma foo : ... Qed. apply foo.

view this post on Zulip Arnoud van der Leer (Apr 24 2023 at 06:43):

Ah, right. So you still have to state the lemma, but now you can do it inside the proof instead of in advance.

view this post on Zulip Arnoud van der Leer (Apr 24 2023 at 06:43):

Thanks :-)

view this post on Zulip Paolo Giarrusso (Apr 24 2023 at 08:37):

On the original question, there is Program.

view this post on Zulip Paolo Giarrusso (Apr 24 2023 at 08:39):

Program Definition free_monoid_theory : algebraic_theory := ... (* term with holes *)
Next Obligation. ... Qed.
Next Obligation. ... Defined.
Next Obligation. ... Qed.

view this post on Zulip Arnoud van der Leer (Apr 24 2023 at 09:30):

Ooooh, that is an interesting one. Thanks!

view this post on Zulip Gaëtan Gilbert (Apr 24 2023 at 09:40):

Guillaume Melquiond said:

Actually, it was implemented, and then it got disabled, because it interacted badly with user interfaces. You can reenable it with Set Nested Proofs Allowed, but I wouldn't be surprised if it is completely bitrot nowadays.

That is not quite the same IMO, you have no access to the proof context and have to fully restate your goal
If you have a big goal that can be pretty painful


Last updated: Jun 20 2024 at 13:02 UTC