From e247c6d0540b9b201a29ea95bdc4df9eeb472a2f Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Fri, 10 Nov 2017 13:28:53 -0500 Subject: Make list functions returning sumbools transparent Specifically Exists_dec, Forall_dec, and Forall_Exists_dec. --- theories/Lists/List.v | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) (limited to 'theories') diff --git a/theories/Lists/List.v b/theories/Lists/List.v index fbf992dbf..eae2c52de 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -2110,13 +2110,13 @@ Section Exists_Forall. {Exists l} + {~ Exists l}. Proof. intro Pdec. induction l as [|a l' Hrec]. - - right. now rewrite Exists_nil. + - right. abstract now rewrite Exists_nil. - destruct Hrec as [Hl'|Hl']. * left. now apply Exists_cons_tl. * destruct (Pdec a) as [Ha|Ha]. + left. now apply Exists_cons_hd. - + right. now inversion_clear 1. - Qed. + + right. abstract now inversion 1. + Defined. Inductive Forall : list A -> Prop := | Forall_nil : Forall nil @@ -2152,9 +2152,9 @@ Section Exists_Forall. - destruct Hrec as [Hl'|Hl']. + destruct (Pdec a) as [Ha|Ha]. * left. now apply Forall_cons. - * right. now inversion_clear 1. - + right. now inversion_clear 1. - Qed. + * right. abstract now inversion 1. + + right. abstract now inversion 1. + Defined. End One_predicate. @@ -2179,6 +2179,16 @@ Section Exists_Forall. * now apply Exists_cons_hd. Qed. + Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) : + (forall x:A, {P x} + { ~ P x }) -> + ~ Forall P l -> + Exists (fun x => ~ P x) l. + Proof. + intro Dec. + apply Exists_Forall_neg; intros. + destruct (Dec x); auto. + Qed. + Lemma Forall_Exists_dec (P:A->Prop) : (forall x:A, {P x} + { ~ P x }) -> forall l:list A, @@ -2186,9 +2196,8 @@ Section Exists_Forall. Proof. intros Pdec l. destruct (Forall_dec P Pdec l); [left|right]; trivial. - apply Exists_Forall_neg; trivial. - intro x. destruct (Pdec x); [now left|now right]. - Qed. + now apply neg_Forall_Exists_neg. + Defined. Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> forall l, Forall P l -> Forall Q l. -- cgit v1.2.3