What would be the best way of finding/tracking/documenting math+CS concepts that have (already) been formalized in Coq? We see already that finite sets seemingly have 10+ Coq encodings, but non-famous concepts/theorems are harder to track down. The problem with people claiming that they are the first to formalize something when there's a 10-20 year old Coq formalization somewhere will only get worse over time.

Example: https://ieeexplore.ieee.org/document/8997376 -- "It is the first Coq formalization about transfinite induction to our knowledge." Yet Simpson did transfinite ordinals/induction 15+ years ago and it lives on as a coq-contrib: https://github.com/coq-contribs/cats-in-zfc

I can imagine using the Coq wiki (quite chaotic with open edits) or a dedicated curated GitHub repo in coq-community. If nothing else, it's useful in the ongoing comparisons with other systems, e.g., https://xenaproject.wordpress.com/what-maths-is-in-lean/

Yes, it would be good to compare across systems. This is a typical MKM topic.

The dedukti people wanted to do something like that, I believe called "logopedia", but google is not very helpful.

It's logipedia: http://logipedia.inria.fr/

I'm a bit familiar with Logipedia, but as far as I understand it will only support concepts/results that are portable via Dedukti --- I have a hard time seeing them include MathComp-related results, for example. Also, to even end up in Dedukti someone needs to have discovered the formalization/paper.

if one wants to do MKM, it would likely start by trawling papers in database like DBLP and looking for the "Coq" keyword, then trying to figure out (say, by NLP) whether the paper actually claims to have formalized something in Coq, extracting what concept was formalized, then figuring out if the formalization is actually available online. Finally, I think there needs to be human checking at some point (otherwise random paper can get away with getting counted as having formally proven famous theorem, without having actually done it).

I wasn't suggesting to depend on dedukti, just suggesting that they have some of the same goals.

Is there somewhere I can find a list of axioms that are known to be incompatible with each other and with Coq theory?

The best resource is likely the wiki: https://github.com/coq/coq/wiki/CoqAndAxioms --- there are also topics on this in the Coq Discourse

specifically, the wiki doesn't cover the univalence axiom and its incompatibility with Streicher's K, but there is a bunch of stuff on that in the Discourse, e.g., https://coq.discourse.group/t/what-do-you-think-of-axioms/231

@Théo Zimmermann btw, would you say collaboratively tracking/listing Coq formalizations is something that falls (clearly or barely?) in the scope of coq-community?

Yeah, I would say so, much like the awesome stuff.

Awesome, this is what I was looking for thanks! Let us know if you open a new project to list this.

Also would you have a reference on how to approach proving compatibility of an axiom?

Pedro Abreu said:

Also would you have a reference on how to approach proving compatibility of an axiom?

you build a model validating the axioms you have in mind ?

I guess MetaCoq could be used for reasoning in Coq about variants of CiC that include different axioms, e.g., showing that there is a model as Kenji suggests. I don't know if they have the machinery for showing that there is *no* model, as for Univalence+K, though.

showing that univalence + K is incompatible is rather easy: assuming both you can prove false in Coq (univalence implies that equality on bool has 2 elements whereas with K it has exactly one), so any model of CIC + univalence + K has a close inhabitant of (the interpretation of) False

@Pedro Abreu so here is how I see listing Coq formalizations --- if somebody did indeed prove **in Coq** that there is a model, for example, of CIC+LEM (not that hard, I think), then it could be listed, but I don't plan for such a list to be collection of metatheoretic results about the Calculus of Constructions, since very few have been formalized in Coq (Barras/Werner work on Coq-in-Coq comes to mind besides MetaCoq).

@Kenji Maillard but to show it "properly", shouldn't one actually prove it at some meta level, e.g., in Coq when reasoning about an encoded Coq system? That should take a bit more work.

Formalizing that argument would definitely be tedious and I don't expect that you would learn much from the process... (not that I would complain if someone decides to do it)

hmm, so I'm thinking the Coq formalization list could be thought of as a bipartite graph, with "concepts" in the first set, and "Coq projects" in the other

@Bas Spitters I think one would want some MKM expert advice here -- can you think of someone we could reach out to? The basic goal would just be to crowdsource the Coq equivalent of Buzzard's Lean math list, if nothing else for future funding reasons... I've dug around in all those "concept alignment" papers, but they didn't seem to amount to much in practice.

Good question, I'd contact Claudio Sacerdoti Coen, Cezary Kalizyk or Michael Kohlhase, I believe.

There have been many projects that have tried to solve "similar" issues, but I'm not sure if anyone has tried something close enough.

https://cicm-conference.org/2020/cicm.php

I have cited more CICM papers than I can count, but they have a clear preference for super-heavyweight and specialized solutions, I just want something very lightweight, an inch above a wiki. Claudio may be the most tuned into the Coq community then.

@Karl Palmskog on axiom incompatibility, why would you want more than an internal proof of False? I agree that a Coq soundness proof should let you do that, but that's just a question on the proof method one uses for soundness (and I can't imagine one that fails)

@Paolo G. Giarrusso simply collecting top-level proofs of False seems like a bad way to organize a library that documents axiom compatibility. For one thing, the system in which the contradiction is derived will be different every time Coq's foundations are altered. Better to show the contradiction for a minimal deeply embedded system, and let MetaCoq maintainers provide a proof that the "current" Coq is a supersystem of the minimal system.

Last updated: Jun 20 2024 at 11:02 UTC