Merge branch 'discrete_fun_helpers' into 'master'

Add some helpers for `discrete_fun_singleton`

See merge request iris/iris!1071

CHANGELOG.md

@@ -13,6 +13,8 @@ lemma.
 * Add lemmas `discrete_fun_update` and `discrete_fun_updateP`, which updates an
   abitrary `discrete_fun` to another. For `discrete_fun_updateP`, this requires
   the domain to be finite, similar to `discrete_fun_included_spec`. (by Janggun Lee)
+* Add lemmas `discrete_fun_singleton_valid` and `discrete_fun_singleton_unit`, which simplify 
+  cmra validity and unit used with `discrete_fun_singleton`. (by Janggun Lee)
 
 **Changes in `proofmode`:**
 

iris/algebra/functions.v

@@ -86,6 +86,16 @@ Section cmra.
       rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne //.
     by apply ucmra_unit_validN.
   Qed.
+  Lemma discrete_fun_singleton_valid x (y : B x) : ✓ discrete_fun_singleton x y ↔ ✓ y.
+  Proof.
+    by rewrite !cmra_valid_validN; setoid_rewrite discrete_fun_singleton_validN.
+  Qed.
+
+  Lemma discrete_fun_singleton_unit x : discrete_fun_singleton x (ε : B x) ≡ ε.
+  Proof.
+    move=>x'; destruct (decide (x = x')) as [->|];
+      by rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne.
+  Qed.
 
   Lemma discrete_fun_singleton_core x (y : B x) :
     core (discrete_fun_singleton x y) ≡ discrete_fun_singleton x (core y).