diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v index 6aa92d2f9482dd47069a99158b0c9f5cce948a7a..7f7bb44779fd81fbb335fbc53e009798619791c4 100644 --- a/iris/algebra/functions.v +++ b/iris/algebra/functions.v @@ -161,4 +161,22 @@ Section cmra. rewrite !cmra_update_updateP; eauto using discrete_fun_singleton_updateP_empty with subst. Qed. + + Lemma discrete_fun_updateP `{Hfin: Finite A} f P : + (∀ a, f a ~~>: P a) → f ~~>: (λ f', ∀ a, P a (f' a)). + Proof. + rewrite cmra_total_updateP. setoid_rewrite cmra_total_updateP. + intros Hf n z Hfz. + destruct (finite_choice + (λ a y, P a y ∧ ✓{n} (y ⋅ (z a))) + ltac:(naive_solver)) as [f' Hf']. + naive_solver. + Qed. + + Lemma discrete_fun_update f g : + (∀ a, f a ~~> g a) → f ~~> g. + Proof. + rewrite cmra_total_update. setoid_rewrite cmra_total_update. + intros Hfg n zf Hz a. apply (Hfg a), Hz. + Qed. End cmra.