Arnoud van der Leer (Apr 24 2023 at 06:10): 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?
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.
Arnoud van der Leer (Apr 24 2023 at 06:37):User interfaces being proof general and such?
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?
Guillaume Melquiond (Apr 24 2023 at 06:39):Yes. Though Proof General being line-oriented, it never had any issue with the feature.
Guillaume Melquiond (Apr 24 2023 at 06:39):No, you just type Lemma foo : ... Qed. apply foo.
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.
Arnoud van der Leer (Apr 24 2023 at 06:43):Thanks :-)
Paolo Giarrusso (Apr 24 2023 at 08:37):On the original question, there is Program.
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.
Ooooh, that is an interesting one. Thanks!
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: Apr 20 2024 at 13:01 UTC