diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 10:02:43 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 10:02:43 +0100 |
| commit | 2168c75c6bcf787ee532c7773f90e09d99c793fc (patch) | |
| tree | d18ecd59224e169582e4ffe7f57f70b6679af0ac /theories | |
| parent | ec5d9779c0dc3579866c375a52e5df51cf5fffd7 (diff) | |
| parent | e247c6d0540b9b201a29ea95bdc4df9eeb472a2f (diff) | |
Merge PR #6139: Make list functions returning sumbools transparent
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Lists/List.v | 27 |
1 files changed, 18 insertions, 9 deletions
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. |