Setoid rewrites with different types and implementations

Using Coq
1

Say I have a simple class for finite maps that allows different implementations:

Class NatMapType :=
  {
    type : Type;
    lookup : nat -> type -> nat;
    insert : nat -> nat -> type -> type;
  }.

Coercion type : NatMapType >-> Sortclass.

Now let’s say I want to define a relation that says that two maps (with possibly different implementations) behave extensionally the same. A first guess might look like:

Record NatMapEquiv
       {NatMap1 : NatMapType} (map1 : NatMap1)
       {NatMap2 : NatMapType} (map2 : NatMap2) : Prop :=
  {
    lookup_eq : forall n, lookup n map1 = lookup n map2;
  }.

But eventually I want to be able to hook this up to setoid rewrite mechanisms of Coq and this does not have the right signature. So I use a sigma type instead:

Record PackedNatMap :=
  {
    p_type : NatMapType;
    p_val :> p_type;
  }.

Record NatMapEquiv (map1 map2 : PackedNatMap) : Prop :=
  {
    lookup_eq : forall n, lookup n map1 = lookup n map2;
  }.

Now we can give a Proper instance for lookup:

Instance lookup_proper :
  forall n, Proper (NatMapEquiv ==> eq) (fun p => lookup n p).
Proof. intros n x y eq. apply lookup_eq; auto. Qed.

But this does not allow me to use it for rewrites:

Lemma lookup_7 (map1 map2 : PackedNatMap) :
  NatMapEquiv map1 map2 -> lookup 7 map1 = lookup 7 map2.
Proof.
  intros eq.
  rewrite eq.
Error: build_signature: no constraint can apply on a dependent argument

Furthermore, even if it did work in the packed case, I would still like to be able to use it in cases like:

Lemma lookup_7
      {NatMap1 : NatMapType}
      (map1 : NatMap1)
      {NatMap2 : NatMapType}
      (map2 : NatMap2) :
  NatMapEquiv (pack map1) (pack map2) -> lookup 7 map1 = lookup 7 map2.

without having to do other tedious changes/rewrites. Is there a way to accomplish these things?

2

This is probably related to fun p => lookup n p being sugar for fun p => @lookup (p_type p) n (p_val p)
For instance if you give it a name the rewrite eq works:

Definition lookupp n (m : PackedNatMap) := lookup n m. 

Instance lookup_proper :
  forall n, Proper (NatMapEquiv ==> eq) (lookupp n).
Proof. intros n x y eq. apply lookup_eq; auto. Qed.

However the second example doesn’t.

3

Thank you. That at least gives the possibility of trying to keep it in the packed form always, although in some situations I might really need to quantify over a single implementation.