diff options
-rw-r--r-- | theories/Logic/Hurkens.v | 86 |
1 files changed, 52 insertions, 34 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 903b91a59..ab50d7c48 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -56,24 +56,24 @@ (see http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz). *) -(* Pleasing coqdoc! *) - Set Universe Polymorphism. -(** A modular proof of Hurkens's paradox. It relies on an - axiomatisation of a shallow embedding of system U- (i.e. types of - U- are interepreted by types of Coq). The universes are encoding - in a style, due to Martin-Löf, where they are given with a set of - name and a family [El:Name->Type] which interprets each name into - a type. This allows the encoding of universe to be decoupled from - Coq's universes. Dependent products and abstractions are similarly - postulated rather than encoded as Coq's dependent products and - abstractions. *) +(** * A modular proof of Hurkens's paradox. *) + +(** It relies on an axiomatisation of a shallow embedding of system U- + (i.e. types of U- are interepreted by types of Coq). The + universes are encoding in a style, due to Martin-Löf, where they + are given with a set of name and a family [El:Name->Type] which + interprets each name into a type. This allows the encoding of + universe to be decoupled from Coq's universes. Dependent products + and abstractions are similarly postulated rather than encoded as + Coq's dependent products and abstractions. *) Module Generic. -(** Notations used in the proof. *) +(* begin hide *) +(* Notations used in the proof. Hidden in coqdoc. *) Reserved Notation "'∀₁' x : A , B" (at level 200, x ident, A at level 200,right associativity). Reserved Notation "A '⟶₁' B" (at level 99, right associativity, B at level 200). @@ -90,10 +90,11 @@ Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associati Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity). Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity). +(* end hide *) + Section Paradox. -(* arnaud: do some Coqdoc formatting *) -(** Axiomatisation of impredicative universes in a Martin-Löf style *) +(** ** Axiomatisation of impredicative universes in a Martin-Löf style *) (** System U- has two impredicative universes. In the proof of the paradox they are slightly asymetric (in particular the reduction @@ -102,10 +103,10 @@ Section Paradox. actual system U-. *) -(** Large universe *) +(** *** Large universe *) Variable U1 : Type. Variable El1 : U1 -> Type. -(** Closure by small product *) +(** **** Closure by small product *) Variable Forall1 : forall u:U1, (El1 u -> U1) -> U1. Notation "'∀₁' x : A , B" := (Forall1 A (fun x => B)). Notation "A '⟶₁' B" := (Forall1 A (fun _ => B)). @@ -115,7 +116,8 @@ Variable app1 : forall u B (f:El1 (Forall1 u B)) (x:El1 u), El1 (B x). Notation "f '·₁' x" := (app1 _ _ f x). Variable beta1 : forall u B (f:forall x:El1 u, El1 (B x)) x, (λ₁ y, f y) ·₁ x = f x. -(** Closure by large products ([U1] only needs to quantify over itself) *) +(** **** Closure by large products *) +(** [U1] only needs to quantify over itself. *) Variable ForallU1 : (U1->U1) -> U1. Notation "'∀₂' A , F" := (ForallU1 (fun A => F)). Variable lamU1 : forall F, (forall A:U1, El1 (F A)) -> El1 (∀₂ A, F A). @@ -125,12 +127,13 @@ Variable appU1 : forall F (f:El1(∀₂ A,F A)) (A:U1), El1 (F A). Variable betaU1 : forall F (f:forall A:U1, El1 (F A)) A, (λ₂ x, f x) ·₁ [ A ] = f A. -(** Small universe *) +(** *** Small universe *) (** The small universe is an element of the large one. *) Variable u0 : U1. Notation U0 := (El1 u0). Variable El0 : U0 -> Type. -(** Closure by small product, [U0] does not need reduction rules *) +(** **** Closure by small product *) +(** [U0] does not need reduction rules *) Variable Forall0 : forall u:U0, (El0 u -> U0) -> U0. Notation "'∀₀' x : A , B" := (Forall0 A (fun x => B)). Notation "A '⟶₀' B" := (Forall0 A (fun _ => B)). @@ -138,7 +141,7 @@ Variable lam0 : forall u B, (forall x:El0 u, El0 (B x)) -> El0 (∀₀ x:u, B x) Notation "'λ₀' x , u" := (lam0 _ _ (fun x => u)). Variable app0 : forall u B (f:El0 (Forall0 u B)) (x:El0 u), El0 (B x). Notation "f '·₀' x" := (app0 _ _ f x). -(** Closure by large products *) +(** **** Closure by large products *) Variable ForallU0 : forall u:U1, (El1 u->U0) -> U0. Notation "'∀₀¹' A : U , F" := (ForallU0 U (fun A => F)). Variable lamU0 : forall U F, (forall A:El1 U, El0 (F A)) -> El0 (∀₀¹ A:U, F A). @@ -146,7 +149,7 @@ Variable lamU0 : forall U F, (forall A:El1 U, El0 (F A)) -> El0 (∀₀¹ A:U, F Variable appU0 : forall U F (f:El0(∀₀¹ A:U,F A)) (A:El1 U), El0 (F A). Notation "f '·₀' [ A ]" := (appU0 _ _ f A). -(** Automating the rewrite rules of our encoding. *) +(** ** Automating the rewrite rules of our encoding. *) Local Ltac simplify := (* spiwack: ideally we could use [rewrite_strategy] here, but I am a tad scared of the idea of depending on setoid rewrite in such a simple @@ -159,12 +162,12 @@ Local Ltac simplify_in h := lazy beta in h. -(** Hurkens's paradox. *) +(** ** Hurkens's paradox. *) (** An inhabitant of [U0] standing for [False]. *) Variable F:U0. -(** Preliminary definitions *) +(** *** Preliminary definitions *) Definition V : U1 := ∀₂ A, ((A ⟶₁ u0) ⟶₁ A ⟶₁ u0) ⟶₁ A ⟶₁ u0. Definition U : U1 := V ⟶₁ u0. @@ -182,7 +185,7 @@ Definition I (x:El1 U) : U0 := (∀₀¹ i:U⟶₁u0, le i x ⟶₀ i ·₁ (λ₁ v, (sb v) ·₁ [U] ·₁ le' ·₁ x)) ⟶₀ F . -(** Proof *) +(** *** Proof *) Lemma Omega : El0 (∀₀¹ i:U⟶₁u0, induct i ⟶₀ i ·₁ WF). Proof. @@ -242,11 +245,14 @@ Qed. End Paradox. +(** The [paradox] tactic can be called as a shortcut to use the paradox. *) Ltac paradox h := refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ));cycle 1. End Generic. +(** * Impredicative universes are not retracts. *) + (** There can be no retract to an impredicative Coq universe from a smaller type. In this version of the proof, the impredicativity of the universe is postulated with a pair of functions from the @@ -261,7 +267,7 @@ Let U2 := Type. Let U1:U2 := Type. Variable U0:U1. -(** [U1] is impredicative *) +(** *** [U1] is impredicative *) Variable u22u1 : U2 -> U1. Hypothesis u22u1_unit : forall (c:U2), c -> u22u1 c. (** [u22u1_counit] and [u22u1_coherent] only apply to dependent @@ -276,13 +282,13 @@ Hypothesis u22u1_counit : forall (F:U1->U1), u22u1 (forall A,F A) -> (forall A,F Hypothesis u22u1_coherent : forall (F:U1 -> U1) (f:forall x:U1, F x) (x:U1), u22u1_counit _ (u22u1_unit _ f) x = f x. -(** [U0] is a retract of [U1] *) +(** *** [U0] is a retract of [U1] *) Variable u02u1 : U0 -> U1. Variable u12u0 : U1 -> U0. Hypothesis u12u0_unit : forall (b:U1), b -> u02u1 (u12u0 b). Hypothesis u12u0_counit : forall (b:U1), u02u1 (u12u0 b) -> b. -(** Paradox *) +(** ** Paradox *) Theorem paradox : forall F:U1, F. Proof. @@ -319,15 +325,20 @@ End Paradox. End NoRetractToImpredicativeUniverse. +(** * Prop is not a retract *) -(** * Inconsistency of the existence in the pure Calculus of Constructions of a retract from Prop into a small type of Prop *) +(** The existence in the pure Calculus of Constructions of a retract + from Prop into a small type of Prop is inconsistent. This is a + special case of the previous result. *) Module NoRetractFromSmallPropositionToProp. Section Paradox. -(** Assumption of a retract from Prop to a small type in Prop, using *) -(* equivalence as the equality on propositions *) +(** ** Retract of [Prop] in a small type *) + +(** The retract is axiomatized using logical equivalence as the + equality on propositions. *) Variable bool : Prop. Variable p2b : Prop -> bool. @@ -335,6 +346,8 @@ Variable b2p : bool -> Prop. Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A. Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A). +(** ** Paradox *) + Theorem paradox : forall B:Prop, B. Proof. intros B. @@ -359,9 +372,12 @@ End Paradox. End NoRetractFromSmallPropositionToProp. -(** * Inconsistency of the existence in the Calculus of Constructions with universes of a retract from some Type universe into Prop. *) +(** * Large universes are no retracts of [Prop]. *) -(** Note: Assuming the context [down:Type->Prop; up:Prop->Type; forth: +(** The existence in the Calculus of Constructions with universes of a + retract from some [Type] universe into [Prop] is inconsistent. *) + +(* 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. *) @@ -373,12 +389,14 @@ Definition Type1 := Type : Type2. Section Paradox. -(** Assumption of a retract from Type into Prop *) +(** ** 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. +(** ** Paradox *) + Theorem paradox : forall P:Prop, P. Proof. intros P. @@ -417,7 +435,7 @@ End Paradox. End NoRetractFromTypeToProp. -(** Application: Prop<>Type for some given Type *) +(** * [Prop<>Type]. *) Module PropNeqType. |