Commit 546ed060 authored by Robbert Krebbers's avatar Robbert Krebbers

Make some arguments explicit that could not be infered.

parent b81fb420
Pipeline #3044 passed with stage
in 10 minutes and 23 seconds
......@@ -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 :
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment