diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v index 8db35f474dd77facc4a2b8ffabb8eb99ccb6ddc7..7a26344f671cda69e9bb0c87c8abd759d96fa65a 100644 --- a/prelude/fin_collections.v +++ b/prelude/fin_collections.v @@ -254,21 +254,21 @@ Proof. rewrite Forall_forall. by setoid_rewrite elem_of_elements. Qed. Lemma set_Exists_elements P X : set_Exists P X ↔ Exists P (elements X). Proof. rewrite Exists_exists. by setoid_rewrite elem_of_elements. Qed. -Lemma set_Forall_Exists_dec {P Q : A → Prop} (dec : ∀ x, {P x} + {Q x}) X : +Lemma set_Forall_Exists_dec (P Q : A → Prop) (dec : ∀ x, {P x} + {Q x}) X : {set_Forall P X} + {set_Exists Q X}. Proof. - refine (cast_if (Forall_Exists_dec dec (elements X))); + refine (cast_if (Forall_Exists_dec P Q dec (elements X))); [by apply set_Forall_elements|by apply set_Exists_elements]. Defined. Lemma not_set_Forall_Exists P `{dec : ∀ x, Decision (P x)} X : ¬set_Forall P X → set_Exists (not ∘ P) X. -Proof. intro. by destruct (set_Forall_Exists_dec dec X). Qed. +Proof. intro. by destruct (set_Forall_Exists_dec P (not ∘ P) dec X). Qed. Lemma not_set_Exists_Forall P `{dec : ∀ x, Decision (P x)} X : ¬set_Exists P X → set_Forall (not ∘ P) X. Proof. - by destruct (@set_Forall_Exists_dec - (not ∘ P) _ (λ x, swap_if (decide (P x))) X). + by destruct (set_Forall_Exists_dec + (not ∘ P) P (λ x, swap_if (decide (P x))) X). Qed. Global Instance set_Forall_dec (P : A → Prop) `{∀ x, Decision (P x)} X : diff --git a/prelude/list.v b/prelude/list.v index c8af713f336f94f9896f192378695f4999573466..8afbbf8a889292c66f14fc551c6fd7071981eca2 100644 --- a/prelude/list.v +++ b/prelude/list.v @@ -2051,7 +2051,7 @@ Lemma list_subseteq_nil l : [] ⊆ l. Proof. intros x. by rewrite elem_of_nil. Qed. (** ** Properties of the [Forall] and [Exists] predicate *) -Lemma Forall_Exists_dec {P Q : A → Prop} (dec : ∀ x, {P x} + {Q x}) : +Lemma Forall_Exists_dec (P Q : A → Prop) (dec : ∀ x, {P x} + {Q x}) : ∀ l, {Forall P l} + {Exists Q l}. Proof. refine ( @@ -2232,21 +2232,19 @@ Section Forall_Exists. Context {dec : ∀ x, Decision (P x)}. Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l. - Proof. intro. destruct (Forall_Exists_dec dec l); intuition. Qed. + Proof. intro. by destruct (Forall_Exists_dec P (not ∘ P) dec l). Qed. Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l. Proof. - (* TODO: Coq 8.6 needs type annotation here, Coq 8.5 did not. - Should we report this? *) - by destruct (@Forall_Exists_dec (not ∘ P) _ + by destruct (Forall_Exists_dec (not ∘ P) P (λ x : A, swap_if (decide (P x))) l). Qed. Global Instance Forall_dec l : Decision (Forall P l) := - match Forall_Exists_dec dec l with + match Forall_Exists_dec P (not ∘ P) dec l with | left H => left H | right H => right (Exists_not_Forall _ H) end. Global Instance Exists_dec l : Decision (Exists P l) := - match Forall_Exists_dec (λ x, swap_if (decide (P x))) l with + match Forall_Exists_dec (not ∘ P) P (λ x, swap_if (decide (P x))) l with | left H => right (Forall_not_Exists _ H) | right H => left H end.