[SOLVED] Morphism signature for dependently-typed vectors in coq

Morphism signature for dependently-typed vectors in coq

I want to be able to rewrite terms inside the predicate P given to Coq.Vectors.Vector.Forall.

The first attempt does not work due to the missing quantification over n.

From Coq Require Import Vector Morphisms Setoid.

Parameter D : Type.
Parameter R : relation D.

Fail Add Parametric Morphism : (@Forall D)
    with signature (R ==> iff) ==> Forall2 R ==> iff
     as morph1.
(* The term "Forall" has type "(D -> Prop) -> forall n : nat, t D n -> Prop"
   while it is expected to have type "(D -> Prop) -> t D ?n -> Prop". *)

I managed to prove the following, with a fixed vector size, but it is useless in practice.

Add Parametric Morphism n : (fun P => @Vector.Forall D P n)
    with signature (R ==> iff) ==> Forall2 R ==> iff
      as morph2.
Proof.
  intros P Q Hpq v1 v2 Hr.
  rewrite 2 Forall_nth_order.
  rewrite Forall2_nth_order in Hr.
  split; intros Hf i Hi; eapply Hpq; eauto.
  Unshelve.
  all: assumption.
Qed.

What could be a correct signature for morph1?

Solution

This seems seems to be the instance I was looking for:

Add Parametric Morphism : (@Forall D)
    with signature (R ==> iff) ==> forall_relation (fun _ => Forall2 R ==> iff)
      as morph1.

It is however not very practical to use, as it requires an explicit eta-expansion in the term before doing the rewrite.