The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 14.05.2014 19:46, schrieb Jonas Oberhauser:

Dear Coq-developers,

On tuesday we realized that there is a much shorter proof of PE -> PI then the one given in the standard library (http://coq.inria.fr/stdlib/Coq.Logic.ClassicalFacts.html#), following the following two steps:

1. PE -> forall X:Prop, X -> X = True
2. (forall X:Prop, X -> X = True) -> PI

One elegant formalization is as follows:

Goal prop_extensionality -> proof_irrelevance.
intros D X E F.
assert (C: X=True) by intuition.
subst. destruct E, F. reflexivity.
Qed.

Why does the standard library include the other proof over this one?

Kind regards,

jonas

As a side note, the script goes through if you replace prop_extensionality by provable_prop_extensionality:

Goal provable_prop_extensionality -> proof_irrelevance.
intros D X E F.
assert (C: X=True) by intuition.
subst. destruct E, F. reflexivity.
Qed.

Kind regards,
jonas