From e8e994afb5a29f92c750fb370d01b704ddf06cc4 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 18 Sep 2014 20:39:34 +0200 Subject: A new version of Hurkens.v. Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs. --- theories/Logic/ClassicalFacts.v | 2 +- theories/Logic/Hurkens.v | 487 ++++++++++++++++++++++++++++------------ 2 files changed, 349 insertions(+), 140 deletions(-) (limited to 'theories/Logic') diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 34ae1cd5b..1a70f7806 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -367,7 +367,7 @@ Section Proof_irrelevance_EM_CC. Proof. refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H. trivial. - apply (paradox B p2b b2p (p2p2 H) p2p1). + apply (NoRetractFromSmallPropositionToProp.paradox B p2b b2p (p2p2 H) p2p1). Qed. End Proof_irrelevance_EM_CC. diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index d7871995c..903b91a59 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -8,22 +8,38 @@ (* Hurkens.v *) (************************************************************************) -(** 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. +(** Exploiting Hurkens's paradox [[Hurkens95]] for system U- so as to + derive various contradictory contexts. + + The file is devided in various sub-modules which all follow the + same structure: a section introduce the contradictory hypotheses + and a theorem named [paradox] concludes the module with a proof of + [False]. + + - The [Generic] module contains the actual Hurkens's paradox for a + postulated shallow encoding of system U- in Coq. This is an + adaptation by Arnaud Spiwack of a previous, more restricted + implementation by Herman Geuvers. It is used to derive every + other special cases of the paradox in this file. + + - The [NoRetractToImpredicativeUniverse] module contains a simple + and effective formulation by Herman Geuvers [[Geuvers01]] of a + result by Thierry Coquand [[Coquand90]]. It states that no + impredicative sort can contain a type of which it is a + retract. This 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 [NoRetractFromSmallPropositionToProp] module is a + specialisation of the [NoRetractToImpredicativeUniverse] module + to the case where the impredicative sort is [Prop]. + + - The [NoRetractFromTypeToProp] module proves that [Prop] cannot + be a retract of a larger type. + + - The [Prop_neq_Type] module proves that [Prop] is different from + any larger [Type]. References: @@ -42,76 +58,306 @@ (* 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. +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. *) + +Module Generic. + +(** Notations used in the proof. *) + +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). +Reserved Notation "'λ₁' x , u" (at level 200, x ident, right associativity). +Reserved Notation "f '·₁' x" (at level 5, left associativity). +Reserved Notation "'∀₂' A , F" (at level 200, A ident, right associativity). +Reserved Notation "'λ₂' x , u" (at level 200, x ident, right associativity). +Reserved Notation "f '·₁' [ A ]" (at level 5, left associativity). +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). +Reserved Notation "'λ₀' x , u" (at level 200, x ident, right associativity). +Reserved Notation "f '·₀' x" (at level 5, left associativity). +Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associativity). +Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity). +Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity). 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. +(* arnaud: do some Coqdoc formatting *) +(** 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 + rules of the small universe are not needed). Therefore, the + axioms are duplicated allowing for a weaker requirement than the + actual system U-. *) + + +(** Large universe *) +Variable U1 : Type. +Variable El1 : U1 -> Type. +(** 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)). +Variable lam1 : forall u B, (forall x:El1 u, El1 (B x)) -> El1 (∀₁ x:u, B x). + Notation "'λ₁' x , u" := (lam1 _ _ (fun x => u)). +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) *) +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). + Notation "'λ₂' x , u" := (lamU1 _ (fun x => u)). +Variable appU1 : forall F (f:El1(∀₂ A,F A)) (A:U1), El1 (F A). + Notation "f '·₁' [ A ]" := (appU1 _ f A). +Variable betaU1 : forall F (f:forall A:U1, El1 (F A)) A, + (λ₂ x, f x) ·₁ [ A ] = f A. + +(** 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 *) +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)). +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 *) +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). + Notation "'λ₀¹' x , u" := (lamU0 _ _ (fun x => u)). +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. *) +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 + file. *) + (repeat rewrite ?beta1, ?betaU1); + lazy beta. + +Local Ltac simplify_in h := + (repeat rewrite ?beta1, ?betaU1 in h); + lazy beta in h. + + +(** Hurkens's paradox. *) + +(** An inhabitant of [U0] standing for [False]. *) +Variable F:U0. + +(** Preliminary definitions *) + +Definition V : U1 := ∀₂ A, ((A ⟶₁ u0) ⟶₁ A ⟶₁ u0) ⟶₁ A ⟶₁ u0. +Definition U : U1 := V ⟶₁ u0. + +Definition sb (z:El1 V) : El1 V := λ₂ A, λ₁ r, λ₁ a, r ·₁ (z·₁[A]·₁r) ·₁ a. + +Definition le (i:El1 (U⟶₁u0)) (x:El1 U) : U0 := + x ·₁ (λ₂ A, λ₁ r, λ₁ a, i ·₁ (λ₁ v, (sb v) ·₁ [A] ·₁ r ·₁ a)). +Definition le' : El1 ((U⟶₁u0) ⟶₁ U ⟶₁ u0) := λ₁ i, λ₁ x, le i x. +Definition induct (i:El1 (U⟶₁u0)) : U0 := + ∀₀¹ x:U, le i x ⟶₀ i ·₁ x. + +Definition WF : El1 U := λ₁ z, (induct (z·₁[U] ·₁ le')). +Definition I (x:El1 U) : U0 := + (∀₀¹ i:U⟶₁u0, le i x ⟶₀ i ·₁ (λ₁ v, (sb v) ·₁ [U] ·₁ le' ·₁ x)) ⟶₀ F +. (** 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. -Definition le (i:U -> bool) (x:U) : bool := - x (fun A r a => i (fun v => sb v A r a)). -Definition induct (i:U -> bool) : Prop := - forall x:U, b2p (le i x) -> b2p (i x). -Definition WF : U := fun z => p2b (induct (z U le)). -Definition I (x:U) : Prop := - (forall i:U -> bool, b2p (le i x) -> b2p (i (fun v => sb v U le x))) -> B. - -Lemma Omega : forall i:U -> bool, induct i -> b2p (i WF). +Lemma Omega : El0 (∀₀¹ i:U⟶₁u0, induct i ⟶₀ i ·₁ WF). Proof. -intros i y. -apply y. -unfold le, WF, induct. -apply p2p2. -intros x H0. -apply y. -exact H0. + refine (λ₀¹ i, λ₀ y, _). + refine (y·₀[_]·₀_). + unfold le,WF,induct. simplify. + refine (λ₀¹ x, λ₀ h0, _). simplify. + refine (y·₀[_]·₀_). + unfold le. simplify. + unfold sb at 1. simplify. + unfold le' at 1. simplify. + exact h0. Qed. -Lemma lemma1 : induct (fun u => p2b (I u)). +Lemma lemma1 : El0 (induct (λ₁ u, I u)). Proof. -unfold induct. -intros x p. -apply (p2p2 (I x)). -intro q. -apply (p2p1 (I (fun v:V => sb v U le x)) (q (fun u => p2b (I u)) p)). -intro i. -apply q with (i := fun y => i (fun v:V => sb v U le y)). + unfold induct. + refine (λ₀¹ x, λ₀ p, _). simplify. + refine (λ₀ q,_). + assert (El0 (I (λ₁ v, (sb v)·₁[U]·₁le'·₁x))) as h. + { generalize (q·₀[λ₁ u, I u]·₀p). simplify. + intros q'. + exact q'. } + refine (h·₀_). + refine (λ₀¹ i,_). + refine (λ₀ h', _). + generalize (q·₀[λ₁ y, i ·₁ (λ₁ v, (sb v)·₁[U] ·₁ le' ·₁ y)]). simplify. + intros q'. + refine (q'·₀_). clear q'. + unfold le at 1 in h'. simplify_in h'. + unfold sb at 1 in h'. simplify_in h'. + unfold le' at 1 in h'. simplify_in h'. + exact h'. Qed. -Lemma lemma2 : (forall i:U -> bool, induct i -> b2p (i WF)) -> B. +Lemma lemma2 : El0 ((∀₀¹i:U⟶₁u0, induct i ⟶₀ i·₁WF) ⟶₀ F). Proof. -intro x. -apply (p2p1 (I WF) (x (fun u => p2b (I u)) lemma1)). -intros i H0. -apply (x (fun y => i (fun v => sb v U le y))). -apply (p2p1 _ H0). + refine (λ₀ x, _). + assert (El0 (I WF)) as h. + { generalize (x·₀[λ₁ u, I u]·₀lemma1). simplify. + intros q. + exact q. } + refine (h·₀_). clear h. + refine (λ₀¹ i, λ₀ h0, _). + generalize (x·₀[λ₁ y, i·₁(λ₁ v, (sb v)·₁[U]·₁le'·₁y)]). simplify. + intros q. + refine (q·₀_). clear q. + unfold le in h0. simplify_in h0. + unfold WF in h0. simplify_in h0. + exact h0. Qed. -Theorem paradox : B. +Theorem paradox : El0 F. Proof. -exact (lemma2 Omega). + exact (lemma2·₀Omega). Qed. End Paradox. -End NoRetractFromSmallPropositionToProp. +Ltac paradox h := + refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ));cycle 1. + +End Generic. + +(** 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 + universe to its type and back which commute with dependent product + in an appropriate way. *) + +Module NoRetractToImpredicativeUniverse. + +Section Paradox. + +Let U2 := Type. +Let U1:U2 := Type. +Variable U0:U1. + +(** [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 + product so that the equations happen in the smaller [U1] rather + than [U2]. Indeed, it is not generally the case that one can + project from a large universe to an impredicative universe and + then get back the original type again. It would be too strong a + hypothesis to require (in particular, it is not true of + [Prop]). The formulation is reminiscent of the monadic + characteristic of the projection from a large type to [Prop].*) +Hypothesis u22u1_counit : forall (F:U1->U1), u22u1 (forall A,F A) -> (forall A,F A). +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] *) +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 *) + +Theorem paradox : forall F:U1, F. +Proof. + intros F. + Generic.paradox h. + (** Large universe *) + + exact U1. + + exact (fun X => X). + + cbn. exact (fun u F => forall x:u, F x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + cbn. easy. + + cbn. exact (fun F => u22u1 (forall x, F x)). + + cbn. exact (fun _ x => u22u1_unit _ x). + + cbn. exact (fun _ x => u22u1_counit _ x). + + cbn. intros **. now rewrite u22u1_coherent. + (** Small universe *) + + exact U0. + (** The interpretation of the small universe is the image of + [U0] in [U1]. *) + + cbn. exact (fun X => u02u1 X). + + cbn. exact (fun u F => u12u0 (forall x:(u02u1 u), u02u1 (F x))). + + cbn. intros * x. exact (u12u0_unit _ x). + + cbn. intros * x. exact (u12u0_counit _ x). + + cbn. exact (fun u F => u12u0 (forall x:u, u02u1 (F x))). + + cbn. intros * x. exact (u12u0_unit _ x). + + cbn. intros * x. exact (u12u0_counit _ x). + + cbn. exact (u12u0 F). + + cbn in h. + exact (u12u0_counit _ h). +Qed. + +End Paradox. + +End NoRetractToImpredicativeUniverse. + + +(** * 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). -Export NoRetractFromSmallPropositionToProp. +Theorem paradox : forall B:Prop, B. +Proof. + intros B. + pose proof + (NoRetractToImpredicativeUniverse.paradox@{Type Prop}) as P. + refine (P _ _ _ _ _ _ _ _ _ _);clear P. + + exact bool. + + exact (fun x => forall P:Prop, (x->P)->P). + + cbn. exact (fun _ x P k => k x). + + cbn. intros F P x. + apply P. + intros f. + exact (f x). + + cbn. easy. + + exact b2p. + + exact p2b. + + exact p2p2. + + exact p2p1. +Qed. + +End Paradox. + +End NoRetractFromSmallPropositionToProp. (** * Inconsistency of the existence in the Calculus of Constructions with universes of a retract from some Type universe into Prop. *) @@ -127,85 +373,44 @@ 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. +Theorem paradox : forall P:Prop, P. 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). + intros P. + Generic.paradox h. + (** Large universe. *) + + exact Type1. + + exact (fun X => X). + + cbn. exact (fun u F => forall x, F x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + cbn. easy. + + exact (fun F => forall A:Prop, F(up A)). + + cbn. exact (fun F f A => f (up A)). + + cbn. + intros F f A. + specialize (f (down A)). + rewrite up_down in f. + exact f. + + cbn. + intros F f A. + destruct (up_down A). cbn. + reflexivity. + + exact Prop. + + cbn. exact (fun X => X). + + cbn. exact (fun A P => forall x:A, P x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun A P => forall x:A, P x). + + cbn. exact (fun _ _ x => x). + + cbn. exact (fun _ _ x => x). + + cbn. exact P. + + exact h. Qed. End Paradox. @@ -214,9 +419,11 @@ End NoRetractFromTypeToProp. (** Application: Prop<>Type for some given Type *) +Module PropNeqType. + Import NoRetractFromTypeToProp. -Section Prop_neq_Type. +Section Paradox. Notation "'rew2' <- H 'in' H'" := (@eq_rect_r Type2 _ (fun X : Type2 => X) H' _ H) (at level 10, H' at level 10). @@ -233,10 +440,12 @@ Proof. unfold up, down. rewrite Heq. reflexivity. Defined. -Theorem Prop_neq_Type : False. +Theorem paradox : False. Proof. apply paradox with down up. apply up_down. Qed. -End Prop_neq_Type. +End Paradox. + +End PropNeqType. -- cgit v1.2.3