Merge branch 'discrete_fun_update' into 'master'

Add `discrete_fun_update{P}`.

See merge request iris/iris!1070

CHANGELOG.md

@@ -10,6 +10,9 @@ lemma.
 * Add lemmas `big_opS_gset_to_gmap` and `big_opS_gset_to_gmap_L`, which rewrite
   between `gset_to_gmap` and big set ops of singleton maps.  (by Isaac van
   Bakel)
+* 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)
 
 **Changes in `proofmode`:**
 

iris/algebra/functions.v

@@ -161,4 +161,23 @@ Section cmra.
     rewrite !cmra_update_updateP;
       eauto using discrete_fun_singleton_updateP_empty with subst.
   Qed.
+
+  Lemma discrete_fun_updateP `{!Finite A} f P Q :
+    (∀ a, f a ~~>: P a) → (∀ f', (∀ a, P a (f' a)) → Q f') → f ~~>: Q.
+  Proof.
+    repeat setoid_rewrite cmra_total_updateP. intros Hf HP n h Hh.
+    destruct (finite_choice
+      (λ a y, P a y ∧ ✓{n} (y ⋅ (h a)))) as [f' Hf']; first naive_solver.
+    naive_solver.
+  Qed.
+  Lemma discrete_fun_updateP' `{!Finite A} f P :
+    (∀ a, f a ~~>: P a) → f ~~>: λ f', ∀ a, P a (f' a).
+  Proof. eauto using discrete_fun_updateP. Qed.
+
+  Lemma discrete_fun_update f g :
+    (∀ a, f a ~~> g a) → f ~~> g.
+  Proof.
+    repeat setoid_rewrite cmra_total_update.
+    intros Hfg n h Hh a. apply (Hfg a), Hh.
+  Qed.
 End cmra.