The Coq mailing list

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

Le 27/04/2015 17:40, Soegtrop, Michael a écrit :

Dear Richard,

below is a proof, that this is actually wrong. It gives a counter example, which shows where the problem is.

Thank you for your kind (and precise) help.
Richard

Best regards,

Michael

Lemma ThisIsWrong: 
  (forall (T:Set) (P:T->Prop), forall (x:T), P x -> (forall y, P y))
   -> False.
Proof.
  intros H.
  specialize (H bool).
  specialize (H (fun b => b=true)).
  specialize (H true).
  simpl in H.
  specialize (H eq_refl).
  specialize (H false).
  inversion H.
Qed.

Lemma ThisIsRight: 
  forall (T:Set) (P:T->Prop), (forall (x:T), P x) -> (forall y, P y).
Proof.
  intros T P H.
  assumption.
Qed.

--

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