The Coq mailing list

[Dan Frumin <difrumin AT gmail.com>]

> On 10 Jan 2014, at 15:21, Nicolas Magaud 
> <magaud AT unistra.fr>
>  wrote:
> 
> Dear Coq users,
> 
> I have a technical question about rewriting with an alternative equality in 
> Coq.
> 
> To make it short, I consider a type A (in Set) equipped with any 
> equivalence relation (equal). I do not want to use Leibnitz Equality.
> I try to prove a goal (see below) which involves rewriting in the type of 
> an universally quantified variable :
> I expect the goal "forall p:(Q x), (R x p)" to be transformed into "forall 
> p:(Q y), (R y p)"  when I try to rewrite with an hypothesis "H:equal x y".
> 
> This actually works fine when "equal" is Leibnitz equality. But with my 
> equality, I simply lead to an error message which I do not know how to 
> interpret.
> Instead, I would have expected the system to tell me about some Proper 
> instances which were missing to do the job correctly.
> 

Right, for the rewrite to succeed you need Q to be a "proper morphism". 
That's it, you need it to respect your equality relation, so that "equal" 
elements in A get sent to equal elements in Prop. 

Probably an axiom like

Proper (equal ==> (=)) Q. 

should do that trick. (I am not sure as I don't have access to Coq at the 
time I'm writing this email). 

You might also want your type A to implement a Setoid class. 

The 'Proper' property is defined in Coq.Classes.Morphisms if I remember this 
correctly 

> Is this just a limitation of the current implementation of Coq (I checked 
> with 8.4pl2 and trunk) or simply impossible to obtain with a non-Leibnitz 
> equality ?
> 
> Thanks in advance for your suggestions.
> 
> Nicolas Magaud
> 
> -------------------------------------------------------------
> 
> Require Import Setoid Morphisms.
> 
> Parameter A:Set.
> 
> Parameter equal : A -> A -> Prop.
> 
> Parameter Q:A-> Prop.
> Parameter R:forall a, Q a->Prop.
> 
> Instance equiv_equal : Equivalence equal.
> Admitted.
> 
> Lemma test : forall x y:A, equal x y -> forall p:(Q x), (R x p).
> intros x y H.
> rewrite H.
> (*
> 
> Error: build_signature: no constraint can apply on a dependent argument
> 
> *)