The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> On Dec 10, 2014, at 14:03 , Guillaume Melquiond 
> <guillaume.melquiond AT inria.fr>
>  wrote:
> 
> You presumably simplified your example too much, because this is a case of 
> eta-conversion. So the "change" tactic will happily do the replacement. You 
> do not need any setoid rewriting there.

I just want to show the rewriting which I want to use in the different 
context.
Suppose I do want to do rewrite as shown, how can I do this? Now I got the 
following
error:

Toplevel input, characters 0-54:
Error:
Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting 
constraints.
Unable to satisfy the following constraints:
EVARS:
 ?52==[A Ae H H0 x Heq (do_subrelation:=do_subrelation)
        |- @Proper (nat -> Prop)
             (?50 ==> @Basics.flip Prop Prop Prop Basics.impl)
             (@equiv nat Equiv_instance_0 (testF A A (@mult A H0 x)))]
        (internal placeholder)
 ?51==[A Ae H H0 x Heq (do_subrelation:=do_subrelation)
        |- @Proper ((A -> A) -> nat)
             (@pointwise_relation A A (@equiv A Ae) ==> ?50) 
             (testF A A)] (internal placeholder)
 ?50==[A Ae H H0 x Heq |- relation nat] (internal placeholder)
UNIVERSES:
 Top.55 <= Top.8
 Top.54 <= Top.8
 Top.51 <= Coq.Classes.Equivalence.1905
 Top.50 <= Coq.Classes.Equivalence.1908
 Top.49 <= Coq.Classes.Equivalence.1905
 Top.48 <= Coq.Classes.Equivalence.1908
 Top.47 <= Coq.Classes.Morphisms.44
 Top.46 <= Coq.Classes.Morphisms.45
 Top.38 <= Coq.Classes.SetoidTactics.16
 Top.36 <= Coq.Classes.SetoidTactics.11
 Top.32 <= Top.13
 



Sincerely,
Vadim Zaliva

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