Stream: Coq devs & plugin devs

Topic: Scheme Equality


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jan 23 2022 at 09:55):

there's https://hal.inria.fr/hal-01897468v2

view this post on Zulip Hugo Herbelin (Jan 23 2022 at 12:17):

Gaëtan Gilbert said:

there's https://hal.inria.fr/hal-01897468v2

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.)

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jan 23 2022 at 16:53):

We also hope to cover sigma typrs with an irrelevant component.

view this post on Zulip Ali Caglayan (Jan 23 2022 at 20:06):

Would it make sense to turn all scheme commands into plugins?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Jan 23 2022 at 20:08):

That way plugins like equations can automatically call Derive by using the hook

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 07:39):

+1 on moving this to elpi, also to make them more maintainable

view this post on Zulip Karl Palmskog (Jan 24 2022 at 10:21):

you have three options then, in my view:

  1. migrate Coq-Elpi to Coq's repo alongside Ltac2, or
  2. put all Scheme stuff into its own repo that depends on both Coq-Elpi and Coq (akin to Bignums, I guess)
  3. put all Scheme stuff in Coq-elpi's repo

All options likely lead to dependency management work...

view this post on Zulip 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}

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 10:23):

I personally advocate for merging the parametricity plugin into Coq and use that everywhere

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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”)

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Enrico Tassi (Jan 24 2022 at 11:27):

I know, and I'm very happy it is ;-)

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:28):

but then tying it to the kernel OCaml AST is a strong static guarantee

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jan 24 2022 at 11:28):

Oh, you mean, is it fully deterministic by comparison with... what? Scheme Eq?

view this post on Zulip Enrico Tassi (Jan 24 2022 at 11:29):

Hum, but that is what CI is for, no? It has a test suite IIRC

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:29):

by comparison with any horrible Proper typeclass search, say

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:30):

I’m also confused, is the point that logic programming is overkill for a syntactic translation?

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:30):

yes

view this post on Zulip Enrico Tassi (Jan 24 2022 at 11:30):

ah ah, define logic programming then ;-)

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:30):

I don't want to rant against LP here anyways

view this post on Zulip Enrico Tassi (Jan 24 2022 at 11:30):

I agree backing serves no purpose

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:31):

serious as in, we the coq devs are commited to maintain it

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:31):

impedance for who?

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:32):

the coq devs

view this post on Zulip 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"

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:32):

Counterpoint: there are few Coq devs, so they should focus on making themselves unnecessary.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:33):

typically, universes

view this post on Zulip Enrico Tassi (Jan 24 2022 at 11:33):

I consider that a feature ;-)

view this post on Zulip Enrico Tassi (Jan 24 2022 at 11:33):

Nobody wants to see how universes are implemented in Coq

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:33):

indeed

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jan 24 2022 at 11:33):

And you know it better than me

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:34):

otherwise you'll see spurious universe constraints pop up

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:34):

and in the long run, the Metacoq-vs-Iris catastrophe is in the tubes

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:35):

for incomplete / heuristical program interpretations I am less concerned

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:35):

I got the metacoq reference but that’s another thread :-)

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 11:36):

that’s what I like about the ideas in Lean 4, and about elpi

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:36):

I do feel pain for our poor users

view this post on Zulip Enrico Tassi (Jan 24 2022 at 11:37):

Indeed, this is why I'm saying that there not just one parametricity translation...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:38):

@Paolo Giarrusso I don't disagree with you on a high-level point

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:39):

my claim was about serious syntactic intepretations

view this post on Zulip Pierre-Marie Pédrot (Jan 24 2022 at 11:39):

anyways

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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: Feb 05 2023 at 21:03 UTC