diff options
Diffstat (limited to 'theories/Logic')
30 files changed, 145 insertions, 118 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index d72f4072..1e0bd0fe 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index d2327498..1420a000 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 600db472..14d83501 100644 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 07153b35..7041ee40 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index bdad50e2..9e6d07b2 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 2d9a1ffd..0e91613d 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 6f736e45..c947062a 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -442,10 +442,10 @@ Section Proof_irrelevance_WEM_CC. Theorem wproof_irrelevance_cc : ~~(b1 = b2). Proof. intros h. - refine (let NB := exist (fun P=>~~P -> P) B _ in _). + unshelve (refine (let NB := exist (fun P=>~~P -> P) B _ in _)). { exact (fun _ => b1). } pose proof (NoRetractToNegativeProp.paradox NB p2b b2p (wp2p2 h) wp2p1) as paradox. - refine (let F := exist (fun P=>~~P->P) False _ in _). + unshelve (refine (let F := exist (fun P=>~~P->P) False _ in _)). { auto. } exact (paradox F). Qed. @@ -658,4 +658,3 @@ Proof. exists x; intro; exact Hx. exists x0; exact Hnot. Qed. - diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index 4b0ec15e..57f367e5 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index 8468ced3..6665798d 100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index be75c4e9..2c69d4f0 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 6f5bfae4..a304dd24 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 545f92bd..2ba7253c 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v index 70cc0787..0239222e 100644 --- a/theories/Logic/Description.v +++ b/theories/Logic/Description.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 64517354..23af5afc 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v index fe17cde4..ffbb5758 100644 --- a/theories/Logic/Epsilon.v +++ b/theories/Logic/Epsilon.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index d9ffe68d..f3a2783e 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 34aba486..30e26c7c 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 65011e8e..b7b4dec2 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v index 61ee9eb9..0e34e7e9 100644 --- a/theories/Logic/ExtensionalityFacts.v +++ b/theories/Logic/ExtensionalityFacts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/FinFun.v b/theories/Logic/FinFun.v index 670aa219..06466801 100644 --- a/theories/Logic/FinFun.v +++ b/theories/Logic/FinFun.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index eb50a3aa..04d9a670 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index ede51f57..8ded7476 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -266,7 +266,7 @@ End Paradox. (** The [paradox] tactic can be called as a shortcut to use the paradox. *) Ltac paradox h := - refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ));cycle 1. + unshelve (refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ))). End Generic. @@ -319,77 +319,31 @@ Proof. + 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. - -(** * Prop is not a retract *) - -(** 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. - -(** ** 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. -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. - 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. + + cbn. intros **. now rewrite u22u1_coherent. + + cbn. intros * x. exact (u12u0_unit _ x). + + cbn. intros * x. exact (u12u0_counit _ x). + + cbn. intros * x. exact (u12u0_unit _ x). + + cbn. intros * x. exact (u12u0_counit _ x). Qed. End Paradox. -End NoRetractFromSmallPropositionToProp. +End NoRetractToImpredicativeUniverse. (** * Modal fragments of [Prop] are not retracts *) @@ -428,7 +382,7 @@ Qed. Definition Forall {A:Type} (P:A->MProp) : MProp. Proof. - refine (exist _ _ _). + unshelve (refine (exist _ _ _)). + exact (forall x:A, El (P x)). + intros h x. eapply strength in h. @@ -458,27 +412,27 @@ Proof. + exact (fun _ => Forall). + cbn. exact (fun _ _ f => f). + cbn. exact (fun _ _ f => f). - + cbn. easy. + exact Forall. + cbn. exact (fun _ f => f). + cbn. exact (fun _ f => f). - + cbn. easy. (** Small universe *) + exact bool. + exact (fun b => El (b2p b)). + cbn. exact (fun _ F => p2b (Forall (fun x => b2p (F x)))). + + exact (fun _ F => p2b (Forall (fun x => b2p (F x)))). + + apply p2b. + exact B. + + cbn in h. auto. + + cbn. easy. + + cbn. easy. + cbn. auto. + cbn. intros * f. apply p2p1 in f. cbn in f. exact f. - + exact (fun _ F => p2b (Forall (fun x => b2p (F x)))). + cbn. auto. + cbn. intros * f. apply p2p1 in f. cbn in f. exact f. - + apply p2b. - exact B. - + cbn in h. auto. Qed. End Paradox. @@ -516,23 +470,97 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem paradox : forall B:NProp, El B. Proof. intros B. - refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1. + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + exact (fun P => ~~P). + + exact bool. + + exact p2b. + + exact b2p. + + exact B. + + exact h. + cbn. auto. + cbn. auto. + cbn. auto. + + auto. + + auto. +Qed. + +End Paradox. + +End NoRetractToNegativeProp. + +(** * Prop is not a retract *) + +(** 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. + +(** ** The universe of propositions. *) + +Definition NProp := { P:Prop | P -> P}. +Definition El : NProp -> Prop := @proj1_sig _ _. + +Section MParadox. + +(** ** Retract of [Prop] in a small type, using the identity modality. *) + +Variable bool : NProp. +Variable p2b : NProp -> El bool. +Variable b2p : El bool -> NProp. +Hypothesis p2p1 : forall A:NProp, El (b2p (p2b A)) -> El A. +Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). + +(** ** Paradox *) + +Theorem mparadox : forall B:NProp, El B. +Proof. + intros B. + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + + exact (fun P => P). + exact bool. + exact p2b. + exact b2p. - + auto. - + auto. + exact B. + exact h. + + cbn. auto. + + cbn. auto. + + cbn. auto. + + auto. + + auto. +Qed. + +End MParadox. + +Section Paradox. + +(** ** 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. +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. + unshelve (refine (mparadox (exist _ bool (fun x => x)) _ _ _ _ + (exist _ B (fun x => x)))). + + intros p. red. red. exact (p2b (El p)). + + cbn. intros b. red. exists (b2p b). exact (fun x => x). + + cbn. intros [A H]. cbn. apply p2p1. + + cbn. intros [A H]. cbn. apply p2p2. Qed. End Paradox. -End NoRetractToNegativeProp. +End NoRetractFromSmallPropositionToProp. + (** * Large universes are no retracts of [Prop]. *) @@ -569,7 +597,6 @@ Proof. + 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. @@ -577,20 +604,21 @@ Proof. specialize (f (down A)). rewrite up_down in f. exact f. + + exact Prop. + + cbn. exact (fun X => X). + + cbn. exact (fun A P => forall x:A, P x). + + cbn. exact (fun A P => forall x:A, P x). + + cbn. exact P. + + exact h. + + cbn. easy. + 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. @@ -637,37 +665,37 @@ Proof. + cbn. exact (fun X F => forall x:X, F x). + cbn. exact (fun _ _ x => x). + cbn. exact (fun _ _ x => x). - + cbn. easy. + exact (fun F => forall x:A, F (up x)). + cbn. exact (fun _ f => fun x:A => f (up x)). + cbn. intros * f X. specialize (f (down X)). rewrite up_down in f. exact f. - + cbn. intros ? f X. - destruct (up_down X). cbn. - reflexivity. (** Small universe *) + exact A. (** The interpretation of [A] as a universe is [U]. *) + cbn. exact up. + cbn. exact (fun _ F => down (forall x, up (F x))). + + cbn. exact (fun _ F => down (forall x, up (F x))). + + cbn. exact (down False). + + rewrite up_down in p. + exact p. + + cbn. easy. + + cbn. intros ? f X. + destruct (up_down X). cbn. + reflexivity. + cbn. intros ? ? f. rewrite up_down. exact f. + cbn. intros ? ? f. rewrite up_down in f. exact f. - + cbn. exact (fun _ F => down (forall x, up (F x))). + cbn. intros ? ? f. rewrite up_down. exact f. + cbn. intros ? ? f. rewrite up_down in f. exact f. - + cbn. exact (down False). - + rewrite up_down in p. - exact p. Qed. End Paradox. @@ -683,7 +711,7 @@ Module PropNeqType. Theorem paradox : Prop <> Type. Proof. intros h. - refine (TypeNeqSmallType.paradox _ _). + unshelve (refine (TypeNeqSmallType.paradox _ _)). + exact Prop. + easy. Qed. diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v index 9875710e..21be5032 100644 --- a/theories/Logic/IndefiniteDescription.v +++ b/theories/Logic/IndefiniteDescription.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 98cddf0a..2f95856b 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v index eb00dedd..305839cd 100644 --- a/theories/Logic/ProofIrrelevance.v +++ b/theories/Logic/ProofIrrelevance.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v index 6ab6abcf..19b3e9e6 100644 --- a/theories/Logic/ProofIrrelevanceFacts.v +++ b/theories/Logic/ProofIrrelevanceFacts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index 61598130..d16835f8 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v index f110237e..33fce6cc 100644 --- a/theories/Logic/SetIsType.v +++ b/theories/Logic/SetIsType.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v index 408eca4a..95f3e83f 100644 --- a/theories/Logic/WKL.v +++ b/theories/Logic/WKL.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -40,7 +40,7 @@ Proposition is_path_from_characterization P n l : Proof. intros. split. - induction 1 as [|* HP _ (l'&Hl'&HPl')|* HP _ (l'&Hl'&HPl')]. - + exists []. split. reflexivity. intros n <-/le_n_0_eq. assumption. + + exists []. split. reflexivity. intros n <-%le_n_0_eq. assumption. + exists (true :: l'). split. apply eq_S, Hl'. intros [|] H. * assumption. * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H. @@ -51,10 +51,10 @@ intros. split. + constructor. apply (HPl' 0). apply le_0_n. + eapply next_left. * apply (HPl' 0), le_0_n. - * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. + * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. + apply next_right. * apply (HPl' 0), le_0_n. - * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. + * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption. Qed. (** [infinite_from P l] means that we can find arbitrary long paths diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v index 2f84ebe5..4416d38d 100644 --- a/theories/Logic/WeakFan.v +++ b/theories/Logic/WeakFan.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -89,7 +89,7 @@ Qed. Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P []. Proof. intros P Hbar. -destruct Hbar with (X P) as (l,(Hd/Y_approx,HP)). +destruct Hbar with (X P) as (l,(Hd%Y_approx,HP)). assert (inductively_barred P l) by (apply (now P l), HP). clear Hbar HP. induction l as [|a l]. |