diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Arith/Between.v | 72 | ||||
| -rw-r--r-- | theories/Init/Datatypes.v | 6 | ||||
| -rw-r--r-- | theories/Init/Logic.v | 22 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 23 | ||||
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 462 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 66 | ||||
| -rw-r--r-- | theories/Logic/Diaconescu.v | 20 | ||||
| -rw-r--r-- | theories/Logic/ExtensionalFunctionRepresentative.v | 24 | ||||
| -rw-r--r-- | theories/Logic/Hurkens.v | 13 | ||||
| -rw-r--r-- | theories/Logic/PropExtensionality.v | 22 | ||||
| -rw-r--r-- | theories/Logic/PropExtensionalityFacts.v | 109 | ||||
| -rw-r--r-- | theories/Logic/SetoidChoice.v | 60 | ||||
| -rw-r--r-- | theories/Logic/vo.itarget | 5 | ||||
| -rw-r--r-- | theories/PArith/BinPos.v | 28 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 45 | ||||
| -rw-r--r-- | theories/ZArith/Zorder.v | 6 |
16 files changed, 905 insertions, 78 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 58d3a2b38c..5a3d5631d5 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -24,7 +24,7 @@ Section Between. Lemma bet_eq : forall k l, l = k -> between k l. Proof. - induction 1; auto with arith. + intros * ->; auto with arith. Qed. Hint Resolve bet_eq: arith. @@ -37,9 +37,7 @@ Section Between. Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l. Proof. - intros k l H; induction H as [|l H]. - intros; absurd (S k <= k); auto with arith. - destruct H; auto with arith. + induction 1 as [|* [|]]; auto with arith. Qed. Hint Resolve between_Sk_l: arith. @@ -74,32 +72,32 @@ Section Between. Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r. Proof. - red; auto with arith. + split; assumption. Qed. Hint Resolve in_int_intro: arith. Lemma in_int_lt : forall p q r, in_int p q r -> p < q. Proof. - induction 1; intros. - apply le_lt_trans with r; auto with arith. + intros * []. + eapply le_lt_trans; eassumption. Qed. Lemma in_int_p_Sq : - forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat. + forall p q r, in_int p (S q) r -> in_int p q r \/ r = q. Proof. - induction 1; intros. - elim (le_lt_or_eq r q); auto with arith. + intros p q r []. + destruct (le_lt_or_eq r q); auto with arith. Qed. Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r. Proof. - induction 1; auto with arith. + intros * []; auto with arith. Qed. Hint Resolve in_int_S: arith. Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r. Proof. - induction 1; auto with arith. + intros * []; auto with arith. Qed. Hint Immediate in_int_Sp_q: arith. @@ -107,10 +105,9 @@ Section Between. forall k l, between k l -> forall r, in_int k l r -> P r. Proof. induction 1; intros. - absurd (k < k); auto with arith. - apply in_int_lt with r; auto with arith. - elim (in_int_p_Sq k l r); intros; auto with arith. - rewrite H2; trivial with arith. + - absurd (k < k). { auto with arith. } + eapply in_int_lt; eassumption. + - destruct (in_int_p_Sq k l r) as [| ->]; auto with arith. Qed. Lemma in_int_between : @@ -120,17 +117,17 @@ Section Between. Qed. Lemma exists_in_int : - forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. + forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. Proof. - induction 1. - case IHexists_between; intros p inp Qp; exists p; auto with arith. - exists l; auto with arith. + induction 1 as [* ? (p, ?, ?)|]. + - exists p; auto with arith. + - exists l; auto with arith. Qed. Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l. Proof. - destruct 1; intros. - elim H0; auto with arith. + intros * (?, lt_r_l) ?. + induction lt_r_l; auto with arith. Qed. Lemma between_or_exists : @@ -139,9 +136,11 @@ Section Between. (forall n:nat, in_int k l n -> P n \/ Q n) -> between k l \/ exists_between k l. Proof. - induction 1; intros; auto with arith. - elim IHle; intro; auto with arith. - elim (H0 m); auto with arith. + induction 1 as [|m ? IHle]. + - auto with arith. + - intros P_or_Q. + destruct IHle; auto with arith. + destruct (P_or_Q m); auto with arith. Qed. Lemma between_not_exists : @@ -150,14 +149,14 @@ Section Between. (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l. Proof. induction 1; red; intros. - absurd (k < k); auto with arith. - absurd (Q l); auto with arith. - elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'. - replace l with l'; auto with arith. - elim inl'; intros. - elim (le_lt_or_eq l' l); auto with arith; intros. - absurd (exists_between k l); auto with arith. - apply in_int_exists with l'; auto with arith. + - absurd (k < k); auto with arith. + - absurd (Q l). { auto with arith. } + destruct (exists_in_int k (S l)) as (l',[],?). + + auto with arith. + + replace l with l'. { trivial. } + destruct (le_lt_or_eq l' l); auto with arith. + absurd (exists_between k l). { auto with arith. } + eapply in_int_exists; eauto with arith. Qed. Inductive P_nth (init:nat) : nat -> nat -> Prop := @@ -168,15 +167,16 @@ Section Between. Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l. Proof. - induction 1; intros; auto with arith. - apply le_trans with (S k); auto with arith. + induction 1. + - auto with arith. + - eapply le_trans; eauto with arith. Qed. Definition eventually (n:nat) := exists2 k : nat, k <= n & Q k. Lemma event_O : eventually 0 -> Q 0. Proof. - induction 1; intros. + intros (x, ?, ?). replace 0 with x; auto with arith. Qed. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index ddaf08bf71..11d80dbc33 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -262,6 +262,11 @@ Inductive comparison : Set := | Lt : comparison | Gt : comparison. +Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'. +Proof. + destruct c, c'; intro H; reflexivity || destruct H; discriminate. +Qed. + Definition CompOpp (r:comparison) := match r with | Eq => Eq @@ -326,7 +331,6 @@ Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, CompSpec eq lt x y c -> CompSpecT eq lt x y c. Proof. intros. apply CompareSpec2Type; assumption. Defined. - (******************************************************************) (** * Misc Other Datatypes *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 85123cc444..9b58c524e4 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -125,6 +125,25 @@ Proof. [apply Hl | apply Hr]; assumption. Qed. +Theorem imp_iff_compat_l : forall A B C : Prop, + (B <-> C) -> ((A -> B) <-> (A -> C)). +Proof. + intros ? ? ? [Hl Hr]; split; intros H ?; [apply Hl | apply Hr]; apply H; assumption. +Qed. + +Theorem imp_iff_compat_r : forall A B C : Prop, + (B <-> C) -> ((B -> A) <-> (C -> A)). +Proof. + intros ? ? ? [Hl Hr]; split; intros H ?; [apply H, Hr | apply H, Hl]; assumption. +Qed. + +Theorem not_iff_compat : forall A B : Prop, + (A <-> B) -> (~ A <-> ~B). +Proof. + intros; apply imp_iff_compat_r; assumption. +Qed. + + (** Some equivalences *) Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False). @@ -553,7 +572,8 @@ Proof. intros A P (x & Hp & Huniq); split. - intro; exists x; auto. - intros (x0 & HPx0 & HQx0) x1 HPx1. - replace x1 with x0 by (transitivity x; [symmetry|]; auto). + assert (H : x0 = x1) by (transitivity x; [symmetry|]; auto). + destruct H. assumption. Qed. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 9fc00e80c1..2cc2ecbc20 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -103,7 +103,7 @@ Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P of an [a] of type [A], a of a proof [h] that [a] satisfies [P], and a proof [h'] that [a] satisfies [Q]. Then [(proj1_sig (sig_of_sig2 y))] is the witness [a], - [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and + [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and [(proj3_sig y)] is the proof of [(Q a)]. *) Section Subset_projections2. @@ -190,6 +190,23 @@ Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X). +(** η Principles *) +Definition sigT_eta {A P} (p : { a : A & P a }) + : p = existT _ (projT1 p) (projT2 p). +Proof. destruct p; reflexivity. Defined. + +Definition sig_eta {A P} (p : { a : A | P a }) + : p = exist _ (proj1_sig p) (proj2_sig p). +Proof. destruct p; reflexivity. Defined. + +Definition sigT2_eta {A P Q} (p : { a : A & P a & Q a }) + : p = existT2 _ _ (projT1 (sigT_of_sigT2 p)) (projT2 (sigT_of_sigT2 p)) (projT3 p). +Proof. destruct p; reflexivity. Defined. + +Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) + : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). +Proof. destruct p; reflexivity. Defined. + (** [sumbool] is a boolean type equipped with the justification of their value *) @@ -263,10 +280,10 @@ Section Dependent_choice_lemmas. (forall x:X, {y | R x y}) -> forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}. Proof. - intros H x0. + intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. - split. reflexivity. + split. reflexivity. induction n; simpl; apply proj2_sig. Defined. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 1420a000b6..07e8b6ef8d 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -22,7 +22,16 @@ description principles - AC! = functional relation reification (known as axiom of unique choice in topos theory, sometimes called principle of definite description in - the context of constructive type theory) + the context of constructive type theory, sometimes + called axiom of no choice) + +- AC_fun_repr = functional choice of a representative in an equivalence class +- AC_fun_setoid_gen = functional form of the general form of the (so-called + extensional) axiom of choice over setoids +- AC_fun_setoid = functional form of the (so-called extensional) axiom of + choice from setoids +- AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of + choice from setoids on locally compatible relations - GAC_rel = guarded relational form of the (non extensional) axiom of choice - GAC_fun = guarded functional form of the (non extensional) axiom of choice @@ -45,6 +54,11 @@ description principles independence of premises) - Drinker = drinker's paradox (small form) (called Ex in Bell [[Bell]]) +- EM = excluded-middle + +- Ext_pred_repr = choice of a representative among extensional predicates +- Ext_pred = extensionality of predicates +- Ext_fun_prop_repr = choice of a representative among extensional functions to Prop We let also @@ -76,6 +90,10 @@ Table of contents 8. Choice -> Dependent choice -> Countable choice +9.1. AC_fun_ext = AC_fun + Ext_fun_repr + EM + +9.2. AC_fun_ext = AC_fun + Ext_prop_fun_repr + PI + References: [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, @@ -84,8 +102,13 @@ unpublished. [[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic Type Theories, Mathematical Logic Quarterly, volume 39, 1993. +[[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to +AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + [[Carlström05]] Jesper Carlström, Interpreting descriptions in intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. + +[[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997. *) Set Implicit Arguments. @@ -108,8 +131,6 @@ Variables A B :Type. Variable P:A->Prop. -Variable R:A->B->Prop. - (** ** Constructive choice and description *) (** AC_rel *) @@ -121,6 +142,10 @@ Definition RelationalChoice_on := (** AC_fun *) +(* Note: This is called Type-Theoretic Description Axiom (TTDA) in + [[Werner97]] (using a non-standard meaning of "description"). This + is called intensional axiom of choice (AC_int) in [[Carlström04]] *) + Definition FunctionalChoice_on := forall R:A->B->Prop, (forall x : A, exists y : B, R x y) -> @@ -148,6 +173,55 @@ Definition FunctionalRelReification_on := (forall x : A, exists! y : B, R x y) -> (exists f : A->B, forall x : A, R x (f x)). +(** AC_fun_repr *) + +(* Note: This is called Type-Theoretic Choice Axiom (TTCA) in + [[Werner97]] (by reference to the extensional set-theoretic + formulation of choice); Note also a typo in its intended + formulation in [[Werner97]]. *) + +Require Import RelationClasses Logic. + +Definition RepresentativeFunctionalChoice_on := + forall R:A->A->Prop, + (Equivalence R) -> + (exists f : A->A, forall x : A, (R x (f x)) /\ forall x', R x x' -> f x = f x'). + +(** AC_fun_setoid *) + +Definition SetoidFunctionalChoice_on := + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x x' y, R x x' -> T x y -> T x' y) -> + (forall x, exists y, T x y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). + +(** AC_fun_setoid_gen *) + +(* Note: This is called extensional axiom of choice (AC_ext) in + [[Carlström04]]. *) + +Definition GeneralizedSetoidFunctionalChoice_on := + forall R : A -> A -> Prop, + forall S : B -> B -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + Equivalence S -> + (forall x x' y y', R x x' -> S y y' -> T x y -> T x' y') -> + (forall x, exists y, T x y) -> + exists f : A -> B, + forall x : A, T x (f x) /\ (forall x' : A, R x x' -> S (f x) (f x')). + +(** AC_fun_setoid_simple *) + +Definition SimpleSetoidFunctionalChoice_on A B := + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x, exists y, forall x', R x x' -> T x' y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). + (** ID_epsilon (constructive version of indefinite description; combined with proof-irrelevance, it may be connected to Carlström's type theory with a constructive indefinite description @@ -234,6 +308,14 @@ Notation FunctionalChoiceOnInhabitedSet := (forall A B : Type, inhabited B -> FunctionalChoice_on A B). Notation FunctionalRelReification := (forall A B : Type, FunctionalRelReification_on A B). +Notation RepresentativeFunctionalChoice := + (forall A : Type, RepresentativeFunctionalChoice_on A). +Notation SetoidFunctionalChoice := + (forall A B: Type, SetoidFunctionalChoice_on A B). +Notation GeneralizedSetoidFunctionalChoice := + (forall A B : Type, GeneralizedSetoidFunctionalChoice_on A B). +Notation SimpleSetoidFunctionalChoice := + (forall A B : Type, SimpleSetoidFunctionalChoice_on A B). Notation GuardedRelationalChoice := (forall A B : Type, GuardedRelationalChoice_on A B). @@ -271,6 +353,26 @@ Definition SmallDrinker'sParadox := forall (A:Type) (P:A -> Prop), inhabited A -> exists x, (exists x, P x) -> P x. +Definition ExcludedMiddle := + forall P:Prop, P \/ ~ P. + +(** Extensional schemes *) + +Local Notation ExtensionalPropositionRepresentative := + (forall (A:Type), + exists h : Prop -> Prop, + forall P : Prop, (P <-> h P) /\ forall Q, (P <-> Q) -> h P = h Q). + +Local Notation ExtensionalPredicateRepresentative := + (forall (A:Type), + exists h : (A->Prop) -> (A->Prop), + forall (P : A -> Prop), (forall x, P x <-> h P x) /\ forall Q, (forall x, P x <-> Q x) -> h P = h Q). + +Local Notation ExtensionalFunctionRepresentative := + (forall (A B:Type), + exists h : (A->B) -> (A->B), + forall (f : A -> B), (forall x, f x = h f x) /\ forall g, (forall x, f x = g x) -> h f = h g). + (**********************************************************************) (** * AC_rel + AC! = AC_fun @@ -284,7 +386,7 @@ Definition SmallDrinker'sParadox := relational formulation) without known inconsistency with classical logic, though functional relation reification conflicts with classical logic *) -Lemma description_rel_choice_imp_funct_choice : +Lemma functional_rel_reification_and_rel_choice_imp_fun_choice : forall A B : Type, FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B. Proof. @@ -298,7 +400,10 @@ Proof. apply HR'R; assumption. Qed. -Lemma funct_choice_imp_rel_choice : +Notation description_rel_choice_imp_funct_choice := + functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6"). + +Lemma fun_choice_imp_rel_choice : forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B. Proof. intros A B FunCh R H. @@ -311,7 +416,9 @@ Proof. trivial. Qed. -Lemma funct_choice_imp_description : +Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6"). + +Lemma fun_choice_imp_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B. Proof. intros A B FunCh R H. @@ -324,17 +431,21 @@ Proof. exists f; exact H0. Qed. -Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr : +Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6"). + +Corollary fun_choice_iff_rel_choice_and_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B. Proof. intros A B. split. intro H; split; - [ exact (funct_choice_imp_rel_choice H) - | exact (funct_choice_imp_description H) ]. - intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H). + [ exact (fun_choice_imp_rel_choice H) + | exact (fun_choice_imp_functional_rel_reification H) ]. + intros [H H0]; exact (functional_rel_reification_and_rel_choice_imp_fun_choice H0 H). Qed. +Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := + fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6"). (**********************************************************************) (** * Connection between the guarded, non guarded and omniscient choices *) @@ -862,3 +973,334 @@ Proof. rewrite Heq in HR. assumption. Qed. + +(**********************************************************************) +(** * About the axiom of choice over setoids *) + +Require Import ClassicalFacts PropExtensionalityFacts. + +(**********************************************************************) +(** ** Consequences of the choice of a representative in an equivalence class *) + +Theorem repr_fun_choice_imp_ext_prop_repr : + RepresentativeFunctionalChoice -> ExtensionalPropositionRepresentative. +Proof. + intros ReprFunChoice A. + pose (R P Q := P <-> Q). + assert (Hequiv:Equivalence R) by (split; firstorder). + apply (ReprFunChoice _ R Hequiv). +Qed. + +Theorem repr_fun_choice_imp_ext_pred_repr : + RepresentativeFunctionalChoice -> ExtensionalPredicateRepresentative. +Proof. + intros ReprFunChoice A. + pose (R P Q := forall x : A, P x <-> Q x). + assert (Hequiv:Equivalence R) by (split; firstorder). + apply (ReprFunChoice _ R Hequiv). +Qed. + +Theorem repr_fun_choice_imp_ext_function_repr : + RepresentativeFunctionalChoice -> ExtensionalFunctionRepresentative. +Proof. + intros ReprFunChoice A B. + pose (R (f g : A -> B) := forall x : A, f x = g x). + assert (Hequiv:Equivalence R). + { split; try easy. firstorder using eq_trans. } + apply (ReprFunChoice _ R Hequiv). +Qed. + +(** *** This is a variant of Diaconescu and Goodman-Myhill theorems *) + +Theorem repr_fun_choice_imp_excluded_middle : + RepresentativeFunctionalChoice -> ExcludedMiddle. +Proof. + intros ReprFunChoice. + apply representative_boolean_partition_imp_excluded_middle, ReprFunChoice. +Qed. + +Theorem repr_fun_choice_imp_relational_choice : + RepresentativeFunctionalChoice -> RelationalChoice. +Proof. + intros ReprFunChoice A B T Hexists. + pose (D := (A*B)%type). + pose (R (z z':D) := + let x := fst z in + let x' := fst z' in + let y := snd z in + let y' := snd z' in + x = x' /\ (T x y -> y = y' \/ T x y') /\ (T x y' -> y = y' \/ T x y)). + assert (Hequiv : Equivalence R). + { split. + - split. easy. firstorder. + - intros (x,y) (x',y') (H1,(H2,H2')). split. easy. simpl fst in *. simpl snd in *. + subst x'. split; intro H. + + destruct (H2' H); firstorder. + + destruct (H2 H); firstorder. + - intros (x,y) (x',y') (x'',y'') (H1,(H2,H2')) (H3,(H4,H4')). + simpl fst in *. simpl snd in *. subst x'' x'. split. easy. split; intro H. + + simpl fst in *. simpl snd in *. destruct (H2 H) as [<-|H0]. + * destruct (H4 H); firstorder. + * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. + + simpl fst in *. simpl snd in *. destruct (H4' H) as [<-|H0]. + * destruct (H2' H); firstorder. + * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. } + destruct (ReprFunChoice D R Hequiv) as (g,Hg). + set (T' x y := T x y /\ exists y', T x y' /\ g (x,y') = (x,y)). + exists T'. split. + - intros x y (H,_); easy. + - intro x. destruct (Hexists x) as (y,Hy). + exists (snd (g (x,y))). + destruct (Hg (x,y)) as ((Heq1,(H',H'')),Hgxyuniq); clear Hg. + destruct (H' Hy) as [Heq2|Hgy]; clear H'. + + split. split. + * rewrite <- Heq2. assumption. + * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1, Heq2. subst; easy. + * intros y' (Hy',(y'',(Hy'',Heq))). + rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy. + split; right; easy. + + split. split. + * assumption. + * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1. subst x'; easy. + * intros y' (Hy',(y'',(Hy'',Heq))). + rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy. + split; right; easy. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC_fun_setoid_gen = AC_fun_setoid_simple *) + +Theorem gen_setoid_fun_choice_imp_setoid_fun_choice : + forall A B, GeneralizedSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B. +Proof. + intros A B GenSetoidFunChoice R T Hequiv Hcompat Hex. + apply GenSetoidFunChoice; try easy. + apply eq_equivalence. + intros * H <-. firstorder. +Qed. + +Theorem setoid_fun_choice_imp_gen_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> GeneralizedSetoidFunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice R S T HequivR HequivS Hcompat Hex. + destruct SetoidFunChoice with (R:=R) (T:=T) as (f,Hf); try easy. + { intros; apply (Hcompat x x' y y); try easy. } + exists f. intros x; specialize Hf with x as (Hf,Huniq). intuition. now erewrite Huniq. +Qed. + +Corollary setoid_fun_choice_iff_gen_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B <-> GeneralizedSetoidFunctionalChoice_on A B. +Proof. + split; auto using gen_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_gen_setoid_fun_choice. +Qed. + +Theorem setoid_fun_choice_imp_simple_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> SimpleSetoidFunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice R T Hequiv Hexists. + pose (T' x y := forall x', R x x' -> T x' y). + assert (Hcompat : forall (x x' : A) (y : B), R x x' -> T' x y -> T' x' y) by firstorder. + destruct (SetoidFunChoice R T' Hequiv Hcompat Hexists) as (f,Hf). + exists f. firstorder. +Qed. + +Theorem simple_setoid_fun_choice_imp_setoid_fun_choice : + forall A B, SimpleSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B. +Proof. + intros A B SimpleSetoidFunChoice R T Hequiv Hcompat Hexists. + destruct (SimpleSetoidFunChoice R T Hequiv) as (f,Hf); firstorder. +Qed. + +Corollary setoid_fun_choice_iff_simple_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B <-> SimpleSetoidFunctionalChoice_on A B. +Proof. + split; auto using simple_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_simple_setoid_fun_choice. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC! + AC_fun_repr *) + +Theorem setoid_fun_choice_imp_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> FunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice T Hexists. + destruct SetoidFunChoice with (R:=@eq A) (T:=T) as (f,Hf). + - apply eq_equivalence. + - now intros * ->. + - assumption. + - exists f. firstorder. +Qed. + +Corollary setoid_fun_choice_imp_functional_rel_reification : + forall A B, SetoidFunctionalChoice_on A B -> FunctionalRelReification_on A B. +Proof. + intros A B SetoidFunChoice. + apply fun_choice_imp_functional_rel_reification. + now apply setoid_fun_choice_imp_fun_choice. +Qed. + +Theorem setoid_fun_choice_imp_repr_fun_choice : + SetoidFunctionalChoice -> RepresentativeFunctionalChoice . +Proof. + intros SetoidFunChoice A R Hequiv. + apply SetoidFunChoice; firstorder. +Qed. + +Theorem functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice : + FunctionalRelReification -> RepresentativeFunctionalChoice -> SetoidFunctionalChoice. +Proof. + intros FunRelReify ReprFunChoice A B R T Hequiv Hcompat Hexists. + assert (FunChoice : FunctionalChoice). + { intros A' B'. apply functional_rel_reification_and_rel_choice_imp_fun_choice. + - apply FunRelReify. + - now apply repr_fun_choice_imp_relational_choice. } + destruct (FunChoice _ _ T Hexists) as (f,Hf). + destruct (ReprFunChoice A R Hequiv) as (g,Hg). + exists (fun a => f (g a)). + intro x. destruct (Hg x) as (Hgx,HRuniq). + split. + - eapply Hcompat. symmetry. apply Hgx. apply Hf. + - intros y Hxy. f_equal. auto. +Qed. + +Theorem functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice : + FunctionalRelReification /\ RepresentativeFunctionalChoice <-> SetoidFunctionalChoice. +Proof. + split; intros. + - now apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + - split. + + now intros A B; apply setoid_fun_choice_imp_functional_rel_reification. + + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. + +(** Note: What characterization to give of +RepresentativeFunctionalChoice? A formulation of it as a functional +relation would certainly be equivalent to the formulation of +SetoidFunctionalChoice as a functional relation, but in their +functional forms, SetoidFunctionalChoice seems strictly stronger *) + +(**********************************************************************) +(** * AC_fun_setoid = AC_fun + Ext_fun_repr + EM *) + +Import EqNotations. + +(** ** This is the main theorem in [[Carlström04]] *) + +(** Note: all ingredients have a computational meaning when taken in + separation. However, to compute with the functional choice, + existential quantification has to be thought as a strong + existential, which is incompatible with the computational content of + excluded-middle *) + +Theorem fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice : + FunctionalChoice -> ExtensionalFunctionRepresentative -> ExcludedMiddle -> RepresentativeFunctionalChoice. +Proof. + intros FunChoice SetoidFunRepr EM A R (Hrefl,Hsym,Htrans). + assert (H:forall P:Prop, exists b, b = true <-> P). + { intros P. destruct (EM P). + - exists true; firstorder. + - exists false; easy. } + destruct (FunChoice _ _ _ H) as (c,Hc). + pose (class_of a y := c (R a y)). + pose (isclass f := exists x:A, f x = true). + pose (class := {f:A -> bool | isclass f}). + pose (contains (c:class) (a:A) := proj1_sig c a = true). + destruct (FunChoice class A contains) as (f,Hf). + - intros f. destruct (proj2_sig f) as (x,Hx). + exists x. easy. + - destruct (SetoidFunRepr A bool) as (h,Hh). + assert (Hisclass:forall a, isclass (h (class_of a))). + { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). + rewrite <- Ha. apply Hc. apply Hrefl. } + pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). + exists (fun a => f (f' a)). + intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + + specialize Hf with (f' x). unfold contains in Hf. simpl in Hf. rewrite <- Hx in Hf. apply Hc. assumption. + + intros y Hxy. + f_equal. + assert (Heq1: h (class_of x) = h (class_of y)). + { apply Huniqx. intro z. unfold class_of. + destruct (c (R x z)) eqn:Hxz. + - symmetry. apply Hc. apply -> Hc in Hxz. firstorder. + - destruct (c (R y z)) eqn:Hyz. + + apply -> Hc in Hyz. rewrite <- Hxz. apply Hc. firstorder. + + easy. } + assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). + { apply proof_irrelevance_cci, EM. } + unfold f'. + rewrite <- Heq2. + rewrite <- Heq1. + reflexivity. +Qed. + +Theorem setoid_functional_choice_first_characterization : + FunctionalChoice /\ ExtensionalFunctionRepresentative /\ ExcludedMiddle <-> SetoidFunctionalChoice. +Proof. + split. + - intros (FunChoice & SetoidFunRepr & EM). + apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + + intros A B. apply fun_choice_imp_functional_rel_reification, FunChoice. + + now apply fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice. + - intro SetoidFunChoice. repeat split. + + now intros A B; apply setoid_fun_choice_imp_fun_choice. + + apply repr_fun_choice_imp_ext_function_repr. + now apply setoid_fun_choice_imp_repr_fun_choice. + + apply repr_fun_choice_imp_excluded_middle. + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC_fun + Ext_pred_repr + PI *) + +(** Note: all ingredients have a computational meaning when taken in + separation. However, to compute with the functional choice, + existential quantification has to be thought as a strong + existential, which is incompatible with proof-irrelevance which + requires existential quantification to be truncated *) + +Theorem fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice : + FunctionalChoice -> ExtensionalPredicateRepresentative -> ProofIrrelevance -> RepresentativeFunctionalChoice. +Proof. + intros FunChoice PredExtRepr PI A R (Hrefl,Hsym,Htrans). + pose (isclass P := exists x:A, P x). + pose (class := {P:A -> Prop | isclass P}). + pose (contains (c:class) (a:A) := proj1_sig c a). + pose (class_of a := R a). + destruct (FunChoice class A contains) as (f,Hf). + - intros c. apply proj2_sig. + - destruct (PredExtRepr A) as (h,Hh). + assert (Hisclass:forall a, isclass (h (class_of a))). + { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). + rewrite <- Ha; apply Hrefl. } + pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). + exists (fun a => f (f' a)). + intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + + specialize Hf with (f' x). simpl in Hf. rewrite <- Hx in Hf. assumption. + + intros y Hxy. + f_equal. + assert (Heq1: h (class_of x) = h (class_of y)). + { apply Huniqx. intro z. unfold class_of. firstorder. } + assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). + { apply PI. } + unfold f'. + rewrite <- Heq2. + rewrite <- Heq1. + reflexivity. +Qed. + +Theorem setoid_functional_choice_second_characterization : + FunctionalChoice /\ ExtensionalPredicateRepresentative /\ ProofIrrelevance <-> SetoidFunctionalChoice. +Proof. + split. + - intros (FunChoice & ExtPredRepr & PI). + apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + + intros A B. now apply fun_choice_imp_functional_rel_reification. + + now apply fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice. + - intro SetoidFunChoice. repeat split. + + now intros A B; apply setoid_fun_choice_imp_fun_choice. + + apply repr_fun_choice_imp_ext_pred_repr. + now apply setoid_fun_choice_imp_repr_fun_choice. + + red. apply proof_irrelevance_cci. + apply repr_fun_choice_imp_excluded_middle. + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index afd64efdf8..021408a37b 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -34,8 +34,11 @@ Table of contents: 3 3. Independence of general premises and drinker's paradox -4. Classical logic and principle of unrestricted minimization +4. Principles equivalent to classical logic +4.1 Classical logic = principle of unrestricted minimization + +4.2 Classical logic = choice of representatives in a partition of bool *) (************************************************************************) @@ -94,12 +97,14 @@ Qed. (** A weakest form of propositional extensionality: extensionality for provable propositions only *) +Require Import PropExtensionalityFacts. + Definition provable_prop_extensionality := forall A:Prop, A -> A = True. Lemma provable_prop_ext : prop_extensionality -> provable_prop_extensionality. Proof. - intros Ext A Ha; apply Ext; split; trivial. + exact PropExt_imp_ProvPropExt. Qed. (************************************************************************) @@ -516,7 +521,7 @@ End Weak_proof_irrelevance_CCI. (** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with - name KC in {[ChagrovZakharyaschev97]] + name KC in [[ChagrovZakharyaschev97]] [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997. @@ -661,6 +666,8 @@ Proof. exists x0; exact Hnot. Qed. +(** * Axioms equivalent to classical logic *) + (** ** Principle of unrestricted minimization *) Require Import Coq.Arith.PeanoNat. @@ -736,3 +743,56 @@ Section Example_of_undecidable_predicate_with_the_minimization_property. Qed. End Example_of_undecidable_predicate_with_the_minimization_property. + +(** ** Choice of representatives in a partition of bool *) + +(** This is similar to Bell's "weak extensional selection principle" in [[Bell]] + + [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, unpublished. +*) + +Require Import RelationClasses. + +Local Notation representative_boolean_partition := + (forall R:bool->bool->Prop, + Equivalence R -> exists f, forall x, R x (f x) /\ forall y, R x y -> f x = f y). + +Theorem representative_boolean_partition_imp_excluded_middle : + representative_boolean_partition -> excluded_middle. +Proof. + intros ReprFunChoice P. + pose (R (b1 b2 : bool) := b1 = b2 \/ P). + assert (Equivalence R). + { split. + - now left. + - destruct 1. now left. now right. + - destruct 1, 1; try now right. left; now transitivity y. } + destruct (ReprFunChoice R H) as (f,Hf). clear H. + destruct (Bool.bool_dec (f true) (f false)) as [Heq|Hneq]. + + left. + destruct (Hf false) as ([Hfalse|HP],_); try easy. + destruct (Hf true) as ([Htrue|HP],_); try easy. + congruence. + + right. intro HP. + destruct (Hf true) as (_,H). apply Hneq, H. now right. +Qed. + +Theorem excluded_middle_imp_representative_boolean_partition : + excluded_middle -> representative_boolean_partition. +Proof. + intros EM R H. + destruct (EM (R true false)). + - exists (fun _ => true). + intros []; firstorder. + - exists (fun b => b). + intro b. split. + + reflexivity. + + destruct b, y; intros HR; easy || now symmetry in HR. +Qed. + +Theorem excluded_middle_iff_representative_boolean_partition : + excluded_middle <-> representative_boolean_partition. +Proof. + split; auto using excluded_middle_imp_representative_boolean_partition, + representative_boolean_partition_imp_excluded_middle. +Qed. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 23af5afc68..896be7c339 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -8,9 +8,9 @@ (************************************************************************) (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle - in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show + in topoi [[Diaconescu75]]. Lacas and Werner adapted the proof to show that the axiom of choice in equivalence classes entails - Excluded-Middle in Type Theory [LacasWerner99]. + Excluded-Middle in Type Theory [[LacasWerner99]]. Three variants of Diaconescu's result in type theory are shown below. @@ -23,22 +23,22 @@ Benjamin Werner) C. A proof that extensional Hilbert epsilon's description operator - entails excluded-middle (taken from Bell [Bell93]) + entails excluded-middle (taken from Bell [[Bell93]]) - See also [Carlström] for a discussion of the connection between the + See also [[Carlström04]] for a discussion of the connection between the Extensional Axiom of Choice and Excluded-Middle - [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation, + [[Diaconescu75]] Radu Diaconescu, Axiom of Choice and Complementation, in Proceedings of AMS, vol 51, pp 176-178, 1975. - [LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply + [[LacasWerner99]] Samuel Lacas, Benjamin Werner, Which Choices imply the excluded middle?, preprint, 1999. - [Bell93] John L. Bell, Hilbert's epsilon operator and classical + [[Bell93]] John L. Bell, Hilbert's epsilon operator and classical logic, Journal of Philosophical Logic, 22: 1-18, 1993 - [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext, - Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent + to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) (**********************************************************************) @@ -263,7 +263,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (**********************************************************************) (** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *) -(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) +(** Proof sketch from Bell [[Bell93]] (with thanks to P. Castéran) *) Local Notation inhabited A := A (only parsing). diff --git a/theories/Logic/ExtensionalFunctionRepresentative.v b/theories/Logic/ExtensionalFunctionRepresentative.v new file mode 100644 index 0000000000..a9da68e165 --- /dev/null +++ b/theories/Logic/ExtensionalFunctionRepresentative.v @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +(** This module states a limited form axiom of functional + extensionality which selects a canonical representative in each + class of extensional functions *) + +(** Its main interest is that it is the needed ingredient to provide + axiom of choice on setoids (a.k.a. axiom of extensional choice) + when combined with classical logic and axiom of (intensonal) + choice *) + +(** It provides extensionality of functions while still supporting (a + priori) an intensional interpretation of equality *) + +Axiom extensional_function_representative : + forall A B, exists repr, forall (f : A -> B), + (forall x, f x = repr f x) /\ + (forall g, (forall x, f x = g x) -> repr f = repr g). diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 56e03e965c..a10c180ccf 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -360,13 +360,12 @@ Module NoRetractToModalProposition. Section Paradox. Variable M : Prop -> Prop. -Hypothesis unit : forall A:Prop, A -> M A. -Hypothesis join : forall A:Prop, M (M A) -> M A. Hypothesis incr : forall A B:Prop, (A->B) -> M A -> M B. Lemma strength: forall A (P:A->Prop), M(forall x:A,P x) -> forall x:A,M(P x). Proof. - eauto. + intros A P h x. + eapply incr in h; eauto. Qed. (** ** The universe of modal propositions *) @@ -470,7 +469,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem paradox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => ~~P). + exact bool. + exact p2b. @@ -480,8 +479,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End Paradox. @@ -516,7 +513,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem mparadox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => P). + exact bool. + exact p2b. @@ -526,8 +523,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End MParadox. diff --git a/theories/Logic/PropExtensionality.v b/theories/Logic/PropExtensionality.v new file mode 100644 index 0000000000..796c602734 --- /dev/null +++ b/theories/Logic/PropExtensionality.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +(** This module states propositional extensionality and draws + consequences of it *) + +Axiom propositional_extensionality : + forall (P Q : Prop), (P <-> Q) -> P = Q. + +Require Import ClassicalFacts. + +Theorem proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. +Proof. + apply ext_prop_dep_proof_irrel_cic. + exact propositional_extensionality. +Qed. + diff --git a/theories/Logic/PropExtensionalityFacts.v b/theories/Logic/PropExtensionalityFacts.v new file mode 100644 index 0000000000..7e455dfa1e --- /dev/null +++ b/theories/Logic/PropExtensionalityFacts.v @@ -0,0 +1,109 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +(** Some facts and definitions about propositional and predicate extensionality + +We investigate the relations between the following extensionality principles + +- Proposition extensionality +- Predicate extensionality +- Propositional functional extensionality +- Provable-proposition extensionality +- Refutable-proposition extensionality +- Extensional proposition representatives +- Extensional predicate representatives +- Extensional propositional function representatives + +Table of contents + +1. Definitions + +2.1 Predicate extensionality <-> Proposition extensionality + Propositional functional extensionality + +2.2 Propositional extensionality -> Provable propositional extensionality + +2.3 Propositional extensionality -> Refutable propositional extensionality + +*) + +Set Implicit Arguments. + +(**********************************************************************) +(** * Definitions *) + +(** Propositional extensionality *) + +Local Notation PropositionalExtensionality := + (forall A B : Prop, (A <-> B) -> A = B). + +(** Provable-proposition extensionality *) + +Local Notation ProvablePropositionExtensionality := + (forall A:Prop, A -> A = True). + +(** Refutable-proposition extensionality *) + +Local Notation RefutablePropositionExtensionality := + (forall A:Prop, ~A -> A = False). + +(** Predicate extensionality *) + +Local Notation PredicateExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q). + +(** Propositional functional extensionality *) + +Local Notation PropositionalFunctionalExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x = Q x) -> P = Q). + +(**********************************************************************) +(** * Propositional and predicate extensionality *) + +(**********************************************************************) +(** ** Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality *) + +Lemma PredExt_imp_PropExt : PredicateExtensionality -> PropositionalExtensionality. +Proof. + intros Ext A B Equiv. + change A with ((fun _ => A) I). + now rewrite Ext with (P := fun _ : True =>A) (Q := fun _ => B). +Qed. + +Lemma PredExt_imp_PropFunExt : PredicateExtensionality -> PropositionalFunctionalExtensionality. +Proof. + intros Ext A P Q Eq. apply Ext. intros x. now rewrite (Eq x). +Qed. + +Lemma PropExt_and_PropFunExt_imp_PredExt : + PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality. +Proof. + intros Ext FunExt A P Q Equiv. + apply FunExt. intros x. now apply Ext. +Qed. + +Theorem PropExt_and_PropFunExt_iff_PredExt : + PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality. +Proof. + firstorder using PredExt_imp_PropExt, PredExt_imp_PropFunExt, PropExt_and_PropFunExt_imp_PredExt. +Qed. + +(**********************************************************************) +(** ** Propositional extensionality and provable proposition extensionality *) + +Lemma PropExt_imp_ProvPropExt : PropositionalExtensionality -> ProvablePropositionExtensionality. +Proof. + intros Ext A Ha; apply Ext; split; trivial. +Qed. + +(**********************************************************************) +(** ** Propositional extensionality and refutable proposition extensionality *) + +Lemma PropExt_imp_RefutPropExt : PropositionalExtensionality -> RefutablePropositionExtensionality. +Proof. + intros Ext A Ha; apply Ext; split; easy. +Qed. diff --git a/theories/Logic/SetoidChoice.v b/theories/Logic/SetoidChoice.v new file mode 100644 index 0000000000..84432dda1b --- /dev/null +++ b/theories/Logic/SetoidChoice.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +(** This module states the functional form of the axiom of choice over + setoids, commonly called extensional axiom of choice [[Carlström04]], + [[Martin-Löf05]]. This is obtained by a decomposition of the axiom + into the following components: + + - classical logic + - relational axiom of choice + - axiom of unique choice + - a limited form of functional extensionality + + Among other results, it entails: + - proof irrelevance + - choice of a representative in equivalence classes + + [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to + AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + + [[Martin-Löf05] Per Martin-Löf, 100 years of Zermelo’s axiom of + choice: what was the problem with it?, lecture notes for KTH/SU + colloquium, 2005. + +*) + +Require Export ClassicalChoice. (* classical logic, relational choice, unique choice *) +Require Export ExtensionalFunctionRepresentative. + +Require Import ChoiceFacts. +Require Import ClassicalFacts. +Require Import RelationClasses. + +Theorem setoid_choice : + forall A B, + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x x' y, R x x' -> T x y -> T x' y) -> + (forall x, exists y, T x y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). +Proof. + apply setoid_functional_choice_first_characterization. split; [|split]. + - exact choice. + - exact extensional_function_representative. + - exact classic. +Qed. + +Theorem representative_choice : + forall A (R:A->A->Prop), (Equivalence R) -> + exists f : A->A, forall x : A, R x (f x) /\ forall x', R x x' -> f x = f x'. +Proof. + apply setoid_fun_choice_imp_repr_fun_choice. + exact setoid_choice. +Qed. diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget index 323597395f..ef2709b472 100644 --- a/theories/Logic/vo.itarget +++ b/theories/Logic/vo.itarget @@ -20,11 +20,14 @@ WeakFan.vo WKL.vo FunctionalExtensionality.vo ExtensionalityFacts.vo +ExtensionalFunctionRepresentative.vo Hurkens.vo IndefiniteDescription.vo JMeq.vo ProofIrrelevanceFacts.vo ProofIrrelevance.vo +PropExtensionality.vo RelationalChoice.vo SetIsType.vo -FinFun.vo
\ No newline at end of file +SetoidChoice.vo +FinFun.vo diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 7baf102aaa..d6385ee314 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -813,6 +813,34 @@ Proof. rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'. Qed. +Lemma compare_cont_Lt_not_Lt p q : + compare_cont Lt p q <> Lt <-> p > q. +Proof. + rewrite compare_cont_Lt_Lt. + unfold gt, le, compare. + now destruct compare_cont; split; try apply comparison_eq_stable. +Qed. + +Lemma compare_cont_Lt_not_Gt p q : + compare_cont Lt p q <> Gt <-> p <= q. +Proof. + apply not_iff_compat, compare_cont_Lt_Gt. +Qed. + +Lemma compare_cont_Gt_not_Lt p q : + compare_cont Gt p q <> Lt <-> p >= q. +Proof. + apply not_iff_compat, compare_cont_Gt_Lt. +Qed. + +Lemma compare_cont_Gt_not_Gt p q : + compare_cont Gt p q <> Gt <-> p < q. +Proof. + rewrite compare_cont_Gt_Gt. + unfold ge, lt, compare. + now destruct compare_cont; split; try apply comparison_eq_stable. +Qed. + (** We can express recursive equations for [compare] *) Lemma compare_xO_xO p q : (p~0 ?= q~0) = (p ?= q). diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 5aa397f8a9..1e3ab66876 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1367,7 +1367,7 @@ Lemma inj_testbit a n : 0<=n -> Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). Proof. apply Z.testbit_Zpos. Qed. -(** Some results concerning Z.neg *) +(** Some results concerning Z.neg and Z.pos *) Lemma inj_neg p q : Z.neg p = Z.neg q -> p = q. Proof. now injection 1. Qed. @@ -1375,18 +1375,54 @@ Proof. now injection 1. Qed. Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q. Proof. split. apply inj_neg. intros; now f_equal. Qed. +Lemma inj_pos p q : Z.pos p = Z.pos q -> p = q. +Proof. now injection 1. Qed. + +Lemma inj_pos_iff p q : Z.pos p = Z.pos q <-> p = q. +Proof. split. apply inj_pos. intros; now f_equal. Qed. + Lemma neg_is_neg p : Z.neg p < 0. Proof. reflexivity. Qed. Lemma neg_is_nonpos p : Z.neg p <= 0. Proof. easy. Qed. +Lemma pos_is_pos p : 0 < Z.pos p. +Proof. reflexivity. Qed. + +Lemma pos_is_nonneg p : 0 <= Z.pos p. +Proof. easy. Qed. + +Lemma neg_le_pos p q : Zneg p <= Zpos q. +Proof. easy. Qed. + +Lemma neg_lt_pos p q : Zneg p < Zpos q. +Proof. easy. Qed. + +Lemma neg_le_neg p q : (q <= p)%positive -> Zneg p <= Zneg q. +Proof. intros; unfold Z.le; simpl. now rewrite <- Pos.compare_antisym. Qed. + +Lemma neg_lt_neg p q : (q < p)%positive -> Zneg p < Zneg q. +Proof. intros; unfold Z.lt; simpl. now rewrite <- Pos.compare_antisym. Qed. + +Lemma pos_le_pos p q : (p <= q)%positive -> Zpos p <= Zpos q. +Proof. easy. Qed. + +Lemma pos_lt_pos p q : (p < q)%positive -> Zpos p < Zpos q. +Proof. easy. Qed. + Lemma neg_xO p : Z.neg p~0 = 2 * Z.neg p. Proof. reflexivity. Qed. Lemma neg_xI p : Z.neg p~1 = 2 * Z.neg p - 1. Proof. reflexivity. Qed. +Lemma pos_xO p : Z.pos p~0 = 2 * Z.pos p. +Proof. reflexivity. Qed. + +Lemma pos_xI p : Z.pos p~1 = 2 * Z.pos p + 1. +Proof. reflexivity. Qed. + Lemma opp_neg p : - Z.neg p = Z.pos p. Proof. reflexivity. Qed. @@ -1402,6 +1438,9 @@ Proof. reflexivity. Qed. Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p. Proof. reflexivity. Qed. +Lemma add_pos_pos p q : Z.pos p + Z.pos q = Z.pos (p+q). +Proof. reflexivity. Qed. + Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p). Proof. apply Z.divide_Zpos_Zneg_r. Qed. @@ -1412,6 +1451,10 @@ Lemma testbit_neg a n : 0<=n -> Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)). Proof. apply Z.testbit_Zneg. Qed. +Lemma testbit_pos a n : 0<=n -> + Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). +Proof. apply Z.testbit_Zpos. Qed. + End Pos2Z. Module Z2Pos. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 73dee0cf24..18915216a0 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -339,7 +339,7 @@ Notation Zle_0_1 := Z.le_0_1 (compat "8.3"). Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q. Proof. - easy. + exact Pos2Z.neg_le_pos. Qed. Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0. @@ -350,12 +350,12 @@ Qed. (* weaker but useful (in [Z.pow] for instance) *) Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p. Proof. - easy. + exact Pos2Z.pos_is_nonneg. Qed. Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0. Proof. - easy. + exact Pos2Z.neg_is_neg. Qed. Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n. |