Hugo Herbelin (Jan 23 2022 at 09:27): Hugo Herbelin (Jan 23 2022 at 09:27):Hi, I wonder what literature exists about the underlying metatheory for the automatic generation of Boolean equality for decidable inductive types. In particular, I realized recently that the syntactic translations developed in Nantes (parametricity, forcing, etc.) can be modified relatively easily to produce a Boolean equality working for the whole Calculus of Inductive Constructions and I wondered what is already known about the subject?
Gaëtan Gilbert (Jan 23 2022 at 09:55):there's https://hal.inria.fr/hal-01897468v2
Hugo Herbelin (Jan 23 2022 at 12:17):Gaëtan Gilbert said:
This looks very impressive! So many lemmas automatically generated, that was one of my dream! What is the exact status? What is the exact extent? From a naive perspective, it seems worth to be compared/merged/unified with what Scheme is (modestly) doing and what Derive does in Equations. I'm sure everyone would benefit _a lot_ from a unified, centrally documented system of automatic generation of schemes.
(On my side, I studied Boolean equality and I will make a draft PR making their generation by Scheme Equality a bit more robust and general but this might well be actually subsumed by what elpi already does.)
Enrico Tassi (Jan 23 2022 at 16:52):Together with others in Sophia we are improving it, in particular to generate smaller proof terms. Hopefully this will also impact inversion.
Enrico Tassi (Jan 23 2022 at 16:53):We also hope to cover sigma typrs with an irrelevant component.
Ali Caglayan (Jan 23 2022 at 20:06):Would it make sense to turn all scheme commands into plugins?
Ali Caglayan (Jan 23 2022 at 20:07):The only issue I can foresee is the calling of the induction schemes after a definition etc.
Ali Caglayan (Jan 23 2022 at 20:07):But we should be able to make a general hook for plugins to run vernac after these commands?
Ali Caglayan (Jan 23 2022 at 20:08):That way plugins like equations can automatically call Derive by using the hook
Ali Caglayan (Jan 23 2022 at 20:08):and our scheme plugin could be something more modular that can easily be replaced by better versions in the future
Paolo Giarrusso (Jan 24 2022 at 07:39):+1 on moving this to elpi, also to make them more maintainable
Karl Palmskog (Jan 24 2022 at 10:21):you have three options then, in my view:
All options likely lead to dependency management work...
Karl Palmskog (Jan 24 2022 at 10:22):the following are Elpi's current dependencies, which I think are not trivial...
"ocaml" {>= "4.04.0"}
"camlp5" {< "7.99"}
"ppxlib" {>= "0.12.0"}
"re" {>= "1.7.2"}
"ppx_deriving" {>= "4.2"}
"ANSITerminal" {with-test}
"cmdliner" {with-test}
"dune" {>= "2.2.0"}
"conf-time" {with-test}
I personally advocate for merging the parametricity plugin into Coq and use that everywhere
Pierre-Marie Pédrot (Jan 24 2022 at 10:24):IMO it's better to do stuff in OCaml for this kind of low-level manipulation (this is not a heuristic tactic, this is a syntactic translation)
Paolo Giarrusso (Jan 24 2022 at 11:16):It seems to me that unless you're a Coq dev, there's a bigger barrier to entry to OCaml than to higher-level languages. I don't think anything in elpi restricts it necessarily to heuristic tactics.
Enrico Tassi (Jan 24 2022 at 11:19):At the moment, I don't see much advantage in merging coq-elpi, the deps are huge and it is still "incomplete" (does not cover full CIC)
Enrico Tassi (Jan 24 2022 at 11:20):Derivations in Elpi, are, so far "ltac free". In some cases we are experimenting with calling tactics, but that is mostly to speed up experimentation.
Paolo Giarrusso (Jan 24 2022 at 11:22):even if elpi is not done yet, I stand by the long-term vision (I “grew up” with Guy Steele’s “Growing a Language”)
Pierre-Marie Pédrot (Jan 24 2022 at 11:27):@Enrico Tassi my point was not about Ltac, rather that the parametricity interpretation is a fully deterministic, total process
Enrico Tassi (Jan 24 2022 at 11:27):About hooks, I tend to agree with that. In Elpi I have quite some code so that I can "parse" stuff like derive Inductive F params := K1 .. and completely take over the declaration, eg open a module F and place in there all the derived stuff. If that was a sort of protocol and one could just set a hook to be called once the inductive is declared, and before the module is closed...
Enrico Tassi (Jan 24 2022 at 11:27):I know, and I'm very happy it is ;-)
Pierre-Marie Pédrot (Jan 24 2022 at 11:28):but then tying it to the kernel OCaml AST is a strong static guarantee
Pierre-Marie Pédrot (Jan 24 2022 at 11:28):whenever somebody adds a constructor or plays dirty tricks with universe instances you'll see it
Enrico Tassi (Jan 24 2022 at 11:28):Oh, you mean, is it fully deterministic by comparison with... what? Scheme Eq?
Enrico Tassi (Jan 24 2022 at 11:29):Hum, but that is what CI is for, no? It has a test suite IIRC
Pierre-Marie Pédrot (Jan 24 2022 at 11:29):by comparison with any horrible Proper typeclass search, say
Paolo Giarrusso (Jan 24 2022 at 11:30):I’m also confused, is the point that logic programming is overkill for a syntactic translation?
Pierre-Marie Pédrot (Jan 24 2022 at 11:30):yes
Enrico Tassi (Jan 24 2022 at 11:30):ah ah, define logic programming then ;-)
Pierre-Marie Pédrot (Jan 24 2022 at 11:30):I don't want to rant against LP here anyways
Enrico Tassi (Jan 24 2022 at 11:30):I agree backing serves no purpose
Pierre-Marie Pédrot (Jan 24 2022 at 11:31):I'd just like to advocate that serious syntactic intepretations should have the lowest impedance
Pierre-Marie Pédrot (Jan 24 2022 at 11:31):serious as in, we the coq devs are commited to maintain it
Paolo Giarrusso (Jan 24 2022 at 11:31):impedance for who?
Pierre-Marie Pédrot (Jan 24 2022 at 11:31):and low impedance means the least amount of abstractions w.r.t. the kernel AST
Pierre-Marie Pédrot (Jan 24 2022 at 11:32):the coq devs
Enrico Tassi (Jan 24 2022 at 11:32):Ok, if it is about speed and maintenance, I agree with that. But for example, there is not just "one parametricity translation"
Paolo Giarrusso (Jan 24 2022 at 11:32):Counterpoint: there are few Coq devs, so they should focus on making themselves unnecessary.
Pierre-Marie Pédrot (Jan 24 2022 at 11:32):it's not so much speed, rather I am concerned about abstraction layers getting in the way of nasty low-level details
Pierre-Marie Pédrot (Jan 24 2022 at 11:33):typically, universes
Enrico Tassi (Jan 24 2022 at 11:33):I consider that a feature ;-)
Enrico Tassi (Jan 24 2022 at 11:33):Nobody wants to see how universes are implemented in Coq
Pierre-Marie Pédrot (Jan 24 2022 at 11:33):indeed
Pierre-Marie Pédrot (Jan 24 2022 at 11:33):so it's the burden of the kernel maintainers to design a translation that behaves correctly wrt universes
Enrico Tassi (Jan 24 2022 at 11:33):And you know it better than me
Pierre-Marie Pédrot (Jan 24 2022 at 11:34):otherwise you'll see spurious universe constraints pop up
Pierre-Marie Pédrot (Jan 24 2022 at 11:34):and in the long run, the Metacoq-vs-Iris catastrophe is in the tubes
Pierre-Marie Pédrot (Jan 24 2022 at 11:35):for incomplete / heuristical program interpretations I am less concerned
Enrico Tassi (Jan 24 2022 at 11:35):I see what you mean now about universes, and I've little experience with explicit universe binders (since I don't have them yet, but maybe they will be soon, since Enzo is helping).
Paolo Giarrusso (Jan 24 2022 at 11:35):I got the metacoq reference but that’s another thread :-)
Paolo Giarrusso (Jan 24 2022 at 11:36):as a user, it’s a disgrace that derive equality is a hardcoded inflexible builtin and nobody has yet patched it to produce boolean equality. Using a good higher-level language would make it easier for people to maintain/extend/customize it.
Paolo Giarrusso (Jan 24 2022 at 11:36):that’s what I like about the ideas in Lean 4, and about elpi
Pierre-Marie Pédrot (Jan 24 2022 at 11:36):I do feel pain for our poor users
Enrico Tassi (Jan 24 2022 at 11:37):Indeed, this is why I'm saying that there not just one parametricity translation...
Pierre-Marie Pédrot (Jan 24 2022 at 11:37):but that one is not total, because users can tweak stuff, so yeah I agree with you
Paolo Giarrusso (Jan 24 2022 at 11:38):I’m not married with logic programming, but it’s clearly a sensible DSL for an elaborator that does backtracking, and I’d rather have 1 DSL (which can do backtracking and LP) than 2.
Pierre-Marie Pédrot (Jan 24 2022 at 11:38):we've been stuck for 20 years with broken induction principles for nested inductive types...
Paolo Giarrusso (Jan 24 2022 at 11:38):and even if you fixed those, that wouldn’t help users that need their own variations anyway
Pierre-Marie Pédrot (Jan 24 2022 at 11:38):@Paolo Giarrusso I don't disagree with you on a high-level point
Pierre-Marie Pédrot (Jan 24 2022 at 11:39):my claim was about serious syntactic intepretations
Pierre-Marie Pédrot (Jan 24 2022 at 11:39):anyways
Pierre-Marie Pédrot (Jan 24 2022 at 11:39):please continue developing it in elpi, that's solving a lot of pain points indeed
Paolo Giarrusso (Jan 24 2022 at 11:43):for everybody confused about metacoq-vs-iris see https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Universe.20incompatibility.20from.20MetaCoq.20and.20Iris
Hugo Herbelin (Jan 24 2022 at 13:30):The discussion goes in several directions and we'll certainly need to have a technical discussion at some time (for instance on the exact choice of parametricity translation used and on the exact coverage of each algorithm) but when I realized the amount of features already implemented in Elpi (and secondarily of Equations), my point became more about how to propose a unified front-end over which we can continue to let things grow in coverage of the CIC and in diversity of translations, integrating contributions from various origins.
I will hereafter rely on the Scheme syntax but it can be any other syntax. The question is: can we imagine a system of registration of translations by plugins which provides flags of the form Set Foo Scheme to automatically generate a scheme for each new definition as well as commands of the form Scheme id := Foo for bar, where each new kind of scheme Foo possibly comes with flavors (e.g. for Boolean equality which I studied, it can be of the forall A B eq_A eq_B, ... or forall A eq_A B eq_B forms, or it can assume proof irrelevance and drop arguments in Prop, or it can support the full cumulative hierarchy of universes or not, etc.)?
As discussed above, delegating the actual implementation to plugins would allow more flexibility in the implementation language they use, and at the same time provides a more distributed responsibility in maintaining the code, while still retaining a unified view and still retaining the possibility to eventually propose new algorithms or better implementations of existing algorithms.
Pierre-Marie Pédrot (Jan 24 2022 at 13:33):one of the problem I see extending the current approach is that we can hit diamond dependencies with scheme registration quite easily
Pierre-Marie Pédrot (Jan 24 2022 at 13:34):so you'd need to ensure that the plugins used to generate one part must coincide globally or something
Hugo Herbelin (Jan 24 2022 at 16:22):You mean dependency e.g. of eq_dec into beq? I was thinking having several variants for a same scheme. For instance, there are already several possible variants for _beq schemes. So, yes, this comes with a problem of naming univoquely a scheme in all its small details.
Hugo Herbelin (Jan 25 2022 at 09:38):To come back on the variant of parametricity that produces Boolean equality, is it documented somewhere? Is it supposed to be folklore? @Enrico Tassi, your paper and the Elpi implementation seem to build Boolean equality independently of the generic parametricity translation, but at the same time there seems to be an implicit statement in the air from the paper, and also from @Pierre-Marie Pédrot that even Boolean equality is a particular case of parametricity (which is the conclusion I also arrived to). If this is not already documented somewhere, this is certainly worth making this more well-known.
Enrico Tassi (Jan 25 2022 at 10:41):I use unary parametricity in order to get deep induction principles which in turn are necessary to prove the correctness of equality tests compositionally and keep their proofs opaque.
Jason Gross (Jan 27 2022 at 16:48):Somewhat related question from reading the paper: are "no confusion" principles the same as inversion principles / type-specific path-induction principles? (It seems like decidable equality is the fixpoint of applying the inversion principle recursively?)
Paolo Giarrusso (Jan 27 2022 at 16:54):(At least in Agda papers), "no confusion" are more specific: they asserts that different constructors have disjoint ranges. "Inversion" should also include that each constructor is an injective function.
Paolo Giarrusso (Jan 27 2022 at 16:58):Sorry I misremembered, you're right; https://dl.acm.org/doi/pdf/10.1145/2628136.2628139 has this, which covers both disjointedness and injectivity
image.png
Last updated: Sep 25 2023 at 14:01 UTC