Stream: Hydras & Co. universe

Topic: Helping with the branch "bullets"


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

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

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

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

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

view this post on Zulip Karl Palmskog (Oct 05 2022 at 15:03):

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)

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

Ah, ok. I used EMacs’ indent-region command too globally…

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

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

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) ?

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

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

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

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

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

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

view this post on Zulip Karl Palmskog (Oct 06 2022 at 14:57):

this is a known problem with the MathComp dev Docker image, see here. I will open a PR to fix this.

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

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

view this post on Zulip Pierre Castéran (Oct 06 2022 at 16:31):

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) ?

view this post on Zulip Karl Palmskog (Oct 06 2022 at 18:38):

OK, I will do separate PR to add the blue hydra-rooster

view this post on Zulip Karl Palmskog (Oct 06 2022 at 20:57):

PR done, I decided to call it "The incomplete rooster hydra"

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

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

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

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

view this post on Zulip Lessness (Oct 08 2022 at 13:46):

Found my mistake, now it's working.

view this post on Zulip Pierre Castéran (Oct 08 2022 at 14:03):

Indeed, this lemma looks nightmarish! Just after a huge Ltac definition !!!

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

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

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

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

view this post on Zulip Lessness (Oct 08 2022 at 15:50):

Committed PRrepresentable.v file to Bullets branch, now waiting for all checks to finish with green status.

view this post on Zulip Lessness (Oct 08 2022 at 15:55):

Success! :tada:

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Karl Palmskog (Oct 20 2022 at 11:25):

@Pierre Castéran

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

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

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

view this post on Zulip Pierre Castéran (Oct 20 2022 at 16:25):

So, we will have three main directories under theories/ : ordinals, goedel and additions.
OK !

view this post on Zulip Théo Zimmermann (Oct 20 2022 at 16:27):

We should probably have gaia-hydras at the same level for consistency, shouldn't we?

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

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

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

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

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

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

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

view this post on Zulip 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 13 2024 at 05:01 UTC