Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Induction principle for nested inductive types

Qinshi Wang (Feb 15 2022 at 15:36):

Can I add a topic "Nested inductive scheme"? It should be a plugin rather than Coq itself. MetaCoq already has such a generator. But I talked with them and find the generator is not updated to the latest Coq.

Ali Caglayan (Feb 15 2022 at 15:42):

@Qinshi Wang Absolutely, we can discuss it in one of the hacking sessions (morning/evening CET) if you like

Kenji Maillard (Feb 15 2022 at 15:47):

@Qinshi Wang On the topic of nested inductive scheme, you might want to have a look at what's been done relatively recently in Coq-elpi (see this paper)

Qinshi Wang (Feb 15 2022 at 15:53):

We want to automatically generate induction schemes for data types with nested inductive types, e.g.
Inductive tree A :=
| leaf : A -> tree A
| node : A -> list (tree A) -> tree A.
We are writing some large induction schemes in our project and so does @TJ Barclay 's group. It seems the MetaCoq template https://github.com/MetaCoq/metacoq/tree/master/template-coq handles it. But while MetaCoq is updated to the latest Coq version, this functionality is not updated.

Qinshi Wang (Feb 15 2022 at 15:55):

@Kenji Maillard Thanks. Yes, I know it.

Yannick Forster (Feb 15 2022 at 16:08):

Are you interested in updating the MetaCoq plugin to more recent MetaCoq versions? :)

Qinshi Wang (Feb 15 2022 at 16:11):

@Yannick Forster Sure. Hopefully I can get some help about MetaCoq.

Yannick Forster (Feb 15 2022 at 16:13):

I will gladly help :) @Matthieu Sozeau (for general MetaCoq things) and @Marcel Ullrich (for the plugin) are usually also very eager yo help

Qinshi Wang (Feb 15 2022 at 16:29):

@Yannick Forster As I said in the email, I can compile MetaCoq on Coq 8.13, but not the induction scheme generator.

Yannick Forster (Feb 15 2022 at 16:30):

Yes, I guess that's because the induction scheme generator was implemented on a different version of MetaCoq branch 8.13

Yannick Forster (Feb 15 2022 at 16:31):

https://github.com/uds-psl/metacoq_plugins

Yannick Forster (Feb 15 2022 at 16:31):

This explains which MetaCoq version is assumed

Yannick Forster (Feb 15 2022 at 16:32):

commit 7281139

Yannick Forster (Feb 15 2022 at 16:32):

which is even a commit on the 8.12 branch it seems

Yannick Forster (Feb 15 2022 at 16:33):

So the natural way to progress would be to install MetaCoq from the tip of the 8.13 branch, compile the plugin there, which will lead to an error message (as you have already noticed :) )

Yannick Forster (Feb 15 2022 at 16:33):

Hopefully the error message is parseable enough s.t. you have an idea where to compare commit 7281139 with the tip of coq-8.13 to see what change is necessary

Enrico Tassi (Feb 15 2022 at 16:34):

@Kenji Maillard Thanks. Yes, I know it.

It is a bit off topic, but @Qinshi Wang are there reasons why you can't use Coq-Elpi? Is there a Coq-Elpi limitation hitting you? Thanks

Qinshi Wang (Feb 15 2022 at 16:37):

As described in the MetaCoq induction paper (https://arxiv.org/abs/2006.15135), it's said Coq-Elpi generates equality function rather than induction scheme. Another problem is not supporting mutually inductive type.

Enrico Tassi (Feb 15 2022 at 16:39):

Coq-Elpi generates the induction scheme as well, since it is needed in order to prove that the equality tests are correct.
It is true that it does not handle mutual inductive types, this is a hard limitation that won't be lifted anytime soon... so MetaCoq seems the right choice right now if you need these.

Yannick Forster (Feb 15 2022 at 16:43):

Sorry if the abstract was unclear :) Indeed Enrico's plugin also generates induction schemes, the same way we do using the MetaCoq implementation. (I don't recall 100%, but maybe we even took the idea from Enrico? That should be traceable from Marcel's Bachelor's thesis)

Qinshi Wang (Feb 15 2022 at 16:44):

