Karl Palmskog (May 15 2020 at 21:05): Karl Palmskog (May 15 2020 at 21:05):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.
Karl Palmskog (May 15 2020 at 21:09):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
Karl Palmskog (May 15 2020 at 21:13):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/
Bas Spitters (May 16 2020 at 08:47):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.
Théo Winterhalter (May 16 2020 at 08:49):It's logipedia: http://logipedia.inria.fr/
Karl Palmskog (May 16 2020 at 11:37):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.
Karl Palmskog (May 16 2020 at 11:48):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).
Bas Spitters (May 16 2020 at 12:02):I wasn't suggesting to depend on dedukti, just suggesting that they have some of the same goals.
Pedro Abreu (May 18 2020 at 15:52):Is there somewhere I can find a list of axioms that are known to be incompatible with each other and with Coq theory?
Karl Palmskog (May 18 2020 at 15:55):The best resource is likely the wiki: https://github.com/coq/coq/wiki/CoqAndAxioms --- there are also topics on this in the Coq Discourse
Karl Palmskog (May 18 2020 at 15:59):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
Karl Palmskog (May 18 2020 at 16:01):@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?
Théo Zimmermann (May 18 2020 at 16:02):Yeah, I would say so, much like the awesome stuff.
Pedro Abreu (May 18 2020 at 16:30):Awesome, this is what I was looking for thanks! Let us know if you open a new project to list this.
Pedro Abreu (May 18 2020 at 16:30):Also would you have a reference on how to approach proving compatibility of an axiom?
Kenji Maillard (May 18 2020 at 16:37):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 ?
Karl Palmskog (May 18 2020 at 16:46):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.
Kenji Maillard (May 18 2020 at 16:50):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
Karl Palmskog (May 18 2020 at 16:50):@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).
Karl Palmskog (May 18 2020 at 16:52):@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.
Kenji Maillard (May 18 2020 at 16:57):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)
Karl Palmskog (May 18 2020 at 18:25):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
Karl Palmskog (May 18 2020 at 18:31):@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.
Bas Spitters (May 18 2020 at 19:58):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
Karl Palmskog (May 18 2020 at 19:59):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.
Paolo Giarrusso (May 20 2020 at 21:20):@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)
Karl Palmskog (May 21 2020 at 11:04):@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: Apr 18 2024 at 23:01 UTC