diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /theories/Logic | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'theories/Logic')
-rw-r--r-- | theories/Logic/ClassicalFacts.v | 78 | ||||
-rw-r--r-- | theories/Logic/Decidable.v | 2 | ||||
-rw-r--r-- | theories/Logic/Eqdep.v | 2 | ||||
-rw-r--r-- | theories/Logic/EqdepFacts.v | 2 | ||||
-rw-r--r-- | theories/Logic/Hurkens.v | 3 | ||||
-rw-r--r-- | theories/Logic/PropFacts.v | 50 |
6 files changed, 133 insertions, 4 deletions
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index c947062a..afd64efd 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -34,6 +34,8 @@ Table of contents: 3 3. Independence of general premises and drinker's paradox +4. Classical logic and principle of unrestricted minimization + *) (************************************************************************) @@ -658,3 +660,79 @@ Proof. exists x; intro; exact Hx. exists x0; exact Hnot. Qed. + +(** ** Principle of unrestricted minimization *) + +Require Import Coq.Arith.PeanoNat. + +Definition Minimal (P:nat -> Prop) (n:nat) : Prop := + P n /\ forall k, P k -> n<=k. + +Definition Minimization_Property (P : nat -> Prop) : Prop := + forall n, P n -> exists m, Minimal P m. + +Section Unrestricted_minimization_entails_excluded_middle. + + Hypothesis unrestricted_minimization: forall P, Minimization_Property P. + + Theorem unrestricted_minimization_entails_excluded_middle : forall A, A\/~A. + Proof. + intros A. + pose (P := fun n:nat => n=0/\A \/ n=1). + assert (P 1) as h. + { unfold P. intuition. } + assert (P 0 <-> A) as p₀. + { split. + + intros [[_ h₀]|[=]]. assumption. + + unfold P. tauto. } + apply unrestricted_minimization in h as ([|[|m]] & hm & hmm). + + intuition. + + right. + intros HA. apply p₀, hmm, PeanoNat.Nat.nle_succ_0 in HA. assumption. + + destruct hm as [([=],_) | [=] ]. + Qed. + +End Unrestricted_minimization_entails_excluded_middle. + +Require Import Wf_nat. + +Section Excluded_middle_entails_unrestricted_minimization. + + Hypothesis em : forall A, A\/~A. + + Theorem excluded_middle_entails_unrestricted_minimization : + forall P, Minimization_Property P. + Proof. + intros P n HPn. + assert (dec : forall n, P n \/ ~ P n) by auto using em. + assert (ex : exists n, P n) by (exists n; assumption). + destruct (dec_inh_nat_subset_has_unique_least_element P dec ex) as (n' & HPn' & _). + exists n'. assumption. + Qed. + +End Excluded_middle_entails_unrestricted_minimization. + +(** However, minimization for a given predicate does not necessarily imply + decidability of this predicate *) + +Section Example_of_undecidable_predicate_with_the_minimization_property. + + Variable s : nat -> bool. + + Let P n := exists k, n<=k /\ s k = true. + + Example undecidable_predicate_with_the_minimization_property : + Minimization_Property P. + Proof. + unfold Minimization_Property. + intros h hn. + exists 0. split. + + unfold P in *. destruct hn as (k&hk₁&hk₂). + exists k. split. + * rewrite <- hk₁. + apply PeanoNat.Nat.le_0_l. + * assumption. + + intros **. apply PeanoNat.Nat.le_0_l. + Qed. + +End Example_of_undecidable_predicate_with_the_minimization_property. diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 2ba7253c..8b6054f9 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -50,7 +50,7 @@ Qed. Theorem dec_iff : forall A B:Prop, decidable A -> decidable B -> decidable (A<->B). Proof. -unfold decidable; tauto. +unfold decidable. tauto. Qed. Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P. diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index f3a2783e..5ef86b8e 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -33,5 +33,5 @@ Export EqdepTheory. (** Exported hints *) -Hint Resolve eq_dep_eq: eqdep v62. +Hint Resolve eq_dep_eq: eqdep. Hint Resolve inj_pair2 inj_pairT2: eqdep. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 30e26c7c..bd59159b 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -164,7 +164,7 @@ Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. Qed. -(** Dependent equality is equivalent tco a dependent pair of equalities *) +(** Dependent equality is equivalent to a dependent pair of equalities *) Set Implicit Arguments. diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 8ded7476..841f843c 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -631,6 +631,8 @@ End NoRetractFromTypeToProp. Module TypeNeqSmallType. +Unset Universe Polymorphism. + Section Paradox. (** ** Universe [U] is equal to one of its elements. *) @@ -655,7 +657,6 @@ Proof. reflexivity. Qed. - Theorem paradox : False. Proof. Generic.paradox p. diff --git a/theories/Logic/PropFacts.v b/theories/Logic/PropFacts.v new file mode 100644 index 00000000..309539e5 --- /dev/null +++ b/theories/Logic/PropFacts.v @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +(** * Basic facts about Prop as a type *) + +(** An intuitionistic theorem from topos theory [[LambekScott]] + +References: + +[[LambekScott]] Jim Lambek, Phil J. Scott, Introduction to higher +order categorical logic, Cambridge Studies in Advanced Mathematics +(Book 7), 1988. + +*) + +Theorem injection_is_involution_in_Prop + (f : Prop -> Prop) + (inj : forall A B, (f A <-> f B) -> (A <-> B)) + (ext : forall A B, A <-> B -> f A <-> f B) + : forall A, f (f A) <-> A. +Proof. +intros. +enough (f (f (f A)) <-> f A) by (apply inj; assumption). +split; intro H. +- now_show (f A). + enough (f A <-> True) by firstorder. + enough (f (f A) <-> f True) by (apply inj; assumption). + split; intro H'. + + now_show (f True). + enough (f (f (f A)) <-> f True) by firstorder. + apply ext; firstorder. + + now_show (f (f A)). + enough (f (f A) <-> True) by firstorder. + apply inj; firstorder. +- now_show (f (f (f A))). + enough (f A <-> f (f (f A))) by firstorder. + apply ext. + split; intro H'. + + now_show (f (f A)). + enough (f A <-> f (f A)) by firstorder. + apply ext; firstorder. + + now_show A. + enough (f A <-> A) by firstorder. + apply inj; firstorder. +Defined. |