I'm interested in revising and extending the "Logic" library of the Coq archive. Would someone be interested in such plan? A first objective would be to provide a library of quotients.
Is this about the Logic sublibrary in the stdlib? If so, I would be happy to help (but I am not a logician). Can I point to this thread about the desire of a push_neg tactic for Coq ?
Also a good first step would be to take inventory and document the existing stuff. I can try to help with this.
About inventory, note this part of the roadmap: https://github.com/coq/ceps/blob/coq-roadmap/text/069-coq-roadmap.md#libraries-and-community (currently in section "Other axes, without sufficient resources" due to a lack of volunteers)
First impression: the stdlib doc is not easy to figure out. The user has to guess if a file will be useful with only its name and there are many files. Is it possible to add more structure to this?
Yes, that's the kind of things that would be useful (c.f., "Identify consistent stdlib components" in the roadmap).
Is this about the Logic sublibrary in the stdlib?
Yes, this is what I meant.
Indeed, why not to put a push_neg
tactic in this library (there is for instance already a tactic related to functional extensionality).
The Logic library currently has typically two roles:
to declare extra axioms (EM, FunExt, PropExt, PI, AC/ε/ɩ, JMeq, ...) (see this picture
about how they relate)
to collect basic consequences of such axioms (and sometimes tactics)
A related question is: would it make sense to connect (or at least synchronize) with libraries about logic (e.g. the Coq Library for Mechanised First-Order Logic and its evolution to a library of constructive reverse mathematics).
Is it possible to add more structure to this?
Certainly and it is somehow a general problem of libraries it seems: we may add systematically a README, or a TOC, or an index.html that guide through the libraries.
@Hugo Herbelin the FOL library now lives here, but it's licensed under a strong copyleft license (CECILL-2.1), so it can't be integrated or used by Coq without changing Coq's license to a strong copyleft license like GPL (which in my view would be infeasible).
cc: @Dominik Kirst @Yannick Forster
Hugo Herbelin said:
Is it possible to add more structure to this?
Certainly and it is somehow a general problem of libraries it seems: we may add systematically a README, or a TOC, or an index.html that guide through the libraries.
All right, let's do this! Also your axioms diagram should be there too.
Karl Palmskog said:
Hugo Herbelin the FOL library now lives here, but it's licensed under a strong copyleft license (CECILL-2.1), so it can't be integrated or used by Coq without changing Coq's license to a strong copyleft license like GPL (which in my view would be infeasible).
cc: Dominik Kirst Yannick Forster
There's more or less no reason whatsoever that the undecidability library and the first-order library are CECILL, we'd be happy to relicense to whatever is easier (MIT?)
A brief answer about the structure:
Files extending Coq with axioms:
Short libraries about logical concepts:
Specific theorems or constructions:
Consequences of axioms:
Don't know if still useful:
Hugo Herbelin said:
A related question is: would it make sense to connect (or at least synchronize) with libraries about logic (e.g. the Coq Library for Mechanised First-Order Logic and its evolution to a library of constructive reverse mathematics).
I think it's premature to think about it, we need to take inventory first.
@Yannick Forster if you want to maximize reusability, we recommend MIT, yes, see our general licensing advice here: https://github.com/coq-community/manifesto/#best-practices
I'd be happy to see more sub-classical principles in the stdlib (MP, LPO, etc). Adding to the library chaos, there is also github.com/uds-psl/coq-synthetic-computability/ which is connected to the undecidability library, formally not yet connected to the FOL library. But it's where most of the stuff about sub-classical principles lives currently
This library is also already MIT :)
there has been some FOL-related work in the Hydras & Co. project. Maybe @Pierre Castéran has some suggestions of purely logic related concepts that would fit into Stdlib
I'd be happy to see more sub-classical principles in the stdlib (MP, LPO, etc)
Yes, typically.
Karl Palmskog said:
there has been some FOL-related work in the Hydras & Co. project. Maybe Pierre Castéran has some suggestions of purely logic related concepts that would fit into Stdlib
To be precise, I'm working on the maintenance, modernization and documentation of Russel O'Connor's proof of Gödel's first incompleteness theorem. This proof uses an ad-hoc (e.g. non-HOAS) formalization of FOL and PA.
Adapting this long (almost 40 KLOC) developpement to a more standard library would be an interesr-ting but huge work.
right, I guess I was thinking of if there was an "official" FOL deep embedding and semantics in Stdlib, then one could prove Russell's encoding equivalent in some way, as validation
I'd be interested to help, but I only have time sporadically.
W.r.t. quotients: in coq-zorns-lemma there is a file Quotients which might serve as a starting point. IMO it is a bit clunky to use. Using RelationClasses
and Morphisms
from the stdlib might be better.
I think it'd be nice if we could distinguish between Choice for different cardinalities. For some results in coq-topology only countable choice is necessary, but there is no standard way to represent this.
Ok, Karl's remark is consistent with what we did in Hydra-Battles with such concepts as ordinals, countability, etc.
For instance, our data structures for ordinals are formally related with Schütte's book, and José Grimm's Gaia.
With respect to FOL, the proof scripts are strongly related to ad-hoc data structures, but we have to show that Russel's definition of e.g. "provable in PA" is equivalent to the "standard" one.
Re Quotients:
So, IIUC, ZornsLemma works with the type of equivalence classes up to propositional extensionality. This seems similar to an implementation posted once by Arturo A. de A. on coq-club (see his blog).
Maybe, Arthur C. has one too in TLC (using indefinite description?).
There is a possible axiomatization as higher inductive type, and then, possibly implementable using private inductive types.
Mikkelsen-Paré theorem builds coequalizers from subsets in elemetary topos, so I believe it should apply to Coq. Maybe is this the same construction as in ZornsLemma and by Arturo.
Last updated: Oct 13 2024 at 01:02 UTC