The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 14 Nov 2012 01:54:10 +0100,
Jonas Oberhauser 
<s9joober AT gmail.com>
 a écrit :

> Can I prove
> 
> Goal Prop <> Type.
> 
> In coq?
> 
> Kind regards,
> Jonas

I hope you cannot (axiom free context).

But it depends on your axioms.

For example, proof degeneracy (I do not remember in which file it is
included) merge all the Prop into one.

I believe it is:

∀ P, (P = True) ∨ (P = False).

In that context, you can prove it (but the proof may not be as short
as you hoped), using the pigeon hole method (I believe it is its name).

In fact, the only way I know to prove two types differ is with this
method.

This method gives a proof of this lemma:

(injection variant)
∀ A B, (∀ (f : A → B), (∀ x y, (f x = f y) → x = y) →
                       ∃ b, (∀ x, (f x = b) → ⊥))) →
       (A = B) ⇒
       ⊥

(surjection variant)
∀ A B, (∀ (f : A → B), (∀ y, (∃ x, f x = y)) →
                       ∃ x, (∃ y, (f x = f y) ∧ ((x = y) → ⊥))) →
       (A = B) ⇒
       ⊥

As there are "reasonnable" theories where Type and
Prop are in bijection, and "reasonnable" others where
it is not the case, neither (Prop=Type) nor
(Prop≠Type) can be proved AFAIU. Of course (Prop=Type) is not wishable
in a developpement (although I am not sure that in an axiom free
context it is really usable).

========================
P.S. I ended to check it, it is on ClassicalFacts.


prop_degeneracy (also referred to as propositional completeness)
asserts (up to consistency) that there are only two distinct formulas
Definition prop_degeneracy := forall A:Prop, A = True \/ A = False.

prop_extensionality asserts that equivalent formulas are equal
Definition prop_extensionality := forall A B:Prop, (A <-> B) -> A = B.

excluded_middle asserts that we can reason by case on the truth or
falsity of any formula Definition excluded_middle := forall A:Prop, A
\/ ~ A.

We show prop_degeneracy <-> (prop_extensionality /\ excluded_middle)

Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality.

Lemma prop_degen_em : prop_degeneracy -> excluded_middle.

Lemma prop_ext_em_degen :
  prop_extensionality -> excluded_middle -> prop_degeneracy.

A weakest form of propositional extensionality: extensionality for
provable propositions only

Definition provable_prop_extensionality := forall A:Prop, A -> A = True.