Commit 2c0bedd5 authored by Michael Sammler's avatar Michael Sammler

added two proper instance with permutations

parent 9407e8cc
......@@ -2245,6 +2245,9 @@ Proof. split; firstorder. Qed.
Lemma list_subseteq_nil l : [] l.
Proof. intros x. by rewrite elem_of_nil. Qed.
Global Instance list_subseteq_Permutation: Proper ((≡ₚ) ==> (≡ₚ) ==> ()) (@{list A}) .
Proof. intros l1 l2 Hl k1 k2 Hk. apply forall_proper; intros x. by rewrite Hl, Hk. Qed.
(** ** Properties of the [Forall] and [Exists] predicate *)
Lemma Forall_Exists_dec (P Q : A Prop) (dec : x, {P x} + {Q x}) :
l, {Forall P l} + {Exists Q l}.
......@@ -2400,6 +2403,10 @@ Section Forall_Exists.
intros ?? l. induction l using rev_ind; auto.
rewrite Forall_app, Forall_singleton; intros [??]; auto.
Qed.
Global Instance Forall_Permutation: Proper ((≡ₚ) ==> ()) (Forall P).
Proof. intros l1 l2 Hl. rewrite !Forall_forall. by setoid_rewrite Hl. Qed.
Lemma Exists_exists l : Exists P l x, x l P x.
Proof.
split.
......@@ -2419,6 +2426,9 @@ Section Forall_Exists.
Exists P l ( x, P x Q x) Exists Q l.
Proof. intros H ?. induction H; auto. Defined.
Global Instance Exists_Permutation: Proper ((≡ₚ) ==> ()) (Exists P).
Proof. intros l1 l2 Hl. rewrite !Exists_exists. by setoid_rewrite Hl. Qed.
Lemma Exists_not_Forall l : Exists (not P) l ¬Forall P l.
Proof. induction 1; inversion_clear 1; contradiction. Qed.
Lemma Forall_not_Exists l : Forall (not P) l ¬Exists P l.
......
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