Regularity & Epsilon induction.

[georgydunaev]

Here I proved the epsilon induction.
Then I verified the proofs of the regularity axiom based on epsilon induction.
Both intuitionistic and classic formulation are available.

[herbelin]

Thanks for this proposition. I'm not the author of the development (it is Benjamin Werner), but I shall assume that he is ok to extend it with your useful and interesting proof. Please see comments. Please also use a name like Regularity.v for the file, rather than 3_Regularity.v.

[herbelin]

This .gitignore is a bit overkill for zfc (no need for the .cache, or the .cm* for instance) but it does not matter.

[herbelin]

Letter P is not very discriminating. Wouldn't you have an alternative name? Maybe something like regular_over, since this is a strengthening of regular as far as I understood.

[herbelin]

I've seen "soundness" abbreviated more often "sound". So, please give preference to "regular_over_sound" or "regular_over_soundness" or something like that.

[herbelin]

Idem, I would rather see a full name like Regularity (compare for instance to how theorems are named in the other file Replacement.v).

[herbelin]

You can remove these useless lines.

[herbelin]

Hi @georgydunaev, are you still working on your project of formalizing Jech's book? (And sorry for not having answered earlier to the three issues #2, #3, #4 you raised.)

[georgydunaev]

Hi @georgydunaev, are you still working on your project of formalizing Jech's book? (And sorry for not having answered earlier to the three issues #2, #3, #4 you raised.)

Hello, mr. Herbelin.

I've proved axioms of ZFC (for Ens) from Jech's book in January and then temporarily stopped this kind of activity. (https://github.com/georgydunaev/Jech/blob/master/Jech.v This code is of lower quality, I should remaster it.)

What are criteria the code shall meet to be placed in coq-contribs or coq-community?
( I have completed(and this code is of much higher quality) formalization of the

1. predicate calculus' soundness(with contexts) and
   Predicate Calculus: https://github.com/georgydunaev/VerifiedMathFoundations/blob/development/OneFile.v
2. the propositional calculus' completeness(with contexts).
   Propositional Calculus: https://github.com/georgydunaev/VerifiedMathFoundations/blob/development/PropLang.v )

[herbelin]

Thanks for your reply.

What are criteria the code shall meet to be placed in coq-contribs or coq-community?

I don't think that formal criteria have clearly been written but this is in progress (if something has been done, @Zimmi48 should know). The typical criteria are: a minimum of coqdoc-style documentation explaining what is done and the roles of the main lemmas, no admit/Admitted (if something is open, use a Conjecture, or a documented Axiom), no remaining "TODO" or "FIXME" of internal usage, an attached README/description file, ...

PropLang would need a little cleaning and a bit of documentation but looks good otherwise. There are already various formalizations of propositional calculus but your formalization is attached to a precise textbook and is thus valuable as an effective formalization of this precise book. Similarly for OneFile. I could not understand if it follows a textbook, but if it does, it is valuable as an effective formalization of this precise book.

Let's first wait for @Zimmi48's position.

[Zimmi48]

What are criteria the code shall meet to be placed in coq-contribs or coq-community?

I'm not sure exactly what you have in mind but coq-community welcomes old projects from coq-contribs when they find a new maintainer, and large refactorings / changes to update / extend such projects are welcome within coq-community.

On the other hand, there has not been any new project integrated in coq-contribs since the rise of opam as a package manager for Coq, which is how people distribute their Coq projects nowadays.

I don't think that formal criteria have clearly been written but this is in progress

I am not aware of any progress being made in this direction. I'm not exactly sure what @herbelin meant by this. All I can say is that in coq-community, there is no minimum quality criterion for transferring a project. There are only criteria of interests and presence of a volunteer maintainer. I'll refer you to the manifesto for more details: https://github.com/coq-community/manifesto

[herbelin]

I don't think that formal criteria have clearly been written but this is in progress

I am not aware of any progress being made in this direction. I'm not exactly sure what @herbelin meant by this.

I was more or less thinking to the formation of an editorial board mentioned in paragraph advertising-interesting-packages of the manifesto, who implicitly would have established some criteria about which packages are worth to be advertized.

In any case, @georgydunaev, the answer seems then to be that you can freely publish to coq-community. And if you estimate that you will not be able to maintain it, I can put it in coq-contribs (which I maintain roughly once or twice a year), or simply opam, with a specific version of Coq to ensure it compiles, and with appropriate keywords for the advertizing, @Zimmi48, is this compatible with your view or do you recommend something else?

More generally, I find the idea to develop a library of formalized mathematical books very exciting, but this is still a long-term project!

[Zimmi48]

I was more or less thinking to the formation of an editorial board mentioned in paragraph advertising-interesting-packages of the manifesto, who implicitly would have established some criteria about which packages are worth to be advertized.

Ah right. When this board is created, then it will set criteria, not for inclusion but for advertisement of packages, indeed.