Stream: Hydras & Co. universe

Topic: Goedel, Pocklington & CoqPrime


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

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

view this post on Zulip Karl Palmskog (Sep 18 2022 at 16:50):

until something has moved to CoqPrime, we can depend on both CoqPrime and Pocklington

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

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

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

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

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

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

view this post on Zulip Lessness (Sep 24 2022 at 20:40):

How can I help the best with converting to CoqPrime?

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

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

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

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

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

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

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

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

view this post on Zulip Karl Palmskog (Sep 25 2022 at 11:14):

OK, so with commit 02584ea it seems we are good again in CI

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

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

view this post on Zulip Lessness (Sep 25 2022 at 13:31):

Now at primeDiv .

view this post on Zulip Lessness (Sep 25 2022 at 14:00):

Current state: https://pastebin.com/LRdYxMSz
More Admitted appeared (for helper lemmas).

Is it of any use?

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

view this post on Zulip Lessness (Sep 25 2022 at 17:33):

Great, then one can replace all the Lincomb with Bezout, right? :) I will try that.

view this post on Zulip Lessness (Sep 25 2022 at 17:47):

Did it, no more Lincomb.

view this post on Zulip Lessness (Sep 25 2022 at 18:04):

https://pastebin.com/FVebgYDG - six admits left. For tomorrow, probably.

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

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

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

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

view this post on Zulip 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 master branch. I can adjust CI so that pull requests against branches other than master get CI runs

Ok, will learn how to do that.

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

view this post on Zulip Lessness (Sep 27 2022 at 10:17):

Thank you for the hints. It's done! :)

view this post on Zulip Pierre Castéran (Sep 27 2022 at 10:35):

So, we have an Admitted-free Pocklington independent Goedel ?!

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

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

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

view this post on Zulip Pierre Castéran (Sep 27 2022 at 11:37):

Looks green :tada: !
I just removed some obsolete comments and pushed again.

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

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

view this post on Zulip Karl Palmskog (Sep 27 2022 at 12:04):

the typical workflow we use is:

view this post on Zulip Pierre Castéran (Sep 27 2022 at 12:33):

OK, I removed tryCoqPrime.v (and its reference in _CoqProject)
So, may I merge now?

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

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

view this post on Zulip Pierre Castéran (Sep 27 2022 at 13:08):

Done!

view this post on Zulip Karl Palmskog (Sep 27 2022 at 13:27):

maybe we could consider submitting lemmas to CoqPrime now? Were there any specific ones missing?

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

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

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

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

view this post on Zulip Pierre Castéran (Sep 28 2022 at 12:31):

Ah, sorry, I forgot to give the link!

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

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

view this post on Zulip Laurent Théry (Sep 28 2022 at 17:30):

FIne with me

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

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

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

view this post on Zulip Laurent Théry (Sep 28 2022 at 18:27):

@Karl Palmskog sure any improvment is welcome!

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

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

view this post on Zulip Pierre Castéran (Sep 28 2022 at 19:23):

I changed modulo into div_eucl (more appropriate), commited and pushed.

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

view this post on Zulip Karl Palmskog (Sep 29 2022 at 07:48):

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

view this post on Zulip Karl Palmskog (Sep 29 2022 at 07:49):

so I can go ahead with the initial CoqPrime PR?

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

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

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

view this post on Zulip Karl Palmskog (Sep 29 2022 at 14:29):

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.

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

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

view this post on Zulip Karl Palmskog (Sep 29 2022 at 15:01):

if you make a goedel pull request I can take care of the boilerplate and merge

view this post on Zulip Pierre Castéran (Sep 29 2022 at 15:03):

OK, I will do the chRemand _CoqProjectstuff, and make a PR.

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

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

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

view this post on Zulip Karl Palmskog (Sep 29 2022 at 15:18):

OK, all boilerplate up to date.

view this post on Zulip Théo Zimmermann (Oct 01 2022 at 17:24):

Are there plans for new CoqPrime and Goedel releases following these changes?

view this post on Zulip Pierre Castéran (Oct 01 2022 at 18:05):

Btw, is the new CoqPrime compatible with recent Coq versions like >= 8.15?

view this post on Zulip Théo Zimmermann (Oct 01 2022 at 18:13):

Yes, its CI tests Coq 8.15 and Coq dev

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

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

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

view this post on Zulip 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 18 2024 at 00:02 UTC