The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Richard,

  I suppose it's your parentheses that are incorrect:

Lemma ProtoTh5 : forall (p q:Prop), forall (T :Morphism), (forall f:Morphism, 

                    p ≡≡ ((forall r, (p ≡≡ f r)) ≡≡ forall r, (q ≡≡ f r))) -> q.

would probably be better (notice the forall r0 renaming in your version).

Cheers,

-- Matthieu

On Tue, Jul 21, 2015 at 4:03 PM richard dapoigny <richard.dapoigny AT univ-savoie.fr> wrote:

Le 21/07/2015 14:29, Matthieu Sozeau a écrit :

Hi Richard,

  I can't replay you script so it's unclear what happens.

Best,

-- Matthieu

Hi Matthieu,
Just before the rewrite tactic, i.e., with:
================================================

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).

================================================
I have the following demonstration step:
================================================
1 subgoals
p : Prop
q : Prop
H1 : p ≡≡ (forall r : Prop, (p ≡≡ T r) ≡≡ (forall r0 : Prop, q ≡≡ T r0))
H2 : (forall r : Prop, p ≡≡ T r) ≡≡ p
H3 : (forall r : Prop, q ≡≡ T r) ≡≡ q
______________________________________(1/1)
q
===============================================
The objective is to rewrite (forall r : Prop, p ≡≡ T r) with p in the _expression_ of H1 (and the same job for (forall r : Prop, q ≡≡ T r) in such a way to get the form:
H1 : p ≡≡ (p ≡≡ q)
Cheers,
Richard