The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Ben,

Le 24 nov. 2011 à 07:39, Ben Horsfall a écrit :

> Suppose that I have Equivalence instances for two types A and B (arising 
> from PartialOrder instances), and I have a function f : A -> B. I would 
> like to be able to use rewriting in a situation like this:
> 
> Lemma example : forall {A B}
> {eqA RA : relation A} `{PartialOrder A eqA RA}
> {eqB RB : relation B} `{PartialOrder B eqB RB}
> (f : A -> B), forall x y, x === y -> f x === f y.
> Proof. intros. rewrite H1. reflexivity. Qed.
> 
> (=== is overloaded notation for eqA and eqB.) But the rewrite step fails to 
> rewrite the goal (to f y === f y), with missing rewriting constraints. What 
> is required (mathematically and technically) to get this kind of example to 
> work, i.e. to get eqB (or RB for that matter) to respect eqA in the 
> appropriate way?

You need to know that [f] is a morphism for the relations involved,
here a [Proper (eqA ==> eqB) f] premise should suffice.

-- Matthieu