Raul (Sep 14 2022 at 22:36): 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. ....
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?).
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.
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):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?
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
Ali Caglayan (Sep 15 2022 at 12:59):What about with universe polymorphism?
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: Apr 19 2024 at 20:01 UTC