From 5e5b2d172123f169b1e3c4d7cddfe82a371c188f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jan 2021 11:21:15 +0100
Subject: [PATCH] add some singleton and snoc lemmas

---
 theories/fin_sets.v | 1 +
 theories/list.v     | 4 ++++
 theories/sets.v     | 4 ++++
 3 files changed, 9 insertions(+)

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index b932ce74..ecca3cff 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -350,6 +350,7 @@ Section map.
   Lemma set_map_union (f : A → B) (X Y : C) :
     set_map (D:=D) f (X ∪ Y) ≡ set_map (D:=D) f X ∪ set_map (D:=D) f Y.
   Proof. set_solver. Qed.
+  (** This cannot be using [=] because list_to_set_singleton does not hold for [=]. *)
   Lemma set_map_singleton (f : A → B) (x : A) :
     set_map (C:=C) (D:=D) f {[x]} ≡ {[f x]}.
   Proof. set_solver. Qed.
diff --git a/theories/list.v b/theories/list.v
index 7b91cdd8..71b761b1 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3442,8 +3442,12 @@ Section fmap.
   Definition fmap_nil : f <$> [] = [] := eq_refl.
   Definition fmap_cons x l : f <$> x :: l = f x :: (f <$> l) := eq_refl.
 
+  Lemma list_fmap_singleton x : f <$> [x] = [f x].
+  Proof. reflexivity. Qed.
   Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
   Proof. by induction l1; f_equal/=. Qed.
+  Lemma fmap_snoc l x : f <$> l ++ [x] = (f <$> l) ++ [f x].
+  Proof. rewrite fmap_app, list_fmap_singleton. done. Qed.
   Lemma fmap_nil_inv k :  f <$> k = [] → k = [].
   Proof. by destruct k. Qed.
   Lemma fmap_cons_inv y l k :
diff --git a/theories/sets.v b/theories/sets.v
index 7b820ee7..7c144f92 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -864,6 +864,10 @@ Section option_and_list_to_set.
   Proof. done. Qed.
   Lemma list_to_set_app l1 l2 : list_to_set (l1 ++ l2) ≡@{C} list_to_set l1 ∪ list_to_set l2.
   Proof. set_solver. Qed.
+  Lemma list_to_set_singleton x : list_to_set [x] ≡@{C} {[ x ]}.
+  Proof. set_solver. Qed.
+  Lemma list_to_set_snoc l x : list_to_set (l ++ [x]) ≡@{C} list_to_set l ∪ {[ x ]}.
+  Proof. set_solver. Qed.
   Global Instance list_to_set_perm : Proper ((≡ₚ) ==> (≡)) (list_to_set (C:=C)).
   Proof. induction 1; set_solver. Qed.
 
-- 
GitLab