The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> On Dec 10, 2014, at 23:18 , Guillaume Melquiond 
> <guillaume.melquiond AT inria.fr>
>  wrote:
> 
> Now you are telling me you are not interested in an equivalence based on 
> eta-convertibility, but without explaining what kind of equivalence you 
> need instead. So perhaps you want a pointwise equivalence?

Thanks! That was helpful. Pointwise equivalence should work. It worked on 
trivial example I've sent earlier, but when I tried to extend the approach to 
more complex functions using dependent types it did not work. Here is a new, 
more specific example. It looks like Proper instance does not match the 
requirements.

Set Printing Implicit.

Require Import Setoid.
Require Import Morphisms.
Require Import Vector.

Class Equiv A := equiv : relation A.
Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :> Equivalence (@equiv A 
Ae).
Class Mult A := mult: A -> A -> A.
Instance vecequiv A `{Equiv A} n : Equiv (Vector.t A n). admit. Defined.
Definition Vmap_reord (A B: Type) (n:nat) (f:A->B) (x: Vector.t A n): 
Vector.t B n := Vector.map f x.

Instance Vmap_reord_proper_pointwise n  (M N:Type) `{Ne:!Equiv N, Me:!Equiv 
M}:
  Proper ((pointwise_relation M Ne) ==> (@vecequiv M Me n) ==> (@vecequiv N 
Ne n)) (@Vmap_reord M N n).
Proof. admit. Qed.

Lemma test (A:Type) `{Setoid A, Ma:!Mult A} (x:A) {n} (z: Vector.t A n):
  equiv
    (Vmap_reord A A n (@mult A Ma x) z)
    (Vmap_reord A A n (fun x0 : A => mult x0 x) z).
Proof.
  setoid_replace (fun x0 : A => mult x0 x) with (@mult A Ma x).
  (* ... *)
Qed.

Error:

Toplevel input, characters 0-60:
Error:
Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting 
constraints.
Unable to satisfy the following constraints:
EVARS:
 ?78==[A Ae H Ma x n z Heq (do_subrelation:=do_subrelation)
        |- @Proper (t A n -> Prop)
             (?74 ==> @Basics.flip Prop Prop Prop Basics.impl)
             (@equiv (t A n) (@vecequiv A Ae n)
                (Vmap_reord A A n (@mult A Ma x) z))] (internal placeholder)
 ?77==[A Ae H Ma x n z Heq |- @ProperProxy (t A n) ?75 z]
        (internal placeholder)
 ?76==[A Ae H Ma x n z Heq (do_subrelation:=do_subrelation)
        |- @Proper ((A -> A) -> t A n -> t A n)
             (@pointwise_relation A A (@equiv A Ae) ==> ?75 ==> ?74)
             (Vmap_reord A A n)] (internal placeholder)
 ?75==[A Ae H Ma x n z Heq |- relation (t A n)] (internal placeholder)
 ?74==[A Ae H Ma x n z Heq |- relation (t A n)] (internal placeholder)
UNIVERSES:
 Top.86 <= Top.8
 Top.85 <= Top.8
 Top.82 <= Coq.Classes.Equivalence.1905
 Top.81 <= Coq.Classes.Equivalence.1908
 Top.80 <= Coq.Classes.Equivalence.1905
 Top.79 <= Coq.Classes.Equivalence.1908
 Top.78 <= Coq.Classes.Morphisms.44
 Top.77 <= Coq.Classes.Morphisms.45
 Top.69 <= Coq.Classes.SetoidTactics.16
 Top.67 <= Coq.Classes.SetoidTactics.11
 Top.49 <= Top.13

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva