diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Compat/Coq85.v | 7 | ||||
| -rw-r--r-- | theories/Init/Datatypes.v | 2 | ||||
| -rw-r--r-- | theories/Lists/List.v | 76 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 109 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 78 | ||||
| -rw-r--r-- | theories/Logic/PropFacts.v | 50 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 2 |
7 files changed, 319 insertions, 5 deletions
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 1622f2aed..7ce04a662 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -7,3 +7,10 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.5 *) + +(* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not + behave as "intros [H|H]" but leave instead hypotheses quantified in + the goal, here producing subgoals A->C and B->C. *) + +Unset Bracketing Last Introduction Pattern. + diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index de615301d..aaffc0978 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -151,6 +151,7 @@ Inductive option (A:Type) : Type := | Some : A -> option A | None : option A. +Arguments Some {A} a. Arguments None {A}. Definition option_map (A B:Type) (f:A->B) (o : option A) : option B := @@ -225,6 +226,7 @@ Inductive list (A : Type) : Type := | cons : A -> list A -> list A. Arguments nil {A}. +Arguments cons {A} a l. Infix "::" := cons (at level 60, right associativity) : list_scope. Delimit Scope list_scope with list. Bind Scope list_scope with list. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index fe18686e2..45306caf0 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -7,7 +7,7 @@ (************************************************************************) Require Setoid. -Require Import PeanoNat Le Gt Minus Bool. +Require Import PeanoNat Le Gt Minus Bool Lt. Set Implicit Arguments. (* Set Universe Polymorphism. *) @@ -1633,6 +1633,80 @@ Section Cutting. end end. + Lemma firstn_nil n: firstn n [] = []. + Proof. induction n; now simpl. Qed. + + Lemma firstn_cons n a l: firstn (S n) (a::l) = a :: (firstn n l). + Proof. now simpl. Qed. + + Lemma firstn_all l: firstn (length l) l = l. + Proof. induction l as [| ? ? H]; simpl; [reflexivity | now rewrite H]. Qed. + + Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l. + Proof. induction n as [|k iHk]. + - intro. inversion 1 as [H1|?]. + rewrite (length_zero_iff_nil l) in H1. subst. now simpl. + - destruct l as [|x xs]; simpl. + * now reflexivity. + * simpl. intro H. apply Peano.le_S_n in H. f_equal. apply iHk, H. + Qed. + + Lemma firstn_O l: firstn 0 l = []. + Proof. now simpl. Qed. + + Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n. + Proof. + induction n as [|k iHk]; simpl; [auto | destruct l as [|x xs]; simpl]. + - auto with arith. + - apply Peano.le_n_S, iHk. + Qed. + + Lemma firstn_length_le: forall l:list A, forall n:nat, + n <= length l -> length (firstn n l) = n. + Proof. induction l as [|x xs Hrec]. + - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. + - destruct n. + * now simpl. + * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). + Qed. + + Lemma firstn_app n: + forall l1 l2, + firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2). + Proof. induction n as [|k iHk]; intros l1 l2. + - now simpl. + - destruct l1 as [|x xs]. + * unfold firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O. + * rewrite <- app_comm_cons. simpl. f_equal. apply iHk. + Qed. + + Lemma firstn_app_2 n: + forall l1 l2, + firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2. + Proof. induction n as [| k iHk];intros l1 l2. + - unfold firstn at 2. rewrite <- plus_n_O, app_nil_r. + rewrite firstn_app. rewrite <- minus_diag_reverse. + unfold firstn at 2. rewrite app_nil_r. apply firstn_all. + - destruct l2 as [|x xs]. + * simpl. rewrite app_nil_r. apply firstn_all2. auto with arith. + * rewrite firstn_app. assert (H0 : (length l1 + S k - length l1) = S k). + auto with arith. + rewrite H0, firstn_all2; [reflexivity | auto with arith]. + Qed. + + Lemma firstn_firstn: + forall l:list A, + forall i j : nat, + firstn i (firstn j l) = firstn (min i j) l. + Proof. induction l as [|x xs Hl]. + - intros. simpl. now rewrite ?firstn_nil. + - destruct i. + * intro. now simpl. + * destruct j. + + now simpl. + + simpl. f_equal. apply Hl. + Qed. + Fixpoint skipn (n:nat)(l:list A) : list A := match n with | 0 => l diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 0a0bf0dea..c8ed95cd4 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -48,7 +48,11 @@ Section first_definitions. end end. - (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *) + (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing. + Invariant: any element should occur at most once in [x], see for + instance [set_add]. We hence remove here only the first occurrence + of [a] in [x]. *) + Fixpoint set_remove (a:A) (x:set) : set := match x with | nil => empty_set @@ -227,6 +231,68 @@ Section first_definitions. intros; elim (Aeq_dec a a0); intros; discriminate. Qed. + Lemma set_add_iff a b l : In a (set_add b l) <-> a = b \/ In a l. + Proof. + split. apply set_add_elim. apply set_add_intro. + Qed. + + Lemma set_add_nodup a l : NoDup l -> NoDup (set_add a l). + Proof. + induction 1 as [|x l H H' IH]; simpl. + - constructor; [ tauto | constructor ]. + - destruct (Aeq_dec a x) as [<-|Hax]; constructor; trivial. + rewrite set_add_iff. intuition. + Qed. + + Lemma set_remove_1 (a b : A) (l : set) : + In a (set_remove b l) -> In a l. + Proof. + induction l as [|x xs Hrec]. + - intros. auto. + - simpl. destruct (Aeq_dec b x). + * tauto. + * intro H. destruct H. + + rewrite H. apply in_eq. + + apply in_cons. apply Hrec. assumption. + Qed. + + Lemma set_remove_2 (a b:A) (l : set) : + NoDup l -> In a (set_remove b l) -> a <> b. + Proof. + induction l as [|x l IH]; intro ND; simpl. + - tauto. + - inversion_clear ND. + destruct (Aeq_dec b x) as [<-|Hbx]. + + congruence. + + destruct 1; subst; auto. + Qed. + + Lemma set_remove_3 (a b : A) (l : set) : + In a l -> a <> b -> In a (set_remove b l). + Proof. + induction l as [|x xs Hrec]. + - now simpl. + - simpl. destruct (Aeq_dec b x) as [<-|Hbx]; simpl; intuition. + congruence. + Qed. + + Lemma set_remove_iff (a b : A) (l : set) : + NoDup l -> (In a (set_remove b l) <-> In a l /\ a <> b). + Proof. + split; try split. + - eapply set_remove_1; eauto. + - eapply set_remove_2; eauto. + - destruct 1; apply set_remove_3; auto. + Qed. + + Lemma set_remove_nodup a l : NoDup l -> NoDup (set_remove a l). + Proof. + induction 1 as [|x l H H' IH]; simpl. + - constructor. + - destruct (Aeq_dec a x) as [<-|Hax]; trivial. + constructor; trivial. + rewrite set_remove_iff; trivial. intuition. + Qed. Lemma set_union_intro1 : forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y). @@ -264,18 +330,26 @@ Section first_definitions. tauto. Qed. + Lemma set_union_iff a l l': In a (set_union l l') <-> In a l \/ In a l'. + Proof. + split. apply set_union_elim. apply set_union_intro. + Qed. + + Lemma set_union_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_union l l'). + Proof. + induction 2 as [|x' l' ? ? IH]; simpl; trivial. now apply set_add_nodup. + Qed. + Lemma set_union_emptyL : forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x. intros a x H; case (set_union_elim _ _ _ H); auto || contradiction. Qed. - Lemma set_union_emptyR : forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x. intros a x H; case (set_union_elim _ _ _ H); auto || contradiction. Qed. - Lemma set_inter_intro : forall (a:A) (x y:set), set_In a x -> set_In a y -> set_In a (set_inter x y). @@ -326,6 +400,21 @@ Section first_definitions. eauto with datatypes. Qed. + Lemma set_inter_iff a l l' : In a (set_inter l l') <-> In a l /\ In a l'. + Proof. + split. + - apply set_inter_elim. + - destruct 1. now apply set_inter_intro. + Qed. + + Lemma set_inter_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_inter l l'). + Proof. + induction 1 as [|x l H H' IH]; intro Hl'; simpl. + - constructor. + - destruct (set_mem x l'); auto. + constructor; auto. rewrite set_inter_iff; tauto. + Qed. + Lemma set_diff_intro : forall (a:A) (x y:set), set_In a x -> ~ set_In a y -> set_In a (set_diff x y). @@ -360,6 +449,20 @@ Section first_definitions. rewrite H; trivial. Qed. + Lemma set_diff_iff a l l' : In a (set_diff l l') <-> In a l /\ ~In a l'. + Proof. + split. + - split; [eapply set_diff_elim1 | eapply set_diff_elim2]; eauto. + - destruct 1. now apply set_diff_intro. + Qed. + + Lemma set_diff_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_diff l l'). + Proof. + induction 1 as [|x l H H' IH]; intro Hl'; simpl. + - constructor. + - destruct (set_mem x l'); auto using set_add_nodup. + Qed. + Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x). red; intros a x H. apply (set_diff_elim2 _ _ _ H). diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index cdc3e0461..d4ebfb42f 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. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index d89919b0a..6e5919b34 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -89,7 +89,7 @@ Section Measure_well_founded. Lemma measure_wf: well_founded MR. Proof with auto. unfold well_founded. - cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a). + cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0). intros. apply (H (m a))... apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). |