Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing
it as a consequence of the derivability of Hurkens' paradox in the
presence of a retract from Type to Prop.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15977 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information
herbelin committed Nov 15, 2012
1 parent ab38868 commit beca7a2
Show file tree
Hide file tree
Showing 2 changed files with 167 additions and 134 deletions.
173 changes: 167 additions & 6 deletions theories/Logic/Hurkens.v
Expand Up @@ -8,29 +8,58 @@
(* Hurkens.v *)
(************************************************************************)

(** This is Hurkens paradox [Hurkens] in system U-, adapted by Herman
Geuvers [Geuvers] to show the inconsistency in the pure calculus of
constructions of a retract from Prop into a small type.
(** Exploiting Hurkens' paradox [[Hurkens95]] for system U- so as to
derive contradictions from
- the existence in the pure Calculus of Constructions of a retract
from Prop into a small type of Prop
- the existence in the Calculus of Constructions with universes
of a retract from some Type universe into Prop
The first proof is a simple and effective formulation by Herman
Geuvers [[Geuvers01]] of a result by Thierry Coquand
[[Coquand90]]. The result implies that Coq with classical logic
stated in impredicative Set is inconsistent and that classical
logic stated in Prop implies proof-irrelevance (see
[ClassicalFacts.v])
The second proof is an adaptation of the first proof by Hugo
Herbelin to eventually prove the inconsistency of Prop=Type.
References:
- [Hurkens] A. J. Hurkens, "A simplification of Girard's paradox",
- [[Coquand90]] T. Coquand, "Metamathematical Investigations of a
Calculus of Constructions", Proceedings of Logic in Computer
Science (LICS'90), 1990.
- [[Hurkens95]] A. J. Hurkens, "A simplification of Girard's paradox",
Proceedings of the 2nd international conference Typed Lambda-Calculi
and Applications (TLCA'95), 1995.
- [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001
(see http://www.cs.kun.nl/~herman/note.ps.gz).
- [[Geuvers01]] H. Geuvers, "Inconsistency of Classical Logic in Type
Theory", 2001, revised 2007
(see http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz).
*)

(* Pleasing coqdoc! *)

(** * Inconsistency of the existence in the pure Calculus of Constructions of a retract from Prop into a small type of Prop *)

Module NoRetractFromSmallPropositionToProp.

Section Paradox.

(** Assumption of a retract from Prop to a small type in Prop, using
equivalence as the equality on propositions *)

Variable bool : Prop.
Variable p2b : Prop -> bool.
Variable b2p : bool -> Prop.
Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
Variable B : Prop.

(** Proof *)

Definition V := forall A:Prop, ((A -> bool) -> A -> bool) -> A -> bool.
Definition U := V -> bool.
Definition sb (z:V) : V := fun A r a => r (z A r) a.
Expand Down Expand Up @@ -79,3 +108,135 @@ exact (lemma2 Omega).
Qed.

End Paradox.

End NoRetractFromSmallPropositionToProp.

Export NoRetractFromSmallPropositionToProp.

(** * Inconsistency of the existence in the Calculus of Constructions with universes of a retract from some Type universe into Prop. *)

(** Note: Assuming the context [down:Type->Prop; up:Prop->Type; forth:
forall (A:Type), A -> up (down A); back: forall (A:Type), up
(down A) -> A; H: forall (A:Type) (P:A->Type) (a:A),
P (back A (forth A a)) -> P a] is probably enough. *)

Module NoRetractFromTypeToProp.

Definition Type2 := Type.
Definition Type1 := Type : Type2.

Section Paradox.

Notation "'rew1' <- H 'in' H'" := (@eq_rect_r Type1 _ (fun X : Type1 => X) H' _ H)
(at level 10, H' at level 10).
Notation "'rew1' H 'in' H'" := (@eq_rect Type1 _ (fun X : Type1 => X) H' _ H)
(at level 10, H' at level 10).

(** Assumption of a retract from Type into Prop *)

Variable down : Type1 -> Prop.
Variable up : Prop -> Type1.
Hypothesis up_down : forall (A:Type1), up (down A) = A :> Type1.

(** Proof *)

Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop.
Definition U : Type1 := V -> Prop.

Definition forth (a:U) : up (down U) := rew1 <- (up_down U) in a.
Definition back (x:up (down U)) : U := rew1 (up_down U) in x.

Definition sb (z:V) : V := fun A r a => r (z A r) a.
Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)).
Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth a)) (back x).
Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x).
Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth a))).
Definition I (x:U) : Prop :=
(forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth x)))) -> False.

Lemma back_forth (a:U) : back (forth a) = a.
Proof.
apply rew_opp_r with (P:=fun X:Type1 => X).
Defined.

Lemma Omega : forall i:U -> Prop, induct i -> up (i WF).
Proof.
intros i y.
apply y.
unfold le, WF, induct.
rewrite up_down.
intros x H0.
apply y.
unfold sb, le', le.
rewrite back_forth.
exact H0.
Qed.

Lemma lemma1 : induct (fun u => down (I u)).
Proof.
unfold induct.
intros x p.
rewrite up_down.
intro q.
generalize (q (fun u => down (I u)) p).
rewrite up_down.
intro r.
apply r.
intros i j.
unfold le, sb, le', le in j |-.
rewrite back_forth in j.
specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth y))).
apply q.
exact j.
Qed.

Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False.
Proof.
intro x.
generalize (x (fun u => down (I u)) lemma1).
rewrite up_down.
intro r. apply r.
intros i H0.
apply (x (fun y => i (fun v => sb v (down U) le' (forth y)))).
unfold le, WF in H0.
rewrite up_down in H0.
exact H0.
Qed.

Theorem paradox : False.
Proof.
exact (lemma2 Omega).
Qed.

End Paradox.

End NoRetractFromTypeToProp.

(** Application: Prop<>Type for some given Type *)

Import NoRetractFromTypeToProp.

Section Prop_neq_Type.

Notation "'rew2' <- H 'in' H'" := (@eq_rect_r Type2 _ (fun X : Type2 => X) H' _ H)
(at level 10, H' at level 10).
Notation "'rew2' H 'in' H'" := (@eq_rect Type2 _ (fun X : Type2 => X) H' _ H)
(at level 10, H' at level 10).

Variable Heq : Prop = Type1 :> Type2.

Definition down : Type1 -> Prop := fun A => rew2 <- Heq in A.
Definition up : Prop -> Type1 := fun A => rew2 Heq in A.

Lemma up_down : forall (A:Type1), up (down A) = A :> Type1.
Proof.
unfold up, down. rewrite Heq. reflexivity.
Defined.

Theorem Prop_neq_Type : False.
Proof.
apply paradox with down up.
apply up_down.
Qed.

End Prop_neq_Type.
128 changes: 0 additions & 128 deletions theories/Logic/UniversesFacts.v

This file was deleted.

0 comments on commit beca7a2

Please sign in to comment.