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

`Succeed Qed. Restart.`

lets you check the first proof is done and start over

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

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

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

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.
Locate add_comm.
About Alt.add_comm.
```

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

```
Definition typ := Type.
Lemma proof1 : Type.
Proof. exact typ. Qed.
Lemma proof2 : Type.
Proof. exact nat. Qed.
Fail Check proof1 : typ.
Check proof2 : typ.
```

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

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.

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.

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.

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.

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

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

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

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?

no

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

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

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

It is exactly that.

OK then what about this:

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

the section is completely useless here

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

I don't know what you mean

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

As in `Context (x : Type@{u}) (y : Type@{v})`

and have `x`

and `y`

used in both proofs

What about with universe polymorphism?

it works exactly the same as if they were axioms

univ polymorphism disables async so not relevant

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