The Coq mailing list

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

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