diff options
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 65 |
1 files changed, 36 insertions, 29 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index d8fb5dd4..d2327498 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -52,7 +52,7 @@ We let also - IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) - IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.) -with no prerequisite on the non-emptyness of domains +with no prerequisite on the non-emptiness of domains Table of contents @@ -89,12 +89,19 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. *) Set Implicit Arguments. +Local Unset Intuition Negation Unfolding. (**********************************************************************) (** * Definitions *) (** Choice, reification and description schemes *) +(** We make them all polymorphic. Most of them have existentials as conclusion + so they require polymorphism otherwise their first application (e.g. to an + existential in [Set]) will fix the level of [A]. +*) +(* Set Universe Polymorphism. *) + Section ChoiceSchemes. Variables A B :Type. @@ -216,39 +223,39 @@ End ChoiceSchemes. (** Generalized schemes *) Notation RelationalChoice := - (forall A B, RelationalChoice_on A B). + (forall A B : Type, RelationalChoice_on A B). Notation FunctionalChoice := - (forall A B, FunctionalChoice_on A B). + (forall A B : Type, FunctionalChoice_on A B). Definition FunctionalDependentChoice := - (forall A, FunctionalDependentChoice_on A). + (forall A : Type, FunctionalDependentChoice_on A). Definition FunctionalCountableChoice := - (forall A, FunctionalCountableChoice_on A). + (forall A : Type, FunctionalCountableChoice_on A). Notation FunctionalChoiceOnInhabitedSet := - (forall A B, inhabited B -> FunctionalChoice_on A B). + (forall A B : Type, inhabited B -> FunctionalChoice_on A B). Notation FunctionalRelReification := - (forall A B, FunctionalRelReification_on A B). + (forall A B : Type, FunctionalRelReification_on A B). Notation GuardedRelationalChoice := - (forall A B, GuardedRelationalChoice_on A B). + (forall A B : Type, GuardedRelationalChoice_on A B). Notation GuardedFunctionalChoice := - (forall A B, GuardedFunctionalChoice_on A B). + (forall A B : Type, GuardedFunctionalChoice_on A B). Notation GuardedFunctionalRelReification := - (forall A B, GuardedFunctionalRelReification_on A B). + (forall A B : Type, GuardedFunctionalRelReification_on A B). Notation OmniscientRelationalChoice := - (forall A B, OmniscientRelationalChoice_on A B). + (forall A B : Type, OmniscientRelationalChoice_on A B). Notation OmniscientFunctionalChoice := - (forall A B, OmniscientFunctionalChoice_on A B). + (forall A B : Type, OmniscientFunctionalChoice_on A B). Notation ConstructiveDefiniteDescription := - (forall A, ConstructiveDefiniteDescription_on A). + (forall A : Type, ConstructiveDefiniteDescription_on A). Notation ConstructiveIndefiniteDescription := - (forall A, ConstructiveIndefiniteDescription_on A). + (forall A : Type, ConstructiveIndefiniteDescription_on A). Notation IotaStatement := - (forall A, IotaStatement_on A). + (forall A : Type, IotaStatement_on A). Notation EpsilonStatement := - (forall A, EpsilonStatement_on A). + (forall A : Type, EpsilonStatement_on A). (** Subclassical schemes *) @@ -292,7 +299,7 @@ Proof. Qed. Lemma funct_choice_imp_rel_choice : - forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B. + forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B. Proof. intros A B FunCh R H. destruct (FunCh R H) as (f,H0). @@ -305,7 +312,7 @@ Proof. Qed. Lemma funct_choice_imp_description : - forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B. + forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B. Proof. intros A B FunCh R H. destruct (FunCh R) as [f H0]. @@ -318,10 +325,10 @@ Proof. Qed. Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr : - forall A B, FunctionalChoice_on A B <-> + forall A B : Type, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B. Proof. - intros A B; split. + intros A B. split. intro H; split; [ exact (funct_choice_imp_rel_choice H) | exact (funct_choice_imp_description H) ]. @@ -333,7 +340,7 @@ Qed. (** We show that the guarded formulations of the axiom of choice are equivalent to their "omniscient" variant and comes from the non guarded - formulation in presence either of the independance of general premises + formulation in presence either of the independence of general premises or subset types (themselves derivable from subtypes thanks to proof- irrelevance) *) @@ -362,7 +369,7 @@ Proof. Qed. Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice : - forall A B, inhabited B -> RelationalChoice_on A B -> + forall A B : Type, inhabited B -> RelationalChoice_on A B -> IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B. Proof. intros A B Inh AC_rel IndPrem P R H. @@ -374,7 +381,7 @@ Proof. Qed. Lemma guarded_rel_choice_imp_rel_choice : - forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B. + forall A B : Type, GuardedRelationalChoice_on A B -> RelationalChoice_on A B. Proof. intros A B GAC_rel R H. destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)). @@ -793,12 +800,13 @@ be applied on the same Type universes on both sides of the first Require Import Setoid. Theorem constructive_definite_descr_excluded_middle : - ConstructiveDefiniteDescription -> + (forall A : Type, ConstructiveDefiniteDescription_on A) -> (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}). Proof. intros Descr EM P. pose (select := fun b:bool => if b then P else ~P). assert { b:bool | select b } as ([|],HP). + red in Descr. apply Descr. rewrite <- unique_existence; split. destruct (EM P). @@ -814,14 +822,13 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context : (forall P:Prop, P \/ ~ P) -> forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C. Proof. - intros FunReify EM C H. - apply relative_non_contradiction_of_definite_descr; trivial. - auto using constructive_definite_descr_excluded_middle. + intros FunReify EM C H. intuition auto using + constructive_definite_descr_excluded_middle, + (relative_non_contradiction_of_definite_descr (C:=C)). Qed. (**********************************************************************) (** * Choice => Dependent choice => Countable choice *) - (* The implications below are standard *) Require Import Arith. |