Applying the parametricity techniques to the generation of Boolean equality

[herbelin]

Hi, I made recently an experiment of using parametricity techniques in Coq to automatically generate a Boolean equality associated to an inductive type as an alternative to the ad hoc algorithm currently in use.

It worked surprisingly well (see rocq-prover/rocq#15527) but I stumbled too on the fix typing issue, that is on the question of proving that F (fix F) is convertible to fix F. I may have a solution working sometimes and reminiscent of the trick used for nice fixpoints in paramcoq. The trick is to use a "match"-expansion: for x an inhabitant of the inductive type and assuming the type has constructor C, we can translate fix f x := F f x as

fix f_R x x' x_R :=
  match x_R with
  | C_R y y' y_R => F_R (fix f x := F f x) (fix f x := F f x) f_R (C y) (C y') (C_R y y' y_R)
  end

what forces the reduction of (fix f x := F f x) y inside F_R into F f y, because y is now a constructor able to trigger the reduction.

I don't know yet the exact extent of the trick. It seems to require further match-expansions in F_R if there are other match in it.

Here is an example for the case of Boolean equality:

Fixpoint f n := (nat * match n with 0 => nat | S n => f n end)%type.

Require Import Bool.

Fail Fixpoint f_beq n : f n -> f n -> bool :=
 fun '(a1,a2) '(b1,b2) => Nat.eqb a1 b1 &&
  match n return f n -> f n -> bool with
  | 0 => Nat.eqb a2 b2
  | S n => f_beq a2 b2
  end.

Fixpoint f_beq n : f n -> f n -> bool :=
  match n return f n -> f n -> bool with
  | 0 => fun '(a1,a2) '(b1,b2) => Nat.eqb a1 b1 && Nat.eqb a2 b2
  | S n => fun '(a1,a2) '(b1,b2) => Nat.eqb a1 b1 && f_beq n a2 b2
  end.

PS: Long time ago, @mlasson mentioned to me a problem with typing fixpoints in CIC but I have to confess that I don't remember if it was about adjusting the types in the recursive call or about the issue with constraints over indices in fixpoints, or maybe about both. So, maybe this was related.

[CohenCyril]

I think the match expansion trick is exactly what we do in coq elpi parametricity implementation

[CohenCyril]

https://github.com/LPCIC/coq-elpi/blob/d8ec6c9c3d7415e0273be71b802264287c81ff56/apps/derive/elpi/param2.elpi#L64

[CohenCyril]

And I think @gares implementation of equality generation and induction scheme reuses this and the same trick...

[gares]

not for equality test, but for induction yes.
eq test is not total on cic, I never understood what parametricity would simplify.

[herbelin]

Ah, thanks for the information! I mentioned I had an issue with fixpoints last Wednesday at the Coq call and it did not ring a bell to anyone. So, I should probably have had to explain the exact problems I had.

About Boolean equality, it is not a problem that it is not total. One can do the parametricity in an option type and return a result only when it is not None. What we gain with parametricity is that we mechanically support the whole language with all its complexity, for instance, the new algorithm supports:

Inductive GI (F:Type->Type) A := GC : F A -> F nat -> GI F A.
Inductive K2 (b:bool) (F : if b then Type else Type->Type) : Type :=
  C2 : (if b return (if b then Type else Type->Type) -> Type
        then fun A => A else fun F => F nat) F ->
        K2 b F.

which I don't think elpi support (see the PR for examples).

Anyway, this is very good news. I've been very enthousiastic when I learned all what elpi derive can do. The need for schemes is ubiquitous and we should make their automatic generation widely available.

What would be e.g. the cost of using the parametricity techniques everywhere in elpi? And how easy would it be to plug the elpi generation of schemes directly within Coq so that e.g. at least all the _rect schemes (which currently are limited when it comes to nested and mutual types) can be provided systematically?

Also, compared to paramcoq, are there further cooperations to install, e.g. so that the match-expansion trick is transferred to paramcoq, and, conversely, if ever paramcoq does things that elpi does not (maybe e.g. deriving schemes also for constants?) can be transferred to elpi?

[gares]

How do you get a boolean test for W for example?

[herbelin]

How do you get a boolean test for W for example?

In practice, the algorithm sees a function type and fails.

But if your question is about what is theoretically possible, we could build a Boolean equality for W A B if B can be equipped with an operator B_forall_eq of type forall a, forall C, (C -> C -> bool) -> (B a -> C) -> (B a -> C) -> bool. This would be the case in particular if B a is finite for every a.

More generally, Escardó and Oliva have explored the decidability of non-finite decidable types and shown that there is a duality between types with decidable equality and compact types (see e.g. this talk). That would be very interesting to apply their work to the synthesis of Boolean equality and, e.g. produce automatically the Boolean equality for (nat -> bool) -> nat which they say is decidable.

[herbelin]

@CohenCyril , @gares:

I think the match expansion trick is exactly what we do in coq elpi parametricity implementation

Do you have an idea of the extent of the applicability of the match-expansion trick? For instance, the if in the following example seems to require extra work:

Fixpoint f (b:bool) n := if b then match n return Type with 0 => nat | S n => f b n end else nat.
Inductive I b n := C : f b n -> I b n.

Is the match-expansion trick documented somewhere? If not, that would justify writing a note about it, what do you think?

[proux01]

I'm not a parametricity expert and I'm just maintaining paramcoq because I'm using it through CoqEAL.
My maintainer point of view: if paramcoq can be subsumed by something implemented in coq-elpi for instance, I'd be happy to ditch paramcoq (or replace it, the coq-elpi implem could even be called paramcoq 2.0 if we want).
Currently, many changes in Coq require both an overlay to paramcoq and coq-elpi, so it seems to me that an elpi implem of paramcoq would save work for Coq developpers.

[gares]

if paramcoq can be subsumed by something implemented in coq-elpi

The only problem I see is that paramcoq does support full CIC. coq-elpi does not cover mutual stuff (and univpoly, but that is coming). So maybe in the future, but not today.

[proux01]

Sure, no hurry (and I wouldn't say the support of univpoly in paramcoq is very elaborate)

[herbelin]

Do you have an idea of the extent of the applicability of the match-expansion trick? For instance, the if in the following example seems to require extra work:

Fixpoint f (b:bool) n := if b then match n return Type with 0 => nat | S n => f b n end else nat.
Inductive I b n := C : f b n -> I b n.

Actually, the example works w/o extra effort and elpi generates parametricity for it (I took a wrong path in my previous investigations). These are good news.

From elpi.apps Require Import derive.
Notation F := (fix f (b:bool) n {struct n} := if b then match n with 0 => nat | S n => f b n end else nat).
Inductive I b n := C : F b n -> I b n.
derive nat.
derive bool.
derive I.
Print I_is_I.

So, regarding standard parametricity, my summary so far is that:

• paramcoq misses a "nice" (and simple) treatment of "fix" not requiring (the now apparently broken) proof obligation system; incidentally, it also misses support for the recent constructors float, int, array (a priori easy to add);
• elpi derive misses polymorphic universes, mutual inductive types and schemes for non-inductive objects; which all seem without surprise to implement;
• on its side, Coq is missing a way to internally have access to what paramcoq or elpi are able to produce.