The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

HI Nicolas, you can use a predicate (allDep below) to pack your
pattern to rewrite into something detectable by rewrite. See below.

You can see in section 26.10 of the manual that there are two
"special" such predicate: all and ex that are automatically refolded
when you try to rewrite on Prop ("products in Prop are implicitly
translated to such applications"). But here you cannot use all and ex
but something like allDep. Using a ltac you should be able to perform
the same kind of replacement.

Best,
Pierre


Require Import Setoid.
Require Import Setoid Morphisms_Prop.
Require Import 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.

Definition allDep (Q: A -> Prop) (R:forall a, Q a->Prop) (x:A) :=
  forall p:(Q x), (R x p).

Add Parametric Morphism (Q: A -> Prop) (R:forall a, Q a->Prop):
  (@allDep Q R)
  with signature (equal ==> iff)
    as morph.
Admitted.


(* Lemma test : forall x y:A, equal x y -> forall p:(Q x), (R x p). *)
Lemma test : forall x y:A, equal x y -> allDep Q R x.
intros x y H.
rewrite H.