I started to work on a branch withCoqPrime
of 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 :
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.
until something has moved to CoqPrime, we can depend on both CoqPrime and Pocklington
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.
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
easiest to ping me in the PR on GitHub when you have the PR in the right state
@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 Pocklington
with 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?
@Pierre Castéran OK, I'll take a look at this branch and add the required CI boilerplate ASAP, hopefully by tonight.
I suggest we simply skip testing with older Coq versions that are difficult to support - I'll set lower version bounds in opam.
How can I help the best with converting to CoqPrime?
for example, Pierre could make a list of Pocklington theorem statements that should be "re-proved" using only CoqPrime
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
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
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 Import
from 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 CoqPrime
and the standard library.
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".
@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
I tried without eauto
on Coq 8.16.0 as well (just auto. Qed.
), works there too
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.
OK, so with commit 02584ea it seems we are good again in CI
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)
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
.
Current state: https://pastebin.com/LRdYxMSz
More Admitted
appeared (for helper lemmas).
Is it of any use?
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.
Great, then one can replace all the Lincomb
with Bezout
, right? :) I will try that.
Did it, no more Lincomb
.
https://pastebin.com/FVebgYDG - six admit
s left. For tomorrow, probably.
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
Indeed, the branch withCoqPrime
, which replaces progressively Pocklington
with Coqprime
has a draft pull request.
The invariant we should maintain on this branch is that all goedel
compiles, and there is no Admitted
, but requires of Pocklington
are 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.
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.
If someone could prove this, the chRem file would be finished. At least my a bit messy version of it.
Karl Palmskog said:
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 thanmaster
get CI runs
Ok, will learn how to do that.
@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 nat
and Z
and technical lemmas but it may be OK.
I start with the following sub-goal (after a few destruct
and 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 n0
and n
. Obviously , g <= n0
.
By H0
, g=1 \/ g=n
.
g=1
, should work.g=n
, we would have a contradiction with Hn0
.Thank you for the hints. It's done! :)
So, we have an Admitted-free Pocklington independent Goedel
?!
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.
Thanks! So, we have now to change some boilerplate (remove links to Pocklington) ?
If it works, may be merged into master ?
@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
.
Looks green :tada: !
I just removed some obsolete comments and pushed again.
@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
@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
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 progressOK, I removed tryCoqPrime.v
(and its reference in _CoqProject)
So, may I merge now?
@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
.
Right! Indeed, it's all the file compatCoqPrime.v
I forgot to remove!
I do it now.
Done!
maybe we could consider submitting lemmas to CoqPrime now? Were there any specific ones missing?
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.
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.
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 gcd
and [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 Pocklington
are covered by CoqPrime
.
I think this is the file with the CoqPrime stuff: https://github.com/coq-community/goedel/blob/master/theories/chRem.v
Ah, sorry, I forgot to give the link!
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 CoqPrime
I knwo that our version of Pocklington is more general than their but I guess you are not using it in Goedel.
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?
FIne with me
@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.
@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
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.
@Karl Palmskog sure any improvment is welcome!
Only the constants div_eucl
, coPrimeBeta
, gtBeta
, uniqueRem
and betaTheorem1
from chRem
occur in the file PRrepresentable.v
of the Goedel library.
modulo
sounds like a very general/generic name, yes, you could change to something more specific like eucl_modulo
I changed modulo
into div_eucl
(more appropriate), commited and pushed.
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.
so I can go ahead with the initial CoqPrime PR?
@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?
Great!
Actually, I have coq-coqprime.1.2.0
on opam. Do I have some commands to run in order to have the dev
version ?
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.
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 ?
right, there is a little bit of boilerplate updating, we are not compatible with CoqPrime 1.2.0 after this
if you make a goedel pull request I can take care of the boilerplate and merge
OK, I will do the chRem
and _CoqProject
stuff, and make a PR.
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
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)).
ah yes, right, it actually installs coq-coqprime.dev
everywhere in CI. I will just do a small commit directly to master
then
OK, all boilerplate up to date.
Are there plans for new CoqPrime and Goedel releases following these changes?
Btw, is the new CoqPrime compatible with recent Coq versions like >= 8.15?
Yes, its CI tests Coq 8.15 and Coq dev
So we may limit Pocklington to 8.14 and lower? Could be nice to advertise the changes when we make the new releases.
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?
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 ?
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