Lessness (Oct 05 2022 at 14:28): Lessness (Oct 05 2022 at 14:28):May I join? I could take the file PRepresentable.v and "bullet" it, for example.
I don't want to duplicate the effort - that's my reason to ask.
Karl Palmskog (Oct 05 2022 at 14:30):current status is here, I think we usually commit quite often: https://github.com/coq-community/goedel/commits/Bullets
So it looks at least like nobody else is working on PRepresentable.v
Karl Palmskog (Oct 05 2022 at 14:32):I disagree about indenting non-proof-script code though [like what is done in Bullets branch currently], it tends to make the margin overflow all the time...
Pierre Castéran (Oct 05 2022 at 15:00):@Lessness . Ok!, thanks !
I’m now working on fol.v (in the Ackermann subdirectory of hydra-battles).
I already bulleted folProp.v
@Karl Palmskog you mean indenting the huge terms in definitions and asserts ? I didn’t find the way to make them human-readable yet…
Karl Palmskog (Oct 05 2022 at 15:01):what I mean is this kind of indenting:
Section s.
Variable x : nat.
Section e.
Variable y : nat.
Definition d := y.
the problem is that this kind of non-proof intending tends to give very long lines when you have complicated proof scripts (since you start already writing the proof indented)
Pierre Castéran (Oct 05 2022 at 15:04):Ah, ok. I used EMacs’ indent-region command too globally…
Karl Palmskog (Oct 05 2022 at 15:04):example:
Section s.
Variable x : nat.
Section e.
Variable y : nat.
Definition d := y.
Lemma my_lemma : True.
Proof.
apply (prove_all_have_message_from_stepwise _ _ _ _ HstepwiseY _ HsY m) in Hm; apply Exists_exists in Hm as [itemY [HitemY Hm]].
I tried a new indenting on Ackermann/folProp.v (branch Bullets).
@Karl Palmskog is it better(except some huge terms inside proof scripts or definitions) ?
Karl Palmskog (Oct 05 2022 at 15:40):@Pierre Castéran looks reasonable in general, much closer to what I think is good indenting, but for example on line 35 - line 39 in folProp.v I don't see the point of indenting more.
Pierre Castéran (Oct 05 2022 at 16:20):Controlling indenting within Emacs doesn't look so simple :grimacing:
Perhaps there some way to tell Emacs or any other tool "please don't indent lines beginning with Proof or Variable, etc."
https://proofassistants.stackexchange.com/questions/636/how-do-i-turn-off-the-aggressive-auto-indent-in-proof-general-coq
There are 45311 LOC in the goedel-Ackermann legacy. I'm just trying to make this code more maintenable.
Karl Palmskog (Oct 05 2022 at 16:32):right, I don't think we want to change the indenting in Ackermann etc. if it somehow already uses the "indent everything" approach. But we could at least limit new "bullet indenting" to only change stuff inside proof scripts, where it actually makes a big difference
Karl Palmskog (Oct 05 2022 at 17:19):my suggestion would be: if using emacs, do careful region-based indenting of the proof scripts after bulleting and avoid changing anything else
Karl Palmskog (Oct 05 2022 at 19:49):for the record, this is exactly the kind of stuff I was aiming to automate with this (and goal structure/level could be taken into account by the neural model), but the funding didn't come through....
Pierre Castéran (Oct 06 2022 at 14:54):I put bullets in three files of theories/ordinals/Ackermann/ fol.v, folProp.vand folProof.v.
In this first step, I kept the meaningless hypotheses names (it should be easier to rename them once the script structure is apparent). Same thing for Coq-8.16 deprecation.
I plan to use now these three files to think about alectryon-based documentation of the goedel stuff.
Btw, the CI failed on dev with an error message related with coqide ???
Error: The compilation of coqide-server.dev failed at "dune build -p coqide-server -j 2 @install".
this is a known problem with the MathComp dev Docker image, see here. I will open a PR to fix this.
Karl Palmskog (Oct 06 2022 at 14:57):@Pierre Castéran or maybe easiest if I makje a commit to your Bullets PR to fix CI?
Karl Palmskog (Oct 06 2022 at 16:07):I fixed the Docker CI job, but now there is a (possibly spurious) error with the Nix doc job:
File "./theories/ordinals/Prelude/Sort_spec.v", line 6, characters 0-39:
Error:
/home/runner/work/hydra-battles/hydra-battles/theories/ordinals/Prelude/DecPreOrder.vo: premature end of file. Try to rebuild it.
make[1]: *** [Makefile.coq:771: theories/ordinals/Prelude/Sort_spec.glob] Error 1
make[1]: *** Waiting for unfinished jobs....
make[1]: Leaving directory '/home/runner/work/hydra-battles/hydra-battles'
make: *** [Makefile:5: html] Error 2
Works now! :tada:
By the way, do we insert your blue hydra in the book (possibly in the gallery of pages 2 to 4, with a caption at your convenance) ?
Karl Palmskog (Oct 06 2022 at 18:38):OK, I will do separate PR to add the blue hydra-rooster
Karl Palmskog (Oct 06 2022 at 20:57):PR done, I decided to call it "The incomplete rooster hydra"
Pierre Castéran (Oct 07 2022 at 19:44):I merged the Bullets branch of hydra-battles into master, and started to document files on first order logic.
It'nice to work with the Alectryon toolkit, particularly thanks to the independance of the chapter structures w.r.t. the Coq files.
First pages in chapter 11 and 12 of the book.
Karl Palmskog (Oct 07 2022 at 19:47):maybe we could ask the people developing the "new" first-order library to comment on the differences between Russel's and their library:
Pierre Castéran (Oct 07 2022 at 21:04):At first sight, they look quite advanced.
I see two questions:
Is it worth maintaining and documenting Russel’s work for historical reasons, given the existence of a more modern library?
Considering the hydra-battles project, the theorem we would like to prove in Coq is that the termination of hydra battles is not provable in PA. Are there in the new library tools that could help us better than the Goedel project?
Anyway, it’s worth looking at their library.
Lessness (Oct 08 2022 at 12:56):It seems that I need help a bit. https://pastebin.com/1CVJFEh5
I have problem at line 4299, where apply Hrecn isn't working ("unable to unify"). And I can't find the difference/reason/anything that causes this problem. :(
Lessness (Oct 08 2022 at 13:46):Found my mistake, now it's working.
Pierre Castéran (Oct 08 2022 at 14:03):Indeed, this lemma looks nightmarish! Just after a huge Ltac definition !!!
Lessness (Oct 08 2022 at 14:19):Yeah, it is. Random thought - maybe that's something to automate (by some plugin, dunno)?
But I don't understand yet what's the lemma proving, I'm just bullet-ing it for now.
Pierre Castéran (Oct 08 2022 at 14:43):Representability is defined in hydra-battles/theories/ordinals/Ackermann/expressible.v
Indeed, when we defined subprojects, we split the old goedel contrib in two parts:
the subdirectory theories/ordinal/Ackermann of hydra battles and the theories subdirectory of goedel.
The criterium was to put in Ackermann all the files that don't require properties of prime numbers (mainly for technical reasons).
So, the basis of logic (syntax, proofs ) are defined in Ackermann.
I think a reasonable strategy is to look first at the most basic files, in order to understand what is proved in these libraries.
For instance, understanding the definitions in expressibleand how they are used in the library could be very interesting.
Like I did with primitive recursive functions, cryptic definitions and lemma statements could be documented (paraphrases, examples, exercises).
Structuring the proofs is important if we maintain goedel, because the code is hard to maintain as it is, but it has less priority than having an idea of the contents of this library, and what could be added to it.
As @Karl Palmskog mentionned, we woul also have to compare various libraries on this topic.
Karl Palmskog (Oct 08 2022 at 14:52):I think Russell's encodings of Goedel and FOL and primitive recursive functions are worth preserving, both for historical reasons and since primitive recursion theory and FOL and Goedel is not yet part of the Coq Platform. In the worst case, we could add code to the Coq CI to have it auto-"maintained" (kept working with latest Coq version).
Karl Palmskog (Oct 08 2022 at 14:55):but it's an unfortunate trend in the Coq world that people make a ton of libraries for the same things and don't compare and don't document. I always thought it was nice in light of this that Hydras & Co. aims to describe and point to alternative approaches.
Lessness (Oct 08 2022 at 15:50):Committed PRrepresentable.v file to Bullets branch, now waiting for all checks to finish with green status.
Lessness (Oct 08 2022 at 15:55):Success! :tada:
Pierre Castéran (Oct 08 2022 at 16:27):Lessness said:
Success! :tada:
Nice!
I'd a look at the following files in hydra-battles/theories/Ackermann: fol*.v and expressible.v. I'm sure it's worth looking at all the definitions and lemma statements. I put my first examples in a separate subdir: hydra-battles/theories/MoreAck/
In particular, Russel has an interesting way of dealing with dependent type (file extEqualNat.v also used to define primitive recursive functions). Please feel free to ask questions on these topics.
Pierre Castéran (Oct 18 2022 at 13:15):I've removed almost all deprecation warnings from goedel/theories/PRrepresentable.v (in branch FixWarnings)
The exceptions are a few warnings in a big Ltac command: it was hard to do the changes without any immediate feedback.
I noticed a big readability issue in this file, mainly due to a high level of nested sub-proofs, and a lack of readability of the abstract syntax of big LNN formulas.
I see two ways of improving this file:
**or *** Lessness (Oct 19 2022 at 20:21):I can take the 2nd point, definitely. (I mean, rewriting the fol+LNN formulas into the new notation when it's ready.)
And probably the 1st point too.
Lessness (Oct 19 2022 at 20:23):But, in my opinion, the big proof (or maybe there were two of them) must be somehow refactored or smth, i don't know. It's incredibly giant and that's not good...
Pierre Castéran (Oct 20 2022 at 06:36):Lessness said:
I can take the 2nd point, definitely. (I mean, rewriting the fol+LNN formulas into the new notation when it's ready.)
And probably the 1st point too.
Thanks !
I will experiment on a suitable notation scope today. It'll probably be in hydra-battles LNN.v.
I do agree with your opinion on giant proofs. I'd add this is an interesting challenge w.r.t proof maintenance and documentation.
For instance these libraries contains several definitions by interactive proofs, which look OK when refactored, but break the compilation of other modules.
About documentation. Several proof scripts contain assertor replacewhich could be of some interest (w.r.t coding, or expressibility). A brutal docmentation with coqdoc -gwould delete this information. With alectryon, we should be able to comment this step on the documentation.
@Karl Palmskog @Théo Zimmermann Btw, it is possible that we had +/- soon to insert alectryon snippets for the book inside goedel's files. Would that make the compilation and CI of the pdf much more complex?
Karl Palmskog (Oct 20 2022 at 06:44):I don't know how difficult it is to include an external repo as part of the Alectryon build for the Hydras & Co. book. But if it's difficult, we may actually consider migrating the Goedel code into the Hydras & Co. repo, monorepo style. Then we would archive the Goedel repo and point to Hydras & Co. @Théo Zimmermann knows the toolchain better than me, so maybe he has opinions?
Karl Palmskog (Oct 20 2022 at 06:45):(we'd still build the Goedel package separately, though, and the coq-goedel in the opam repo would continue, but point to Hydras & Co. archive/release)
Théo Zimmermann (Oct 20 2022 at 07:23):I agree with @Karl Palmskog that as soon as you are interested in documenting Goedel as well, then adding Goedel to the Hydras & Co monorepo is the most efficient solution (even if there were a way to integrate snippets in other projects it would be a pain eventually).
Pierre Castéran (Oct 20 2022 at 09:20):If it helps, I can create a branch GoedelInc, containing the .v files from Goedel.
For instance, we would have directories like ordinals/Ackermann ordinals/Goedel and ordinals/MoreAck.
Later, it would be time to replace ordinals with a more inclusive denomination ?
Pierre Castéran (Oct 20 2022 at 11:13):@Lessness I experimented a new scope for LNN formulas.
I tried to keep a syntax as close as possible to Coq's syntax.
For instance:
Let f2 : Formula :=
(existH 2 (Zero < var 2 /\ 4 < var 2 + var 2))%NN.
Let f3 := (var 0 = Zero \/ existH 1 (var 0 = Succ (var 1)))%NN.
Let f4 := (var 0 = var 1 + var 1 <-> var 0 = var 1 * 2)%NN.
Note, that in f3, replacing Zerowith 0fails ? (Perhaps a problem with coercions)
(The other choice would be to use different symbols like +NN, \/NN, ... ?)
The experimental branch is LNNScope, the modified files are theories/ordinals/Ackermann/LNN.v and theories/ordinals/MoreAck/LNN_examples.v
Karl Palmskog (Oct 20 2022 at 11:25):@Pierre Castéran
Karl Palmskog (Oct 20 2022 at 11:26):I think we should put Goedel under its own namespace, e.g., goedel, as a sibling directory to ordinals
Karl Palmskog (Oct 20 2022 at 11:27):this makes it easier to package in opam using Dune. And we don't force people to install the whole Goedel proof if they only want the library on ordinals and primitive recursive functions.
Karl Palmskog (Oct 20 2022 at 11:30):if a sibling directory to ordinals is OK, I can create a branch with the Goedel content this weekend (I'm at a conference now). But I think I need Théo's help with the Nix CI side.
Pierre Castéran (Oct 20 2022 at 16:25):So, we will have three main directories under theories/ : ordinals, goedel and additions.
OK !
Théo Zimmermann (Oct 20 2022 at 16:27):We should probably have gaia-hydras at the same level for consistency, shouldn't we?
Pierre Castéran (Oct 20 2022 at 16:33):Théo Zimmermann said:
We should probably have gaia-hydras at the same level for consistency, shouldn't we?
Sure! I forgot it! :worried:
Karl Palmskog (Oct 23 2022 at 10:28):everything works in transfer branch add-goedel now except for some Nix jobs: https://github.com/coq-community/hydra-battles/pull/138
Pierre Castéran (Oct 23 2022 at 15:47):In order to define notation scopes for NN-formulas, I created a branch LNNScope2 of hydra-battles.
The issue with mastercame from redefinitions like:
Definition var := var LNN.
Definition equal := equal LNN.
Definition impH := impH LNN.
Thus , for a given NN-formula, there exists at least two gallina-terms. This made the use of notation scopes hard to use
in printing mode.
The experimental branch LNNScope2 tries to bypass this issue by removing such redefinitions, and uses implicit arguments
a lot. At present, it works with all the Ackermann sub-directory (but it's improvable).
For instance, the old sysntax:
forall n : nat,
SysPrf NN
(impH (orH (LT (var 1) (natToTerm n)) (equal (var 1) (natToTerm n)))
(LT (var 1) (Succ (natToTerm n)))).
Becomes
forall n : nat,
SysPrf NN (var 1 < k_ n \/ var 1 = k_ n -> var 1 < Succ (k_ n))%NN.
Note that this version is highly unstable. We still have to check whether it really increases formulas readibility (in scripts as well as ouputs of Compute) and behaves well with the ex goedel/theories/ files.
Pierre Castéran (Nov 04 2022 at 09:25):I believe that hydra-battles are a metaphor of fixing all 8.16 deprecate warnings in the hydra-battles project.
The hardest part was to fix warnings which suggest composed actions or replacing applys with rewrites. In order not to break Russel's long proofs, I used (provisionally?) a compatibility module.
Now, the task is to make goedel and Ackermann libraries more readable and documented.
Hercules (a.k.a. Pierre)
Lessness (Nov 15 2022 at 20:15):I'm disappearing until second half of the January (when exams will be successfully done), most probably. :|
Having some problems in studies for now.
Pierre Castéran (Nov 15 2022 at 20:30):I wish you will fully succeed!
Thank you for your interest in the project and your encouragement!
Lessness (Dec 14 2022 at 01:46):Thank you for your good wishes! :) But I will reappear here much sooner - I am pausing my studies (dropping out for now) as I have financial problems (need to help family, basically). Don't know yet how active I will be here, but it (re)starts today. :)
Cheers!
Pierre Castéran (Feb 07 2023 at 12:36):I've just completed a first step of transformations on ordinals/Ackermann/and goedelsub-libraries (40 Kloc).
mainly, writing bullets up to ***level, and making intros patterns explicit. I hope that making the script structure more explicit will make easier the code's maintenance and the tasks to come.
Last updated: Jun 11 2023 at 01:30 UTC