The Coq mailing list

[Ben Horsfall <ben.horsfall AT gmail.com>]

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?


Ben