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?

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.

User interfaces being proof general and such?

So you type `Set Nested Proofs Allowed`

and then something like

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

Or what is the syntax?

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

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

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

Thanks :-)

On the original question, there is Program.

```
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!

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