diff options
Diffstat (limited to 'theories/Logic')
-rw-r--r-- | theories/Logic/ClassicalFacts.v | 78 | ||||
-rw-r--r-- | theories/Logic/PropFacts.v | 50 |
2 files changed, 128 insertions, 0 deletions
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 18faacbaf..2ae0ade80 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/PropFacts.v b/theories/Logic/PropFacts.v new file mode 100644 index 000000000..309539e5c --- /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. |