Stream: Coq users

Topic: Multiple Proofs


view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Sep 15 2022 at 06:06):

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

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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. ....

view this post on Zulip 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.

Locate add_comm.
About Alt.add_comm.

view this post on Zulip 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?).

view this post on Zulip 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.

view this post on Zulip abab9579 (Sep 15 2022 at 08:11):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Sep 15 2022 at 12:53):

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

view this post on Zulip 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

view this post on Zulip abab9579 (Sep 15 2022 at 12:54):

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

view this post on Zulip Théo Zimmermann (Sep 15 2022 at 12:55):

It is exactly that.

view this post on Zulip Ali Caglayan (Sep 15 2022 at 12:56):

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?

view this post on Zulip Gaëtan Gilbert (Sep 15 2022 at 12:57):

the section is completely useless here

view this post on Zulip Ali Caglayan (Sep 15 2022 at 12:57):

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

view this post on Zulip Gaëtan Gilbert (Sep 15 2022 at 12:58):

I don't know what you mean

view this post on Zulip Gaëtan Gilbert (Sep 15 2022 at 12:58):

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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Sep 15 2022 at 12:59):

What about with universe polymorphism?

view this post on Zulip Gaëtan Gilbert (Sep 15 2022 at 12:59):

it works exactly the same as if they were axioms

view this post on Zulip Gaëtan Gilbert (Sep 15 2022 at 12:59):

univ polymorphism disables async so not relevant

view this post on Zulip 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: Jan 29 2023 at 04:05 UTC