Parametricity for fixpoints on specialized instances of type families + preservation of guard properties

[herbelin]

Elpi's derive improves on Keller-Lasson's paramcoq by iota-expanding the body of fixpoints so that there is no need, as in paramcoq, to manually proving that (fix f x := t) x is observationally equal to t[f:=fix f x := t].

I tried to understand better the scope of the iota-expansion trick and found two situations where it does not apply directly:

1. fixpoints over terms in inductive types with non-trivial indices as e.g. for Vector.rectS
2. fixpoints which require to return a variable rather than a constructor so that the guard condition scales, as in Nat.sub where n in the right-hand side should not be expanded so that sub can be used in other fixpoints (e.g., indirectly, in Nat.gcd)

I don't know if these questions have already been investigated in the context of Elpi.

For 1., generalizing first may help, as in the following example:

Inductive A : bool -> Type :=
  | Z b : A b
  | C : A false -> A false.

Fixpoint f (a : A false) : bool :=
  match a with
  | Z b => true
  | C a => f a
  end.

From elpi.apps Require derive.std.
Elpi derive.param1 bool.
Elpi derive.param1 A.
Fail Elpi derive.param1 f.

Fixpoint f_gen b (a : A b) : bool :=
  match a with
  | Z b => true
  | C a => f_gen false a
  end.
Elpi derive.param1 f_gen. (* works *)
Definition is_f := is_f_gen false is_false. (* bypassing the limitation *)

It seems that integrating small inversion can also help in some cases as in this alternative definition of parametricity for f:

Fixpoint is_f (a : A false) (Pa : is_A false is_false a) {struct Pa} : is_bool (f a) :=
  match Pa in (is_A b P_ s1)
     return (if b return A b -> _ then fun _ => unit else fun s1 : A false => is_bool (f s1)) s1
  with
  | is_Z b _ =>
     if b return (if b return A b -> _ then fun _ => unit else fun s1 : A false => is_bool (f s1)) (Z b)
     then tt
     else is_true
  | is_C x P_ =>
     is_f x P_
  end.

For 2., I suspect that inserting rewriting may work but I see also a possible solution Coq side. The idea would be to slightly change the expressiveness of the match construct in Coq, adding to:

match t as x in I y return P y x with
| C z => u
end

an explicit access to the instance of the term being matched:

match t as x in I y return P y x with
| C z as w => u
end

so that is_sub, that is currently generated (up to reduction) as:

Fixpoint is_sub (n : nat) (Pn : is_nat n) {struct Pn} :
    forall m : nat, is_nat m -> is_nat (Nat.sub n m) :=
  match
    Pn in (is_nat s1)
    return (forall m : nat, is_nat m -> is_nat (Nat.sub s1 m))
  with
  | is_O => fun (m : nat) (_ : is_nat m) => is_O
  | is_S x P_ => fun (m : nat) (Pm : is_nat m) =>
      match
        Pm in (is_nat m0)
        return (is_nat match m0 with 0 => S x | S l => Nat.sub x l end)
      with
      | is_O => is_S x P_
      | is_S l Pl => is_sub x P_ l Pl
      end
  end.

would instead be generated as:

Fixpoint is_sub (n : nat) (Pn : is_nat n) {struct Pn} :
    forall m : nat, is_nat m -> is_nat (Nat.sub n m) :=
  match
    Pn in (is_nat s1)
    return (forall m : nat, is_nat m -> is_nat (Nat.sub s1 m))
  with
  | is_O as x => fun (m : nat) (_ : is_nat m) => x
  | is_S x P_ as x => fun (m : nat) (Pm : is_nat m) =>
      match
        Pm in (is_nat m0)
        return (is_nat match m0 with 0 => S x | S l => Nat.sub x l end)
      with
      | is_O => x
      | is_S l Pl => is_sub x P_ l Pl
      end
  end.

and the subterm property on x is preserved. [Added: see coq/ceps#73 for a proposal]

Do you think it would eventually be possible in Elpi to support one way or the others the two examples above? (And more generally, is it possible to imagine one day Coq's generation of _rect schemes to be provided by Elpi?)

[gares]

The author of parametricity is @CohenCyril

[gares]

About returning the original value I think it should be doable, and even desirable. I have no time now to work it out, but I may give it a try eventually