From 2c0bedd55ceb7c8fc2ec962d522f2d87fc697e2e Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Tue, 25 Jun 2019 16:36:16 +0200 Subject: [PATCH] added two proper instance with permutations --- theories/list.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/theories/list.v b/theories/list.v index ab606e0..c83aa15 100644 --- a/theories/list.v +++ b/theories/list.v @@ -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. -- 2.26.2