From 47cfb44c35297eadd06c4bb4fae47e0d914d5f4a Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen Date: Wed, 12 Jan 2022 14:43:57 +0100 Subject: [PATCH 1/4] Added some lemmas about [sublist] --- theories/list.v | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/theories/list.v b/theories/list.v index b78ba495..6dcedb4e 100644 --- a/theories/list.v +++ b/theories/list.v @@ -987,6 +987,16 @@ Proof. intros; eapply elem_of_list_lookup_2. destruct (nth_lookup_or_length l i d); [done | by lia]. Qed. +Lemma elem_of_list_delete x i l : + x ∈ delete i l → x ∈ l. +Proof. + revert i. + induction l as [|z l IHl]; [done|]; intros i Hin. + destruct i as [|i]; [by right|]. + apply elem_of_cons in Hin. + destruct Hin as [-> | Hin]; [by left|]. + right. by eapply IHl. +Qed. Lemma not_elem_of_app_cons_inv_l x y l1 l2 k1 k2 : x ∉ k1 → y ∉ l1 → @@ -2418,6 +2428,21 @@ Proof. auto using sublist_inserts_l, sublist_skip. - intros (?&?&?&?&?); subst. auto using sublist_app. Qed. +Lemma sublist_list_split l1 l2 l x : + l1 ++ x :: l2 `sublist_of` l → + ∃ l1' l2', l = l1' ++ x :: l2' ∧ l1 `sublist_of` l1' ∧ l2 `sublist_of` l2'. +Proof. + intros Hl. + apply sublist_app_l in Hl. + destruct Hl as (k1&k2&->&Hle1&Hle2). + apply sublist_cons_l in Hle2. + destruct Hle2 as (k1'&k2'&->&Hle3). + exists (k1++k1'), k2'. + split; [by rewrite app_assoc|]. split; [|done]. + apply sublist_app_r. + exists l1, []. + split; [by rewrite app_nil_r|]. split; [done|apply sublist_nil_l]. +Qed. Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist_of` k ++ l2 → l1 `sublist_of` l2. Proof. induction k as [|y k IH]; simpl; [done |]. @@ -2473,6 +2498,21 @@ Proof. - destruct (IH k) as [is His]. exists (is ++ [length k]). rewrite fold_right_app. simpl. by rewrite delete_middle. Qed. +Lemma elem_of_sublist x l1 l2 : + x ∈ l1 → l1 `sublist_of` l2 → x ∈ l2. +Proof. + intros Hin Hle%sublist_alt. + destruct Hle as [l' ->]. + induction l' as [|y l' IHl']; [done|]. + by eapply IHl', elem_of_list_delete. +Qed. +Lemma sublist_filter P `{! ∀ x : A, Decision (P x)} l : + filter P l `sublist_of` l. +Proof. + induction l as [|x l IHl]; [done|]. + rewrite filter_cons. + by destruct (decide (P x)); [apply sublist_skip|apply sublist_cons]. +Qed. Lemma Permutation_sublist l1 l2 l3 : l1 ≡ₚ l2 → l2 `sublist_of` l3 → ∃ l4, l1 `sublist_of` l4 ∧ l4 ≡ₚ l3. Proof. -- GitLab From f5e219af04cebe3b3d110790cef72ae398bb2fc3 Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen Date: Wed, 19 Jan 2022 12:40:49 +0100 Subject: [PATCH 2/4] Cleaned up and renamed lemmas --- theories/list.v | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/theories/list.v b/theories/list.v index 6dcedb4e..d204da78 100644 --- a/theories/list.v +++ b/theories/list.v @@ -990,12 +990,9 @@ Qed. Lemma elem_of_list_delete x i l : x ∈ delete i l → x ∈ l. Proof. - revert i. - induction l as [|z l IHl]; [done|]; intros i Hin. - destruct i as [|i]; [by right|]. - apply elem_of_cons in Hin. - destruct Hin as [-> | Hin]; [by left|]. - right. by eapply IHl. + revert i. induction l as [|z l IHl]; [done|]; intros i Hin. + destruct i as [|i]; [by right|]. apply elem_of_cons in Hin. + destruct Hin as [-> | Hin]; [by left|]. right. by eapply IHl. Qed. Lemma not_elem_of_app_cons_inv_l x y l1 l2 k1 k2 : @@ -2428,7 +2425,7 @@ Proof. auto using sublist_inserts_l, sublist_skip. - intros (?&?&?&?&?); subst. auto using sublist_app. Qed. -Lemma sublist_list_split l1 l2 l x : +Lemma sublist_app_cons_inv l1 l2 l x : l1 ++ x :: l2 `sublist_of` l → ∃ l1' l2', l = l1' ++ x :: l2' ∧ l1 `sublist_of` l1' ∧ l2 `sublist_of` l2'. Proof. @@ -2439,8 +2436,7 @@ Proof. destruct Hle2 as (k1'&k2'&->&Hle3). exists (k1++k1'), k2'. split; [by rewrite app_assoc|]. split; [|done]. - apply sublist_app_r. - exists l1, []. + apply sublist_app_r. exists l1, []. split; [by rewrite app_nil_r|]. split; [done|apply sublist_nil_l]. Qed. Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist_of` k ++ l2 → l1 `sublist_of` l2. @@ -2501,10 +2497,8 @@ Qed. Lemma elem_of_sublist x l1 l2 : x ∈ l1 → l1 `sublist_of` l2 → x ∈ l2. Proof. - intros Hin Hle%sublist_alt. - destruct Hle as [l' ->]. - induction l' as [|y l' IHl']; [done|]. - by eapply IHl', elem_of_list_delete. + intros Hin Hle%sublist_alt. destruct Hle as [l' ->]. + induction l' as [|y l' IHl']; [done|]. by eapply IHl', elem_of_list_delete. Qed. Lemma sublist_filter P `{! ∀ x : A, Decision (P x)} l : filter P l `sublist_of` l. -- GitLab From 300c1b8492d023d248d66317c38c706632c471ba Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen Date: Mon, 29 Aug 2022 14:06:58 +0200 Subject: [PATCH 3/4] Resolved some review feedback --- theories/list.v | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/theories/list.v b/theories/list.v index d204da78..85faa72b 100644 --- a/theories/list.v +++ b/theories/list.v @@ -2430,10 +2430,8 @@ Lemma sublist_app_cons_inv l1 l2 l x : ∃ l1' l2', l = l1' ++ x :: l2' ∧ l1 `sublist_of` l1' ∧ l2 `sublist_of` l2'. Proof. intros Hl. - apply sublist_app_l in Hl. - destruct Hl as (k1&k2&->&Hle1&Hle2). - apply sublist_cons_l in Hle2. - destruct Hle2 as (k1'&k2'&->&Hle3). + apply sublist_app_l in Hl as (k1&k2&->&Hle1&Hle2). + apply sublist_cons_l in Hle2 as (k1'&k2'&->&Hle3). exists (k1++k1'), k2'. split; [by rewrite app_assoc|]. split; [|done]. apply sublist_app_r. exists l1, []. @@ -2494,19 +2492,24 @@ Proof. - destruct (IH k) as [is His]. exists (is ++ [length k]). rewrite fold_right_app. simpl. by rewrite delete_middle. Qed. -Lemma elem_of_sublist x l1 l2 : - x ∈ l1 → l1 `sublist_of` l2 → x ∈ l2. +Lemma sublist_le l1 l2 : + l1 `sublist_of` l2 → l1 ⊆ l2. Proof. - intros Hin Hle%sublist_alt. destruct Hle as [l' ->]. + intros Hle%sublist_alt x Hin. destruct Hle as [l' ->]. induction l' as [|y l' IHl']; [done|]. by eapply IHl', elem_of_list_delete. Qed. -Lemma sublist_filter P `{! ∀ x : A, Decision (P x)} l : +Lemma elem_of_sublist x l1 l2 : + x ∈ l1 → l1 `sublist_of` l2 → x ∈ l2. +Proof. intros Hin Hle. by apply (sublist_le l1 l2 Hle). Qed. +Lemma filter_sublist P `{! ∀ x : A, Decision (P x)} l : filter P l `sublist_of` l. Proof. - induction l as [|x l IHl]; [done|]. - rewrite filter_cons. + induction l as [|x l IHl]; [done|]. rewrite filter_cons. by destruct (decide (P x)); [apply sublist_skip|apply sublist_cons]. Qed. +Lemma list_filter_subseteq P `{! ∀ x : A, Decision (P x)} l : + filter P l ⊆ l. +Proof. apply sublist_le, filter_sublist. Qed. Lemma Permutation_sublist l1 l2 l3 : l1 ≡ₚ l2 → l2 `sublist_of` l3 → ∃ l4, l1 `sublist_of` l4 ∧ l4 ≡ₚ l3. Proof. -- GitLab From 4575401f83d004daabe68b0e6819c2e1f412edc8 Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen Date: Mon, 29 Aug 2022 15:25:29 +0200 Subject: [PATCH 4/4] Resolved duplicate lemma --- theories/list.v | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/theories/list.v b/theories/list.v index 85faa72b..965096f5 100644 --- a/theories/list.v +++ b/theories/list.v @@ -2507,9 +2507,6 @@ Proof. induction l as [|x l IHl]; [done|]. rewrite filter_cons. by destruct (decide (P x)); [apply sublist_skip|apply sublist_cons]. Qed. -Lemma list_filter_subseteq P `{! ∀ x : A, Decision (P x)} l : - filter P l ⊆ l. -Proof. apply sublist_le, filter_sublist. Qed. Lemma Permutation_sublist l1 l2 l3 : l1 ≡ₚ l2 → l2 `sublist_of` l3 → ∃ l4, l1 `sublist_of` l4 ∧ l4 ≡ₚ l3. Proof. @@ -2854,11 +2851,7 @@ Proof. Qed. Lemma list_filter_subseteq P `{!∀ x : A, Decision (P x)} l : filter P l ⊆ l. -Proof. - induction l as [|x l IHl]; [done|]. rewrite filter_cons. - destruct (decide (P x)); - [by apply list_subseteq_skip|by apply list_subseteq_cons]. -Qed. +Proof. apply sublist_le, filter_sublist. 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. -- GitLab