Pierre Castéran (Sep 18 2022 at 16:41): Pierre Castéran (Sep 18 2022 at 16:41):I started to work on a branch withCoqPrimeof goedel, progressively replacing some Pocklington stuff with standard library's or Coqprime.
Looks like some lemmas or definitions of Pocklington are missing from the other libraries.
This modification should take time: What about :
Karl Palmskog (Sep 18 2022 at 16:50):my view: if it has anything to do with primes, do a pull request to CoqPrime. Since CoqPrime is in the Coq Platform, everyone will benefit.
Karl Palmskog (Sep 18 2022 at 16:50):until something has moved to CoqPrime, we can depend on both CoqPrime and Pocklington
Pierre Castéran (Sep 18 2022 at 16:59):OK, so I will continue to work with both libraries and list what should be added to Coqprime.
Meanwhile, should we add something to this branch's boilerplate, if we want to test CI on push?
Some lemmas are about the injection from nat to Z, and may benefit to standard library too.
Karl Palmskog (Sep 18 2022 at 17:00):if you make a PR that fails (that uses both CoqPrime and Pocklington, for example) I can edit it and add the dependencies to make CI pass
Karl Palmskog (Sep 18 2022 at 17:01):easiest to ping me in the PR on GitHub when you have the PR in the right state
Pierre Castéran (Sep 23 2022 at 12:16):@Karl Palmskog I created a PR on branch withCoqPrime that fails as expected (requiring CoqPrime, but maybe also for the apply with renaming issue for old versions of Coq).
Note that the full replacement of Pocklingtonwith CoqPrime will take some time, since it would involve several definitions of divide and gcd (with nat, Z, positive, meaning of "greatest common divisor" (w.r.t. which order: <=or |?), etc.
Of course, compatibility lemmas should be added gradually. For the time being, some old proofs have been already shortened and structured (bullets, named intros, etc.)
In short, we may work mainly on this version, but with recents versions of Coq?
Karl Palmskog (Sep 23 2022 at 12:17):@Pierre Castéran OK, I'll take a look at this branch and add the required CI boilerplate ASAP, hopefully by tonight.
Karl Palmskog (Sep 23 2022 at 12:18):I suggest we simply skip testing with older Coq versions that are difficult to support - I'll set lower version bounds in opam.
Lessness (Sep 24 2022 at 20:40):How can I help the best with converting to CoqPrime?
Karl Palmskog (Sep 24 2022 at 21:16):for example, Pierre could make a list of Pocklington theorem statements that should be "re-proved" using only CoqPrime
Karl Palmskog (Sep 24 2022 at 21:21):CI passes now: https://github.com/coq-community/goedel/pull/13
I excluded testing with Coq master, since hydra-battles repo/package currently doesn't build with Coq master
Pierre Castéran (Sep 25 2022 at 06:25):Ok, I will list which lemmas of chRem.v are applied in the other files of goedel/theories.
I will put comments in the branch withCoqPrime
Pierre Castéran (Sep 25 2022 at 08:25):Looks like a few lemmas and function definitions are used in the rest of goedel's files.
Indeed, doing grep chRem *.v, I noticed that only PRrepresentable.v is involved.
Then I removed the Importfrom the Require Import chRem and looked at the error messages.
I found a simple function definition coPrimeBeta and a few lemmas: modulo, gtBeta (should be easy to adapt).
The only "big" lemma is betaTheorem1 (which applies a bunch of helper lemmas in chRem.v)
My intuition: the goal is to prove the above lemmas (and, if necessary, some helpers from chRem), using only CoqPrimeand the standard library.
Pierre Castéran (Sep 25 2022 at 10:12):There is an issue in PRrepresentable.v, L.1230.
The commit f705f800dc (by @Karl Palmskog ) works on CI, but on my computer, fails with an "incomplete proof" error.
If I add "eauto" , it compiles on my computer, but the CI fails now with "no such goal".
Karl Palmskog (Sep 25 2022 at 10:41):@Pierre Castéran which Coq version are you using? I tried without the eauto on 8.15.2, and there PRepresentable.v compiles for me
Karl Palmskog (Sep 25 2022 at 11:12):I tried without eauto on Coq 8.16.0 as well (just auto. Qed.), works there too
Pierre Castéran (Sep 25 2022 at 11:13):coqtop --version
The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.10.2
I (shamefully, without understanding the issue) fixed the problem, by adding an ;eauto to the tactic which created this sub-goal.
Karl Palmskog (Sep 25 2022 at 11:14):OK, so with commit 02584ea it seems we are good again in CI
Pierre Castéran (Sep 25 2022 at 11:33):At least, it illustrates the importance of bullets :grinning:
Perhaps, its a problem with coqrc files ? (But I have no such file in my home directory)
Lessness (Sep 25 2022 at 12:38):Got this far in chRem.v file: https://pastebin.com/x9MFxBFn
With one admit of gcd_lincomb_nat.
Lemma gcd_lincomb_nat:
forall (x y d : nat),
(x > 0)%nat ->
Zis_gcd (Z_of_nat x) (Z_of_nat y) (Z_of_nat d) ->
LinComb (Z_of_nat d) (Z_of_nat x) (Z_of_nat y).
Now at primeDiv .
Lessness (Sep 25 2022 at 14:00):Current state: https://pastebin.com/LRdYxMSz
More Admitted appeared (for helper lemmas).
Is it of any use?
Pierre Castéran (Sep 25 2022 at 14:40):Indeed, Lincomb is named Bezout in Coq.ZArith.Znumtheory (with a slight difference).
Lemma LinComb_Bezout x y d :
LinComb d x y <-> Bezout x y d.
Proof.
split.
- destruct 1 as [u [v H]]; exists u v;
rewrite (Z.mul_comm u), (Z.mul_comm v); now symmetry.
- destruct 1 as [u v H].
red; exists u, v; rewrite (Z.mul_comm x), (Z.mul_comm y);
now symmetry.
Qed.
Lemma gcd_lincomb_nat:
forall (x y d : nat),
(x > 0)%nat ->
Zis_gcd (Z_of_nat x) (Z_of_nat y) (Z_of_nat d) ->
Bezout (Z_of_nat x) (Z_of_nat y) (Z_of_nat d) .
Proof.
intros x y d H H0; destruct (Zis_gcd_bezout (Z.of_nat x)
(Z.of_nat y) (Z.of_nat d) H0).
exists u v; assumption.
Qed.
Thus, we don't need this Admitted any more.
Lessness (Sep 25 2022 at 17:33):Great, then one can replace all the Lincomb with Bezout, right? :) I will try that.
Lessness (Sep 25 2022 at 17:47):Did it, no more Lincomb.
Lessness (Sep 25 2022 at 18:04):https://pastebin.com/FVebgYDG - six admits left. For tomorrow, probably.
Karl Palmskog (Sep 26 2022 at 12:22):if you can, please use pull requests to manage contributions. Recall that pull requests need not target the master branch. I can adjust CI so that pull requests against branches other than master get CI runs
Pierre Castéran (Sep 27 2022 at 06:43):Indeed, the branch withCoqPrime, which replaces progressively Pocklington with Coqprimehas a draft pull request.
The invariant we should maintain on this branch is that all goedelcompiles, and there is no Admitted, but requires of Pocklingtonare provisionally allowed.
Besides this branch, it may be useful to have a draft branch, e.g. CoqPrimeAdmitted where no Pocklington is required, but about which we may have discussions.
Lessness (Sep 27 2022 at 08:21):Ok, the only lemma I have left Admitted (in chRem file) is Lemma Prime_prime (n: nat) : Prime n -> prime (Z.of_nat n).
Got stuck with it.
Lessness (Sep 27 2022 at 08:31):If someone could prove this, the chRem file would be finished. At least my a bit messy version of it.
Lessness (Sep 27 2022 at 08:32):Karl Palmskog said:
if you can, please use pull requests to manage contributions. Recall that pull requests need not target the
masterbranch. I can adjust CI so that pull requests against branches other thanmasterget CI runs
Ok, will learn how to do that.
Pierre Castéran (Sep 27 2022 at 09:16):@Lessness
Here's a possible informal proof. Could you verify it's OK (and compatible with your last version) ?
I ignored the usual conversions between natand Z and technical lemmas but it may be OK.
I start with the following sub-goal (after a few destructand split)
n : nat
H : n > 1
H0 : forall q : nat, divides.Divides q n -> q = 1 \/ q = n
n0 : Z
Hn0 : (1 <= n0 < Z.of_nat n)%Z
============================
Zis_gcd n0 (Z.of_nat n) 1
Let g be the gcd of n0and n. Obviously , g <= n0.
By H0, g=1 \/ g=n.
g=1, should work.g=n, we would have a contradiction with Hn0. Lessness (Sep 27 2022 at 10:17):Thank you for the hints. It's done! :)
Pierre Castéran (Sep 27 2022 at 10:35):So, we have an Admitted-free Pocklington independent Goedel ?!
Lessness (Sep 27 2022 at 10:37):It seems so, yes. I tried to make a pull request. Do you see it? That's my first PR, not sure if I did everything right.
Pierre Castéran (Sep 27 2022 at 11:06):Thanks! So, we have now to change some boilerplate (remove links to Pocklington) ?
If it works, may be merged into master ?
Karl Palmskog (Sep 27 2022 at 11:11):@Pierre Castéran if the changes look good to you, please merge them into the withCoqPrime branch (the target of the PR by @Lessness ). I can then change the boilerplate in withCoqPrime to avoid Pocklington. Once CI is green after that, we merge into master.
Pierre Castéran (Sep 27 2022 at 11:37):Looks green :tada: !
I just removed some obsolete comments and pushed again.
Karl Palmskog (Sep 27 2022 at 11:51):@Pierre Castéran I removed Pocklington as a dependency now, and CI is green.
Before merging to master, you probably want to remove theories/tryCoqPrime.v
Karl Palmskog (Sep 27 2022 at 11:58):@Lessness I invited you to collaborate on the goedel repo. If you accept the invite, you can propose changes by creating branches in the goedel repo instead of in your fork. This makes it easier for us to collaborate on changes before merging to master
Karl Palmskog (Sep 27 2022 at 12:04):the typical workflow we use is:
remove-pocklington, and opens a pull request using this branch targeting master. This pull request can be a draft to indicate it's a work in progress Pierre Castéran (Sep 27 2022 at 12:33):OK, I removed tryCoqPrime.v (and its reference in _CoqProject)
So, may I merge now?
Karl Palmskog (Sep 27 2022 at 12:36):@Pierre Castéran fine by me to merge, only comment I have is that you may want to remove the commented-out lemmas in compatCoqPrime.v like Zis_gcd_compat.
Pierre Castéran (Sep 27 2022 at 12:50):Right! Indeed, it's all the file compatCoqPrime.v I forgot to remove!
I do it now.
Pierre Castéran (Sep 27 2022 at 13:08):Done!
Karl Palmskog (Sep 27 2022 at 13:27):maybe we could consider submitting lemmas to CoqPrime now? Were there any specific ones missing?
Pierre Castéran (Sep 27 2022 at 13:32):Ok, I'll make some editing tomorrow on the chRem.v file. Then we may ask Laurent if he thinks some lemmas may be useful in CoqPrime.
Karl Palmskog (Sep 27 2022 at 13:39):we should also think about the future of Pocklington. Since it's not longer a primary concern via Goedel, one could ponder whether key results there could be ported CoqPrime, and then the repo is archived/obsoleted.
Pierre Castéran (Sep 28 2022 at 12:08):Hi, @Laurent Théry
We (@Karl Palmskog , @Lessness and me), finally connected https://github.com/coq-community/goedel to CoqPrime instead of Pocklington.
Indeed, we had just to modify a file theories/chRem.v dedicated to the Chinese remainder properties.
Thus, it raises to (non-urgent) questions
The mentionned file is mainly dedicated to arithmetic properties of the gcdand [co]-primality on natural numbers.
Only the other files are Gödel-specific.
Is it worth migrating some lemmas to CoqPrime?
On the other side, I don't kwow whether all parts of Pocklingtonare covered by CoqPrime.
Karl Palmskog (Sep 28 2022 at 12:26):I think this is the file with the CoqPrime stuff: https://github.com/coq-community/goedel/blob/master/theories/chRem.v
Pierre Castéran (Sep 28 2022 at 12:31):Ah, sorry, I forgot to give the link!
Laurent Théry (Sep 28 2022 at 17:27):Great! When looking at theories/chRem.v my first impression is that it would benefit a lot by using MathComp. I did it recently for the elliptic curve part of Coqprime and it is clearly smoother. But II understand it is a big change. Anyway I see no problem to add chRem.v to the N part of Coqprime. For Pocklington vs CoqPrimeI knwo that our version of Pocklington is more general than their but I guess you are not using it in Goedel.
Karl Palmskog (Sep 28 2022 at 17:29):I think we could definitely put on our TODO to convert results from chRem.v to use MathComp, but maybe we do pull request now to add it to CoqPrime and do additional pull requests to convert to MathComp later?
Laurent Théry (Sep 28 2022 at 17:30):FIne with me
Karl Palmskog (Sep 28 2022 at 17:32):@Pierre Castéran do you want to do any final touches to chRem.v before we make a pull request to CoqPrime? Otherwise, I can open the PR and notify people.
Karl Palmskog (Sep 28 2022 at 17:48):@Laurent Théry could I also make an orthogonal PR to CoqPrime to modernize the in-repo opam handling a bit? For example, having descr/url like here is deprecated: https://github.com/thery/coqprime/tree/master/opam
Pierre Castéran (Sep 28 2022 at 18:16):What I can do tomorrow is to verify which symbols of chRem are imported by goedel (I believe only five of them).
So, the adaptation to MathComp would be free to use the usual naming conventions for all other helpers.
Laurent Théry (Sep 28 2022 at 18:27):@Karl Palmskog sure any improvment is welcome!
Pierre Castéran (Sep 28 2022 at 19:08):Only the constants div_eucl, coPrimeBeta, gtBeta, uniqueRem and betaTheorem1 from chRemoccur in the file PRrepresentable.v of the Goedel library.
Karl Palmskog (Sep 28 2022 at 19:09):modulo sounds like a very general/generic name, yes, you could change to something more specific like eucl_modulo
Pierre Castéran (Sep 28 2022 at 19:23):I changed modulo into div_eucl (more appropriate), commited and pushed.
Pierre Castéran (Sep 29 2022 at 07:45):I made a few more minor changes this morning (mainly making the proof structure more visible).
But, if the future of chRem is to use SSreflect tactics, the best is to complete this work with MathComp style.
So, is the following sequence appropriate?
- migrate `chRem`as is, through a PR, and update `goedel`'s _CoqProject
- work on a fork of `CoqPrime` in order to build a MathComp-compatible version.
@Pierre Castéran currently, CoqPrime doesn't depend on MathComp, so I would go for the first bullet point, and then ask Laurent about the best way to do the second one.
Karl Palmskog (Sep 29 2022 at 07:49):so I can go ahead with the initial CoqPrime PR?
Karl Palmskog (Sep 29 2022 at 13:29):@Pierre Castéran the change to CoqPrime was merged. Should we start to depend on CoqPrime master (dev version in opam) now? Or do we do a tag/release before that?
Pierre Castéran (Sep 29 2022 at 14:26):Great!
Actually, I have coq-coqprime.1.2.0 on opam. Do I have some commands to run in order to have the devversion ?
Karl Palmskog (Sep 29 2022 at 14:28):if you want to install the dev version of coq-coq-prime, you will have to add the extra-dev repo:
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
fair warning that this adds a bunch of dev versions of packages, so maybe good to use a separate switch. coq-coqprime.dev works with Coq 8.15 and 8.16 just fine, though.
Pierre Castéran (Sep 29 2022 at 14:58):Yeah !
On my version of goedel I put the line From Coqprime Require Import ChineseRem. instead of the old chRem, and it worked ! :tada:
The next steps: removing chRem.v(also from _CoqProject) and update a few boilerplates ?
Karl Palmskog (Sep 29 2022 at 15:00):right, there is a little bit of boilerplate updating, we are not compatible with CoqPrime 1.2.0 after this
Karl Palmskog (Sep 29 2022 at 15:01):if you make a goedel pull request I can take care of the boilerplate and merge
Pierre Castéran (Sep 29 2022 at 15:03):OK, I will do the chRemand _CoqProjectstuff, and make a PR.
Karl Palmskog (Sep 29 2022 at 15:09):for the record, chRem was pretty cryptic, I didn't even make the connection until I looked through the file, ChineseRem.v seemed more clear and in line with CoqPrime conventions
Pierre Castéran (Sep 29 2022 at 15:14):Yes, me too ! I took "ch" for "character" until I arrived at the end of the file.
(Ups, I forgot I was on master, so it didn't create a PR (but it works)).
Karl Palmskog (Sep 29 2022 at 15:15):ah yes, right, it actually installs coq-coqprime.dev everywhere in CI. I will just do a small commit directly to master then
Karl Palmskog (Sep 29 2022 at 15:18):OK, all boilerplate up to date.
Théo Zimmermann (Oct 01 2022 at 17:24):Are there plans for new CoqPrime and Goedel releases following these changes?
Pierre Castéran (Oct 01 2022 at 18:05):Btw, is the new CoqPrime compatible with recent Coq versions like >= 8.15?
Théo Zimmermann (Oct 01 2022 at 18:13):Yes, its CI tests Coq 8.15 and Coq dev
Pierre Castéran (Oct 01 2022 at 18:17):So we may limit Pocklington to 8.14 and lower? Could be nice to advertise the changes when we make the new releases.
Théo Zimmermann (Oct 01 2022 at 18:22):Yes, that's definitely possible. And the release notes should of course explain these changes. Did you mean advertise beyond that, e.g., by an announcement on Discourse?
Pierre Castéran (Oct 01 2022 at 18:51):I thought about a recall that Coq-community considers how important historical contributions like Russel’s are, hence supports their maintenance and adaptation to new techniques and idioms of modern Coq. Then explain the dependency graph, before and after the transformation. We may say also that a Zulip stream is dedicated to this bunch of projects.
It may be a post in our stream and/or in a more global place ?
Théo Zimmermann (Oct 01 2022 at 20:03):Very interesting idea. This would indeed deserve a post in a more global place I think.
Last updated: Jun 11 2023 at 00:30 UTC