## Stream: Coq users

### Topic: Multiple Proofs

#### Raul (Sep 14 2022 at 22:36):

Why isn't possible to define multiple proofs for a proposition (e.g. with multiple Proof. Qed. clauses) if anyways proposition definitions are opaque?

#### Paolo Giarrusso (Sep 15 2022 at 06:06):

`Succeed Qed. Restart.` lets you check the first proof is done and start over

#### Paolo Giarrusso (Sep 15 2022 at 06:07):

But not sure if that's what you want: why do you want to have a second proof?

#### Paolo Giarrusso (Sep 15 2022 at 06:09):

As a partial answer, proofs aren't entirely opaque: at least Print and Print Assumptions can look at their contents. And IIUC universe inference can leak proof details as well...

#### Enrico Tassi (Sep 15 2022 at 06:48):

why do you need to use the very same name for all he proofs?
Also consider

``````Definition statement := forall x y, ....
Lemma proof1 : statement. ....
Lemma proof2 : statement. ....
``````

#### Pierre Castéran (Sep 15 2022 at 07:06):

You may also use the module system:

``````Require Import Arith Lia.
Module Alt.
Lemma add_comm n p : n + p = p + n.
Proof. lia. Qed.
End Alt.

``````

#### Raul (Sep 15 2022 at 07:54):

I think Succed - Restart would fit what I thought, it was just for convinience when writing mathematical texts, where multiple proofs might help undersanding better the result but it's unnecessary to record all of them.
But I don't see how IIUC can leak proof details (I mean, depending on the type level of the definitions used inside? Wouldn't it end up being the same always?).

#### Gaëtan Gilbert (Sep 15 2022 at 08:06):

``````Definition typ := Type.

Lemma proof1 : Type.
Proof. exact typ. Qed.

Lemma proof2 : Type.
Proof. exact nat. Qed.

Fail Check proof1 : typ.
Check proof2 : typ.
``````

#### abab9579 (Sep 15 2022 at 08:11):

Oh no.. so "opaque" proofs will, in fact, leak details here and there through universe?

#### Théo Zimmermann (Sep 15 2022 at 08:41):

Yes :sad:, this is why the async compilation mechanism, in CoqIDE for instance, has a button to "Fully check the document". Without universes, the parallel checking would be sufficient.

#### Karl Palmskog (Sep 15 2022 at 12:19):

for precision, I think you mean "asynchronous checking". Parallelism at proof level is only possible thanks to async, but you can use async proofs without parallelism.

#### Karl Palmskog (Sep 15 2022 at 12:21):

would be interesting if there were some easy (syntactic?) conditions that guaranteed universe consistency in async proof checking case. I think a lot of Coq projects are using universes (and universe polymorphism) in a very limited way.

#### Ali Caglayan (Sep 15 2022 at 12:30):

AFAIK sections make universe checking hard since all the proofs have to be checked before the universe constraints at the end of a section can be checked.

#### Ali Caglayan (Sep 15 2022 at 12:31):

If you are not using sections then universes don't impede async checking (at least that I know of)

#### Gaëtan Gilbert (Sep 15 2022 at 12:34):

Karl Palmskog said:

would be interesting if there were some easy (syntactic?) conditions that guaranteed universe consistency in async proof checking case. I think a lot of Coq projects are using universes (and universe polymorphism) in a very limited way.

there is no such condition, applying a constant to another constant can involve arbitrary universe constraints

#### Gaëtan Gilbert (Sep 15 2022 at 12:34):

Ali Caglayan said:

AFAIK sections make universe checking hard since all the proofs have to be checked before the universe constraints at the end of a section can be checked.

there are no constraints at the end of the section, you are confused somehow

#### Ali Caglayan (Sep 15 2022 at 12:49):

Gaëtan Gilbert said:

Ali Caglayan said:

AFAIK sections make universe checking hard since all the proofs have to be checked before the universe constraints at the end of a section can be checked.

there are no constraints at the end of the section, you are confused somehow

Yes probably. Aren't the universe constraints checked at the end of a section when everything is being generalized?

#### Gaëtan Gilbert (Sep 15 2022 at 12:53):

no
there is nothing new to check at the end of a section

#### Gaëtan Gilbert (Sep 15 2022 at 12:54):

it is all checked during the section
the end of the section only does the generalization
in other words any failure of `End` for a section is a bug

#### abab9579 (Sep 15 2022 at 12:54):

I thought section was a syntactic construct to avoid writing down environment again and again..

#### Théo Zimmermann (Sep 15 2022 at 12:55):

It is exactly that.

#### Ali Caglayan (Sep 15 2022 at 12:56):

``````Section sec.
Universe u v.

Lemma a : A. Proof. (* force u = v *) Qed.
Lemma b : B. Proof. (* force u <> v *) Qed.

End sec.
``````

How does this work with async?

#### Gaëtan Gilbert (Sep 15 2022 at 12:57):

the section is completely useless here

#### Ali Caglayan (Sep 15 2022 at 12:57):

Right we could add some Type arguments to both lemmas for the universes.

#### Gaëtan Gilbert (Sep 15 2022 at 12:58):

I don't know what you mean

#### Gaëtan Gilbert (Sep 15 2022 at 12:58):

in any case sections have no interesting interaction with monomorphic (global) universes

#### Ali Caglayan (Sep 15 2022 at 12:58):

As in `Context (x : Type@{u}) (y : Type@{v})` and have `x` and `y` used in both proofs

#### Gaëtan Gilbert (Sep 15 2022 at 12:59):

it works exactly the same as if they were axioms

#### Gaëtan Gilbert (Sep 15 2022 at 12:59):

univ polymorphism disables async so not relevant

#### Ali Caglayan (Sep 15 2022 at 13:00):

hmm ok, I seem to recall @Pierre-Marie Pédrot telling me something like this before, but likely I am misremembering

Last updated: Jun 14 2024 at 17:02 UTC