From 88f03cb9e62371ed308f19b56c21b465fbcc6ac4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Jul 2021 19:49:21 +0200
Subject: [PATCH] shorten proofs, tweak lemmas (most of it by Robbert)

---
 theories/list.v | 56 +++++++++++++++++++++----------------------------
 1 file changed, 24 insertions(+), 32 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 27c81376..568cfc86 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2454,6 +2454,15 @@ Proof. red. auto using submseteq_Permutation_length_le, submseteq_length. Qed.
 
 Lemma elem_of_submseteq l k x : x ∈ l → l ⊆+ k → x ∈ k.
 Proof. intros ? [l' ->]%submseteq_Permutation. apply elem_of_app; auto. Qed.
+Lemma lookup_submseteq l k i x :
+  l !! i = Some x →
+  l ⊆+ k →
+  ∃ j, k !! j = Some x.
+Proof.
+  intros Hsub Hlook.
+  eapply elem_of_list_lookup_1, elem_of_submseteq;
+    eauto using elem_of_list_lookup_2.
+Qed.
 
 Lemma submseteq_take l i : take i l ⊆+ l.
 Proof. auto using sublist_take, sublist_submseteq. Qed.
@@ -2581,45 +2590,28 @@ Proof.
 Qed.
 
 Lemma submseteq_insert l1 l2 i j x y :
-  l1 ⊆+ l2 →
   l1 !! i = Some x →
   l2 !! j = Some x →
-  (<[i := y]> l1) ⊆+ (<[j := y]> l2).
-Proof.
-  intros Hsub H1 H2.
-  eapply lookup_lt_Some in H1 as Hlt1.
-  eapply lookup_lt_Some in H2 as Hlt2.
-  eapply take_drop_middle in H1.
-  eapply take_drop_middle in H2.
-  rewrite <-H1, <-H2.
-  rewrite !insert_app_r_alt; [|(rewrite take_length; lia)..].
-  rewrite !take_length.
-  replace (i - i `min` length l1) with 0 by lia.
-  replace (j - j `min` length l2) with 0 by lia. simpl.
-  rewrite <-H1, <-H2 in Hsub. revert Hsub.
-  rewrite !cons_middle.
-  rewrite !(Permutation_app_comm [x]), !(Permutation_app_comm [y]).
-  rewrite !app_assoc.
-  intros ?%submseteq_app_inv_r; by eapply submseteq_skips_r.
-Qed.
-
-Lemma submseteq_lookup l1 l2 i x :
   l1 ⊆+ l2 →
-  l1 !! i = Some x →
-  ∃ j, l2 !! j = Some x.
+  (<[i := y]> l1) ⊆+ (<[j := y]> l2).
 Proof.
-  intros Hsub Hlook.
-  eapply elem_of_list_lookup_1, elem_of_submseteq;
-    eauto using elem_of_list_lookup_2.
+  intros ?? Hsub.
+  rewrite !insert_take_drop,
+    <-!Permutation_middle by eauto using lookup_lt_Some.
+  rewrite <-(take_drop_middle l1 i x), <-(take_drop_middle l2 j x),
+    <-!Permutation_middle in Hsub by done.
+  by apply submseteq_skip, (submseteq_app_inv_l _ _ [x]).
 Qed.
 
-Lemma submseteq_singleton l i x :
-  l !! i = Some x →
-  [x] ⊆+ l.
+Lemma submseteq_singleton l x :
+  [x] ⊆+ l ↔ x ∈ l.
 Proof.
-  intros Hlook.
-  eapply take_drop_middle in Hlook; rewrite <-Hlook.
-  eapply submseteq_cons_middle, submseteq_nil_l.
+  split.
+  - intros Hsub. eapply elem_of_submseteq; [|done].
+    apply elem_of_list_singleton. done.
+  - intros [i Hlook]%elem_of_list_lookup.
+    eapply take_drop_middle in Hlook; rewrite <-Hlook.
+    eapply submseteq_cons_middle, submseteq_nil_l.
 Qed.
 
 Section submseteq_dec.
-- 
GitLab