# Setoid rewrites with different types and implementations
**URL:** https://discourse.rocq-prover.org/t/setoid-rewrites-with-different-types-and-implementations/268
**Category:** Using Rocq
**Created:** [April 14, 2019, 10:57am UTC](https://discourse.rocq-prover.org/t/setoid-rewrites-with-different-types-and-implementations/268 "2019-04-14T10:57:40Z")
**Posts on this page:** 3
**Page:** 1
### Author:  [@jakobbotsch](https://discourse.rocq-prover.org/u/jakobbotsch)
#### Post date: [April 14, 2019, 10:57am UTC](https://discourse.rocq-prover.org/t/setoid-rewrites-with-different-types-and-implementations/268/1 "2019-04-14T10:57:40Z")
Say I have a simple class for finite maps that allows different implementations:
```auto
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:
```auto
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:
```auto
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`:
```auto
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:
```auto
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:
```auto
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?
---
### Author:  [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)
#### Post date: [April 14, 2019, 11:31am UTC](https://discourse.rocq-prover.org/t/setoid-rewrites-with-different-types-and-implementations/268/2 "2019-04-14T11:31:10Z")
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:
```coq
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.
---
### Author:  [@jakobbotsch](https://discourse.rocq-prover.org/u/jakobbotsch)
#### Post date: [April 14, 2019, 6:07pm UTC](https://discourse.rocq-prover.org/t/setoid-rewrites-with-different-types-and-implementations/268/3 "2019-04-14T18:07:58Z")
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.