The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Hi all,

I have defined a setoid equality for propositional variables as follows:
============================================
Notation "a ≡≡ b" := (iff a b)  (at level 70).
Structure Morphism  : Type := {
  f       :> Prop -> Prop;
  compat  : forall (x1 x2: Prop), (x1 ≡≡ x2) ≡≡ ((f x1) ≡≡ (f x2))}.

Add Parametric Morphism  (M : Morphism) :
            (@f M) with signature (@iff ==> @iff) as extensional_prop.
Proof.
    apply (compat M).
Qed.

Lemma ProtoT1 : forall (p q:Prop)(F:Morphism), (p ≡≡ q) ≡≡ (F p ≡≡ F q).
Proof.
intros a b F.
split; [intro H;rewrite H;reflexivity | intro H;apply (compat F);assumption].
Qed.
=============================================
But when I try to use rewriting in the demonstration of the following theorem:
=============================================
Lemma ProtoTh5 : forall (p q:Prop), (forall f:Morphism,
                    p ≡≡ (forall r, (p ≡≡ f r) ≡≡ forall r, (q ≡≡ f r))) -> q.
Proof.
intros p q H1.
specialize (H1 T).
assert (H2:(forall p:Prop, (forall r, p ≡≡ T r) ≡≡ p)).
apply ProtoTh4.
assert (H3:=H2).
specialize (H2 p).
specialize (H3 q).
rewrite H2 in H1.
=============================================
The Coq reply is:
Error:
Found no subterm matching "forall r : Prop, p ≡≡ T r" in the current goal.

Is anybody has some idea of what goes wrong here?
Thanks in advance,
Richard

--

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard