From 59ff9eae72c7286df459c9e7a9e5e17f3d19ea72 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Jan 2023 15:49:19 +0100
Subject: [PATCH] miscellaneous map lemmas

---
 stdpp/fin_map_dom.v |  7 +++++
 stdpp/fin_maps.v    | 68 ++++++++++++++++++++++++++++++++++++++++++---
 2 files changed, 71 insertions(+), 4 deletions(-)

diff --git a/stdpp/fin_map_dom.v b/stdpp/fin_map_dom.v
index b956dce9..65d2f289 100644
--- a/stdpp/fin_map_dom.v
+++ b/stdpp/fin_map_dom.v
@@ -187,6 +187,13 @@ Proof.
   unfold size, map_size. rewrite fmap_length. done.
 Qed.
 
+Lemma map_eq_dom `{!Elements K D, !FinSet K D} {A} (m m' : M A) :
+  dom m ≡@{D} dom m' → m' ⊆ m → m = m'.
+Proof.
+  intros Hdom. apply map_eq_size.
+  rewrite <-!size_dom. rewrite Hdom. done.
+Qed.
+
 Lemma dom_singleton_inv {A} (m : M A) i :
   dom m ≡@{D} {[i]} → ∃ x, m = {[i := x]}.
 Proof.
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 2f3ed7b4..739bb251 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1094,6 +1094,9 @@ Lemma map_imap_empty {A B} (f : K → A → option B) :
 Proof. unfold map_imap. by rewrite map_to_list_empty. Qed.
 
 (** ** Properties of the size operation *)
+Lemma map_size_length {A} (m : M A) :
+  size m = length (map_to_list m).
+Proof. reflexivity. Qed.
 Lemma map_size_empty {A} : size (∅ : M A) = 0.
 Proof. unfold size, map_size. by rewrite map_to_list_empty. Qed.
 Lemma map_size_empty_iff {A} (m : M A) : size m = 0 ↔ m = ∅.
@@ -1108,6 +1111,22 @@ Proof. by rewrite map_size_empty_iff. Qed.
 Lemma map_size_singleton {A} i (x : A) : size ({[ i := x ]} : M A) = 1.
 Proof. unfold size, map_size. by rewrite map_to_list_singleton. Qed.
 
+Lemma map_size_lookup_nonzero {A} i (m : M A) :
+  is_Some (m !! i) → 0 < size m.
+Proof.
+  intros Hi. cut (size m ≠ 0). 1:lia.
+  apply map_size_non_empty_iff. intros Hemp. rewrite Hemp, lookup_empty in Hi.
+  destruct Hi as [??]. done.
+Qed.
+Lemma map_size_nonzero_lookup {A} (m : M A) :
+  0 < size m → ∃ i, is_Some (m !! i).
+Proof.
+  intros Hsz.
+  assert (is_Some (head (map_to_list m))) as [[i x] EQ].
+  { apply head_is_Some. rewrite <-length_zero_iff_nil, <-map_size_length. lia. }
+  exists i, x. apply elem_of_map_to_list, head_Some_elem_of. done.
+Qed.
+
 Lemma map_size_insert {A} i x (m : M A) :
   size (<[i:=x]> m) = (match m !! i with Some _ => id | None => S end) (size m).
 Proof.
@@ -1150,6 +1169,24 @@ Proof.
   eauto with f_equal.
 Qed.
 
+Lemma map_eq_size {A} (m m' : M A) :
+  size m = size m' → m' ⊆ m → m = m'.
+Proof.
+  intros Hsz. remember (size m) as n eqn:Hn.
+  revert m m' Hn Hsz. induction n as [|n IH]; intros m m' Hn Hsz.
+  { intros _. rewrite map_size_empty_inv by done. rewrite (map_size_empty_inv m) by done. done. }
+  intros Hsub.
+  destruct (map_size_nonzero_lookup m') as [i [x Hix']]. 1:lia.
+  assert (m !! i = Some x) as Hix.
+  { by eapply lookup_weaken. }
+  rewrite <-(insert_delete m i x) by done.
+  rewrite <-(insert_delete m' i x) by done.
+  f_equal. apply IH.
+  - rewrite map_size_delete_Some by eauto. lia.
+  - rewrite map_size_delete_Some by eauto. lia.
+  - apply delete_mono. done.
+Qed.
+
 (** ** Properties of conversion from sets *)
 Section set_to_map.
   Context {A : Type} `{FinSet B C}.
@@ -1216,9 +1253,11 @@ Proof.
   - by apply not_elem_of_list_to_map_1.
   - apply IH; auto using map_to_list_to_map.
 Qed.
-Lemma map_to_list_length {A} (m1 m2 : M A) :
-  m1 ⊂ m2 → length (map_to_list m1) < length (map_to_list m2).
+
+Lemma map_subset_size {A} (m1 m2 : M A) :
+  m1 ⊂ m2 → size m1 < size m2.
 Proof.
+  rewrite !map_size_length.
   revert m2. induction m1 as [|i x m ? IH] using map_ind.
   { intros m2 Hm2. rewrite map_to_list_empty. simpl.
     apply Nat.neq_0_lt_0, Nat.neq_sym. intros Hlen. symmetry in Hlen.
@@ -1230,11 +1269,27 @@ Proof.
 Qed.
 Lemma map_wf {A} : wf (⊂@{M A}).
 Proof.
-  apply (wf_projected (<) (length ∘ map_to_list)).
-  - by apply map_to_list_length.
+  apply (wf_projected (<) size).
+  - by apply map_subset_size.
   - by apply lt_wf.
 Qed.
 
+Lemma map_subseteq_size {A} (m1 m2 : M A) :
+  m1 ⊆ m2 → size m1 ≤ size m2.
+Proof.
+  revert m2. induction m1 as [|i x m Hfresh IH] using map_ind.
+  { rewrite map_size_empty. lia. }
+  intros m2 Hm2.
+  rewrite map_size_insert_None by done.
+  assert (m2 !! i = Some x).
+  { eapply lookup_weaken. 2:done. rewrite lookup_insert. done. }
+  rewrite <-(insert_delete m2 i x) by done.
+  rewrite map_size_insert_None.
+  2:{ rewrite lookup_delete. done. }
+  apply le_n_S. apply IH.
+  eapply insert_delete_subseteq; done.
+Qed.
+
 (** ** The fold operation *)
 Lemma map_fold_empty {A B} (f : K → A → B → B) (b : B) :
   map_fold f b ∅ = b.
@@ -1691,6 +1746,11 @@ Section map_filter.
     rewrite map_subseteq_spec. intros Hm1m2.
     apply map_filter_strong_subseteq_ext. naive_solver.
   Qed.
+
+  Lemma map_size_filter m :
+    size (filter P m) ≤ size m.
+  Proof. apply map_subseteq_size. apply map_filter_subseteq. Qed.
+
 End map_filter.
 
 Lemma map_filter_comm {A}
-- 
GitLab