We do use mutual inductive types in our development.

Yannick Forster (Feb 15 2022 at 16:45):

I would expect that lifting to mutual inductives would not be very hard, but as always also not trivial

Enrico Tassi (Feb 15 2022 at 16:46):

I think that lifting the algorithm should work. But Coq-Elpi's HOAS of Coq terms does not cover mutual inductive/fixpoints, so you can't really write the extended algorithm in Coq-Elpi :-/

Ali Caglayan (Feb 15 2022 at 16:46):

What's the problem with mutuals?

Qinshi Wang (Feb 15 2022 at 16:48):

Actually what I'm thinking of (which is also how our hand-written inductive schemes look like now) does not include generating a Forall-like relation.

Enrico Tassi (Feb 15 2022 at 16:49):

Nothing special, it is just that I never coded it (it seems that the usefulness/work-needed ratio is not stellar to me, but I may be wrong). @Qinshi Wang can you share some of these types? I always had the impression that many mutual types were written like that because Coq did generate bad induction for the non nested variant (e.g. I've seen the type of lists being made mutual for that reason many times).

Ali Caglayan (Feb 15 2022 at 16:51):

Are we talking about mutuals in general or nested inductive mutuals?

Qinshi Wang (Feb 15 2022 at 16:52):

Mutual inductive types that use list and so on in their declaration.

Enrico Tassi (Feb 15 2022 at 16:53):

@Ali Caglayan I was talking about writing Inductive rose := Node (l : list rose) | Leaf as Inductive rose := Node (l : my_list) | Leaf with Inductive my_list := MyNil | MyCons (x : rose) (xs : my_list)

Qinshi Wang (Feb 15 2022 at 16:54):

@Enrico Tassi
Inductive ExpressionPreT :=
| ExpBool (b: bool)
...
with Expression :=
| MkExpression (tags: tags_t) (expr: ExpressionPreT) (typ: @P4Type tags_t) (dir: direction).

Qinshi Wang (Feb 15 2022 at 16:54):

We use mutual induction to add on additional information. It's unnecessary but makes things easier.

Ali Caglayan (Feb 15 2022 at 16:54):

Right, coq doesn't do the "correct" scheme unless its mutual.

Enrico Tassi (Feb 15 2022 at 16:55):

Does ExpressionPreT actually mention Expression?

Qinshi Wang (Feb 15 2022 at 16:55):

@Enrico Tassi Certainly.

Yannick Forster (Feb 15 2022 at 16:55):

Enrico Tassi said:

I think that lifting the algorithm should work. But Coq-Elpi's HOAS of Coq terms does not cover mutual inductive/fixpoints, so you can't really write the extended algorithm in Coq-Elpi :-/

What I meant is that adapting the MetaCoq plugin implementing the same algorithm would not be very hard

Enrico Tassi (Feb 15 2022 at 16:56):

OK, then it is a real mutual, I suggest to follow @Yannick Forster suggestion

Yannick Forster (Feb 15 2022 at 16:57):

I would be interested in discussing whether induction principles with Forall are preferable or not

Yannick Forster (Feb 15 2022 at 16:58):

I think that's orthogonal to supporting mutual inductive types, right? Already the induction principle for tree as above could be written with either a predicate P and using Forall P or with predicates P : tree -> Prop, P' : list (tree) -> Prop

Qinshi Wang (Feb 15 2022 at 16:59):

@Yannick Forster I did have thought about it. It seems it's indeed the strongest, but maybe not ideal for computation when we are using for recursive function rather than inductive proof.

Yannick Forster (Feb 15 2022 at 16:59):

Are you saying the Forall variant is stronger or the "mutual in spirit" variant?

Pierre-Marie Pédrot (Feb 15 2022 at 16:59):

the strongest variant is using the inductive parametricity predicate, which is a generalization of Forall

Qinshi Wang (Feb 15 2022 at 17:00):

Sorry. It seems I misunderstood. You are talking about the existing Forall versus the generated one?

Qinshi Wang (Feb 15 2022 at 17:01):

@Pierre-Marie Pédrot I'm not sure about what you mean.

Pierre-Marie Pédrot (Feb 15 2022 at 17:02):

Forall is just the unary parametricity predicate, and the induction principle for nested inductive types is literally the statement of the parametricity lemma

Pierre-Marie Pédrot (Feb 15 2022 at 17:03):

that is, you define the inductive listε : forall A (P : A -> Type), list A -> Type with nilε : listε A P nil and consε : forall (x : A) (xε : P x) (l : list A) (lε : listε A P l), listε A P (cons x l)

Enrico Tassi (Feb 15 2022 at 17:04):

indeed

Pierre-Marie Pédrot (Feb 15 2022 at 17:04):

with the predicates inlined, I see a major problem which is that the induction tactic must be clever

Pierre-Marie Pédrot (Feb 15 2022 at 17:05):

say you have e.g. P : tree -> Type and Q : list tree -> Type

Pierre-Marie Pédrot (Feb 15 2022 at 17:05):

then induction must invent Q before hand with this variant

Yannick Forster (Feb 15 2022 at 17:05):

I think problems with induction are orthogonal, they would appear already in the hand-written code they currently have, no?

Pierre-Marie Pédrot (Feb 15 2022 at 17:06):

no, it's a design issue that would bubble up

Pierre-Marie Pédrot (Feb 15 2022 at 17:06):

if you pick the predicate lifter variant you don't have to invent a predicate Q so it's easier to use in practice

Yannick Forster (Feb 15 2022 at 17:06):

Are you suggesting a third variant?

Yannick Forster (Feb 15 2022 at 17:07):

There is the unary parametricity variant we have. And there is the variant with two predicates @Qinshi Wang is currently using. Isn't the second what you suggest Pierre-Marie?

Pierre-Marie Pédrot (Feb 15 2022 at 17:07):

no, no, I'm advocating for unary parametricity rather than inlined predicates

Pierre-Marie Pédrot (Feb 15 2022 at 17:08):

(I call inlined predicates the two-predicate variants)

Yannick Forster (Feb 15 2022 at 17:08):

Yes, but are there 3 options on the table and you're advocating for option 1? Or are there 2 and you are advocating for option 1?

Pierre-Marie Pédrot (Feb 15 2022 at 17:08):

there are at least 2, and I am advocating for the first one

Yannick Forster (Feb 15 2022 at 17:09):

I think @Qinshi Wang is already using the other option, so I'd guess that induction already becomes hard to use / unusable

Yannick Forster (Feb 15 2022 at 17:09):

Just from daily experience, I'd also have guessed that the unary parametricity version is always sufficient

Pierre-Marie Pédrot (Feb 15 2022 at 17:10):

it's literally the universal principle, so it's hard to make it any stronger

Qinshi Wang (Feb 15 2022 at 17:10):

Pierre-Marie Pédrot said:

that is, you define the inductive listε : forall A (P : A -> Type), list A -> Type with nilε : listε A P nil and consε : forall (x : A) (xε : P x) (l : list A) (lε : listε A P l), listε A P (cons x l)

Is this just different from Forall by Prop versus Type?

Yannick Forster (Feb 15 2022 at 17:11):

I'd also have guessed that the unary parametricity version is always more convenient to use

Pierre-Marie Pédrot (Feb 15 2022 at 17:12):

@Qinshi Wang unfortunately you need all variants for each sort elimination is allowed into

Pierre-Marie Pédrot (Feb 15 2022 at 17:12):

(I think)

Yannick Forster (Feb 15 2022 at 17:14):

I think we cover that already, but even if not that would be a relatively trivial extension

Yannick Forster (Feb 15 2022 at 17:15):

@Qinshi Wang can you explain why you prefer the two predicate version of induction principles in your code?

Paolo Giarrusso (Feb 15 2022 at 17:18):

@Enrico Tassi

I always had the impression that many mutual types were written like that because Coq did generate bad induction for the non nested variant (e.g. I've seen the type of lists being made mutual for that reason many times).

[BedRock hat off] [Scala / DOT hat on] but that leaves out any grammar that's genuinely mutually recursive...

Paolo Giarrusso (Feb 15 2022 at 17:19):

(there's probably mutual inductives in C++ too, but this isn't something that I've run into at the present job)

Pierre-Marie Pédrot (Feb 15 2022 at 17:20):

Mutual inductive types are encodable away with standard indexed inductive types, but AFAIK that's not the case for nested inductive types.

Pierre-Marie Pédrot (Feb 15 2022 at 17:20):

if you're really desperate you can thus get the right principle by bending a bit the definition

Paolo Giarrusso (Feb 15 2022 at 17:21):

but that sounds like encoding something that works with something that doesn't :sweat_smile:

Paolo Giarrusso (Feb 15 2022 at 17:22):

(or "is not well supported")

Qinshi Wang (Feb 15 2022 at 17:22):

Pierre-Marie Pédrot said:

Qinshi Wang unfortunately you need all variants for each sort elimination is allowed into

Can we define
Definition list_ind A (P : list A -> Prop) := list_rect P.

TJ Barclay (Feb 15 2022 at 17:23):

Qinshi Wang said:

Pierre-Marie Pédrot said:

Qinshi Wang unfortunately you need all variants for each sort elimination is allowed into

Can we define
Definition list_ind A (P : list A -> Prop) := list_rect P.

This is currently what I do by hand for my nested inductive types

Qinshi Wang (Feb 15 2022 at 17:24):

Yannick Forster said:

Qinshi Wang can you explain why you prefer the two predicate version of induction principles in your code?

Because it's easy to write, I guess?
Oh, I guess actually, it's much nicer when handling monads.

Pierre-Marie Pédrot (Feb 15 2022 at 17:28):

I'm not sure that in the case of nested inductive types, relying on the Prop ⊆ Type cumulativity gives rise to an equivalent principle, actually

Qinshi Wang (Feb 15 2022 at 17:28):

For example, we want (Q : list A -> Type) to be (m (list A)) instead of (list (m A)).

Qinshi Wang (Feb 15 2022 at 17:28):

I don't mean we have carefully justified this design decision. It just happens to be what we're doing.

Qinshi Wang (Feb 15 2022 at 17:42):

Yannick Forster said:

Are you saying the Forall variant is stronger or the "mutual in spirit" variant?

I just understood what you mean by "mutual in spirit". The "mutual in spirit" version easily implies the Forall version by putting Forall as Q in it. But for inductive proofs, it seems the Forall version always works because the strongest induction hypothesis for list A is (Forall P), where P is the induction hypothesis for a single point. So they should be equivalent for the Prop case.

Yannick Forster (Feb 15 2022 at 17:44):

And they are not equivalent for the Type case?

Yannick Forster (Feb 15 2022 at 17:44):

I would be surprised if they are not

Yannick Forster (Feb 15 2022 at 17:44):

For me, the unary parametricity version is easier to write

Yannick Forster (Feb 15 2022 at 17:46):

I didn't expect a fleshed-out answer :) But I guess before spending time on writing a plugin generating induction principles it makes sense to understand how the best induction principles look

Qinshi Wang (Feb 15 2022 at 17:46):

Yannick Forster said:

And they are not equivalent for the Type case?

I think they are not, considering the computation process.

Marcel Ullrich (Feb 15 2022 at 17:48):

I have written another version of the induction principles:
https://github.com/NeuralCoder3/nested_induction_v2
This code is for MetaCoq 8.13, and thus, very similar to the newest version.
It is also more in line with the previous work of Enrico Tassi in Elpi and the
examples from Qinshi.
But is not fully working right now as the 'functorial' lemmas are missing.

@Qinshi It is true that your scheme does not use an explicit Forall construct but I feel like
that the "PAList : list (tree1 A) -> Type" in one of your examples for rose trees
has the same or less functionality as a Forall but needs to be user-provided.
Please correct me if I am wrong.

Pierre-Marie Pédrot (Feb 15 2022 at 17:50):

in such a simple case as rose trees they're equivalent, but there are weird cases permitted with nested inductive types

Qinshi Wang (Feb 15 2022 at 17:54):

As I said, for proof/definition purposes, Forall is the strongest. But for computation purposes, either extraction or proof by computation, we might want to skip some recursive calls?

Pierre-Marie Pédrot (Feb 15 2022 at 17:55):

You can always thunk the subcalls, picking P' := unit -> P.

Pierre-Marie Pédrot (Feb 15 2022 at 17:55):

I don't think it's a good idea anyways to use induction principles when writing programs

Pierre-Marie Pédrot (Feb 15 2022 at 17:56):

they're tailored for cbn

Yannick Forster (Feb 15 2022 at 17:58):

I have convinced myself that you can implement the two predicate version using the parametricity version in the case for rose trees

Yannick Forster (Feb 15 2022 at 17:59):

The proof is straightforward

Yannick Forster (Feb 15 2022 at 17:59):

/ the implementation is straightforward

Pierre-Marie Pédrot (Feb 15 2022 at 18:00):

yeah, it's basically the iso (forall s : A + B, P s) ~ (forall x : A, P (L x)) × (forall y : B, P (R y))

Pierre-Marie Pédrot (Feb 15 2022 at 18:00):

that's a definitional iso

Yannick Forster (Feb 15 2022 at 18:01):

My feeling would be that a "good" plugin would generate the parametricity version, and then there could be a second phase deriving the two predicate version from it

Pierre-Marie Pédrot (Feb 15 2022 at 18:02):

I always have the fancy counter-example Inductive t := T : forall x y : t, x = y -> t if you want an example of a weird nested type.

Pierre-Marie Pédrot (Feb 15 2022 at 18:02):

I never really thought about the 2-predicate inductive principle for that one.

Pierre-Marie Pédrot (Feb 15 2022 at 18:03):

(note the equality between two terms of the type being defined)

Pierre-Marie Pédrot (Feb 15 2022 at 18:04):

more generally, nesting indices is likely a minefield

Gaëtan Gilbert (Feb 15 2022 at 18:04):

(add another constructor so it's not empty)

Pierre-Marie Pédrot (Feb 15 2022 at 18:05):

I don't care about inhabitation of my types, the very fact they type-check is suspicious

Gaëtan Gilbert (Feb 15 2022 at 18:06):

if you try to translate to mutual inductives I guess you get an inductive-inductive

Inductive t := T : forall x y, T_eq x y -> t
with T_eq (a:t) : t -> Prop := T_eq_refl : T_eq a a.

Pierre-Marie Pédrot (Feb 15 2022 at 18:08):

indeed, this is one of the reason I suspect we can already get a bit of induction / induction in the current Coq kernel (or maybe prove UIP who knows)

Pierre-Marie Pédrot (Feb 15 2022 at 18:09):

isn't the 2-predicate variant not writable? I think that the second predicate should not be universally quantified over the equality parameter, but you must put something there and I don't see what it might be

Gaëtan Gilbert (Feb 15 2022 at 18:12):

what?

Pierre-Marie Pédrot (Feb 15 2022 at 18:13):

give me the intended type of the 2-predicate recursor

Gaëtan Gilbert (Feb 15 2022 at 18:17):

something like

Fixpoint t_rect (P:T -> Type) (Q:forall x y, P x -> P y -> T_eq x y -> Type) (fT : forall x px y py e, Q x y px py e -> P (T x y e)) : forall t, P t
with T_eq_rect ... : forall x y e, Q x y (t_rect ... x) (t_rect ... y) e

Gaëtan Gilbert (Feb 15 2022 at 18:18):

(if I remember how the fully general ind-ind recursors work)

Pierre-Marie Pédrot (Feb 15 2022 at 18:29):

hm, I am realizing I don't even know how to implement the parametricity-based induction principle for that one.

Pierre-Marie Pédrot (Feb 15 2022 at 18:34):

I mean I can inhabit the type but I'm not sure it has the right computational behaviour

Yannick Forster (Feb 15 2022 at 19:00):

Can you even have two principles with different behaviour?

Qinshi Wang (Feb 15 2022 at 19:02):

Pierre-Marie Pédrot said:

I don't think it's a good idea anyways to use induction principles when writing programs

Sometimes recursive functions do not pass Coq's structural check and we need to use an induction scheme.

Paolo Giarrusso (Feb 15 2022 at 19:28):

That doesn't sound plausible if the function is hand-written: inlining the induction scheme will give you a scheme-free function.

Paolo Giarrusso (Feb 15 2022 at 19:29):

Sorry: it's not plausible that you have to call the principle. It is true that the right way to do the recursion might be surprising with nested types.

Paolo Giarrusso (Feb 15 2022 at 19:30):

You'll need to write some nested fixpoints; I think it's covered in CPDT

Enrico Tassi (Feb 15 2022 at 21:07):

One of the points solved by the unary parametricity is that fixpoints do pass the termination check, even when composed

Pierre-Marie Pédrot (Feb 15 2022 at 22:25):

Can you even have two principles with different behaviour?

@Yannick Forster I'm pretty sure that due to intensionality there are infinitely many variants of a given recursor. For instance, for natural numbers you could define a variant where you do a η-expansion through pattern-matching in the recursive case

Pierre-Marie Pédrot (Feb 15 2022 at 22:25):

in general recursors are underspecified, you only care about the situation when they're fully applied to a constructor.

Yannick Forster (Feb 15 2022 at 22:26):

But extensionally there should be just one function with the type of the recursor of natural numbers, no?

Pierre-Marie Pédrot (Feb 15 2022 at 22:29):

yes, but extensionality is but an illusion

Pierre-Marie Pédrot (Feb 15 2022 at 22:30):

the "weird nested type" above is slightly more problematic because I am not even sure of the expected computational behaviour of the recursor, and the one I managed to write is not enjoying the one I would have liked to see.

Pierre-Marie Pédrot (Feb 15 2022 at 22:30):

? is Coq guard not strong enough? Am I not skilled enough in dependent-elimination-fu? So many foundational mysteries.

Hugo Herbelin (Feb 16 2022 at 09:12):

On a practical note, seizing the opportunity of parametricity experts being gathered here, with the accumulated knowledge and available implementations, isn't it the right time to deprecate the current system for generating induction schemes in Coq and replace it with a compositional parametricity-based system (supporting nested schemes and schemes for arbitrary abbreviations of type)? This was suggested by @ppedrot in a previous discussion I think.

Yannick Forster (Feb 16 2022 at 09:53):

I think it would be great to have more support for this, yes. What I am unclear about is what the right level of implementation for this is. Should these kinds of features be shipped by Coq natively? That would mean they are implemented in OCaml. Maybe such a feature should be an independent plugin, which is however part of the Coq platform? That would give more flexibility with regard to the implementation and any plugin system part of the Coq platform (Ltac2, Coq-Elpi, MetaCoq) could be used

Gaëtan Gilbert (Feb 16 2022 at 09:54):

nothing stops us from shipping stuff written in ltac2 with coq

Yannick Forster (Feb 16 2022 at 09:55):

We can swap Ltac2 and Mtac from the list then

Pierre-Marie Pédrot (Feb 16 2022 at 09:55):

I'm a supporter of writing it in OCaml as a program translation (i.e. no tactics, just building terms)

Pierre-Marie Pédrot (Feb 16 2022 at 09:56):

this would give us the more robust implementation

Yannick Forster (Feb 16 2022 at 09:56):

Are you a supporter of you writing OCaml program translations, or anybody?

Pierre-Marie Pédrot (Feb 16 2022 at 09:56):

anybody, but I can do it if I find a bit of time

Pierre-Marie Pédrot (Feb 16 2022 at 09:57):

Ltac2 doesn't provide any advantage over OCaml for this kind of stuff

Pierre-Marie Pédrot (Feb 16 2022 at 09:57):

and we're sure to have access to all the lowest-level horrors of inductive types and whatnot.

Yannick Forster (Feb 16 2022 at 09:57):

Maybe my point is a bit orthogonal to actual induction principles. Surely it would be good to have more support for nested X (X being induction, subterm relations, equality deciders, etc) already now in OCaml

Yannick Forster (Feb 16 2022 at 09:58):

But is that the right way to go on the long run?

Pierre-Marie Pédrot (Feb 16 2022 at 09:58):

I believe that for thing so critical as induction schemes, yes

Pierre-Marie Pédrot (Feb 16 2022 at 09:58):

look at the amount of trouble when an autogenerated name changes

Yannick Forster (Feb 16 2022 at 09:58):

My feeling always was that the OCaml part of Coq is even more opaque to newcomers than things like MetaCoq - which is a strong statement, because MetaCoq is very opaque

Pierre-Marie Pédrot (Feb 16 2022 at 09:59):

we can strive to make the translation easy to read (it's not currently)

Paolo Giarrusso (Feb 16 2022 at 10:09):

Since we're recapping the previous discussion, long-term deleting as much OCaml code as possible would be desirable (this might be an exception but I'm not so convinced).

Paolo Giarrusso (Feb 16 2022 at 10:13):

and a reason is exactly "I can do it if I find a bit of time" — the Coq core team cannot scale to all the needed metaprogramming, customizations, etc.

Paolo Giarrusso (Feb 16 2022 at 10:14):

If other tools have limitations that hinder doing this task properly, I'd personally vote for the core team to improve those tools.

Pierre-Marie Pédrot (Feb 16 2022 at 10:16):

I'm fine with people developing their libraries outside but mark my words, autogenerating this kind of subtle code is bound to create backwards compat issues and horrendous eisenbugs

Pierre-Marie Pédrot (Feb 16 2022 at 10:16):

the less impedance, the better

Yannick Forster (Feb 16 2022 at 10:29):

I agree with everything Paolo said, including the ambiguity about the point whether this should be an exception

Hugo Herbelin (Feb 16 2022 at 10:30):

If other tools have limitations that hinder doing this task properly, I'd personally vote for the core team to improve those tools.

I don't think we can say that there is no work involved in the MetaCoq, coq-elpi, and Ltac2 tools. What should be done more?

Hugo Herbelin (Feb 16 2022 at 10:54):

Here are different implementations I know to build the parametricity translation:

• coq-elpi
• MetaCoq
• paramcoq

The one in coq-elpi is particularly compact. If we remove from paramcoq all the debug code and the costly treatment of fixpoints which coq-elpi actually improved (using match-expansion rather than generating obligations), I'm pretty sure it reduces to less than 250 lines. Then, it is a question of taste of which language we prefer I guess, even if I agree with @Pierre-Marie Pédrot that relying directly on the internal structures of Coq gives full control over all the tiny details.

Hugo Herbelin (Feb 16 2022 at 10:55):

This does not mean that functions written in coq-elpi or MetaCoq, or other plugins should not be able to register features usable from Coq (e.g. in tactics). For instance, that would be very useful if induction/elim could automatically take benefit of a scheme written in coq-elpi, MetaCoq or paramcoq. We need for that to make the system of Scheme indeed more flexible and open to extensions by plugins.

Paolo Giarrusso (Feb 16 2022 at 11:31):

I haven't used elpi, but I've seen multiple colleagues pick it up very quickly :-)

Paolo Giarrusso (Feb 16 2022 at 11:32):

I wonder if elpi could also offer the low-level control (as needed) without rewriting the code to another tool, but I don't have an informed opinion on the specifics.

Paolo Giarrusso (Feb 16 2022 at 11:34):

For instance, that would be very useful if induction/elim could automatically take benefit of a scheme written in coq-elpi, MetaCoq or paramcoq.

tactics in Iris Proof Mode (/MoSeL) are extensible via typeclass instances, even if this case seems more challenging (and mixing TCs and CSes will be hard unless unifall lands)

Hugo Herbelin (Feb 16 2022 at 11:40):

Tactics like reflexivity are extensible by means of type classes. Would this be possible for the dependency in induction schemes (sorry for a naive question but my culture in TC is low)?

Pierre-Marie Pédrot (Feb 16 2022 at 11:42):

Yes, but TC is a sledgehammer for this kind of pin.

Pierre-Marie Pédrot (Feb 16 2022 at 11:43):

When you only want a table, it seems to me that bringing in the kind of sheer horror of proof search that TC provides is really counter-indicated.

Matthieu Sozeau (Feb 16 2022 at 11:52):

It's not ideal indeed. Equations uses TCs to lookup induction principle but it's a pretty blind search, I think you might want an explicitely structured table (do you want the dependent or non dependent eliminator, into which sort etc...)

Gaëtan Gilbert (Feb 16 2022 at 11:57):

it seems like we want Register to take a list of strings and refs as keys

Register foo_ind as "induction.prop" foo.

Enrico Tassi (Feb 16 2022 at 12:04):

Paolo Giarrusso said:

I wonder if elpi could also offer the low-level control (as needed) without rewriting the code to another tool, but I don't have an informed opinion on the specifics.

If I knew which kind of control @Pierre-Marie Pédrot is talking about, I would try to answer. IMO it is more about habit, we core devs are all very fluent bin OCaml, not equally fluent in the others languages.

Hugo Herbelin (Feb 16 2022 at 12:11):

(As a parenthesis, I don't think we should be afraid of writing code in OCaml, whose name precisely derives from being the MetaLanguage of LCF. Isabelle also uses ML as meta-language. The APIs of Coq are probably a bit frightening, because some complexity has been accumulated - and cleanups are necessary -, but such complexity would arise also in MetaCoq, and coq-elpi, as they continue to grow.)

Paolo Giarrusso (Feb 16 2022 at 14:28):

such complexity would arise also in MetaCoq, and coq-elpi, as they continue to grow.)

The main requirement is that this doesn't happen. It'd be good if coq-elpi _allowed_ lower-level control _if needed_...

Enrico Tassi (Feb 16 2022 at 14:51):

One of the good points of extension languages is that you can raise the abstraction barriers, and hence simplify the API.

For example declaring an inductive type in OCaml is a horror, just think at the context that you have to provide in which you have to put the parameters but also an entry for the inductive type itself... in Elpi you use a HOAS data type which is much simpler. So you give up some control, and maybe some speed, but the barrier to entry is much lower.
In the same way when you code in Ltac2 (or Elpi) you don't thread sigma (with evars and universe constraints), since the runtime carries them for you. In OCaml you have a monad, which is not a pleasure to work with since the type parameter is unit (for some reasons) so hello CPS...

Moreover, the APIs of all the extension languages we have mentioned here is a fresh start, we have some hope we do a better job than what "history" did in Coq.

Gaëtan Gilbert (Feb 16 2022 at 15:11):

In OCaml you have a monad, which is not a pleasure to work with since the type parameter is unit

??

Enrico Tassi (Feb 16 2022 at 15:28):

The tactic monad

Gaëtan Gilbert (Feb 16 2022 at 15:29):

unit?

Enrico Tassi (Feb 16 2022 at 15:29):

Goal.enter

Gaëtan Gilbert (Feb 16 2022 at 15:30):

the reason isn't a mystery, it's because you can have multiple or 0 goals

Gaëtan Gilbert (Feb 16 2022 at 15:31):

we can add fold_enter : (goal -> 'a -> 'a tactic) -> 'a -> 'a tactic if you want

Enrico Tassi (Feb 16 2022 at 15:32):

I know, but as soon as you need the proof context (the goal) you have 2 choices: write all your code outside the monad, or go CPS

Pierre-Marie Pédrot (Feb 16 2022 at 15:32):

no, you can also fail on non-focussed goals

Enrico Tassi (Feb 16 2022 at 15:33):

no to what?

Pierre-Marie Pédrot (Feb 16 2022 at 15:33):

no to two choices

Pierre-Marie Pédrot (Feb 16 2022 at 15:33):

there are at least three

Pierre-Marie Pédrot (Feb 16 2022 at 15:33):

and also, proof search != term translation

Gaëtan Gilbert (Feb 16 2022 at 15:33):

how are non focussed goals relevant?

Pierre-Marie Pédrot (Feb 16 2022 at 15:34):

I mean that if you have several goals under focus

Enrico Tassi (Feb 16 2022 at 16:02):

I was talking about two "coding styles" to split your code into functions. If you write your bricks outside the monad, well, you lose the state carrying/hiding benefit; if you write them in the monad, most combinators make your bind operator void. IMO using the monad type parameter to separate mono-goal-and-context code and multi-goal-not-same-context code was a mistake, since you have the illusion you can share combinators but you actually can't; better to have two types for tactics (with two monads if you like monads).

Last updated: Apr 19 2024 at 20:01 UTC