Merge branch 'ralf/algebra-lemmas' into 'master'

various algebra lemmas

See merge request iris/iris!523

theories/algebra/csum.v

@@ -299,6 +299,28 @@ Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
 Global Instance Cinr_id_free b : IdFree b → IdFree (Cinr b).
 Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
 
+(** Interaction with [option] *)
+Lemma Some_csum_includedN x y n :
+  Some x ≼{n} Some y ↔
+    y = CsumBot ∨
+    (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ Some a ≼{n} Some a') ∨
+    (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ Some b ≼{n} Some b').
+Proof.
+  repeat setoid_rewrite Some_includedN. rewrite csum_includedN. split.
+  - intros [Hxy|?]; [inversion Hxy|]; naive_solver.
+  - naive_solver by f_equiv.
+Qed.
+Lemma Some_csum_included x y :
+  Some x ≼ Some y ↔
+    y = CsumBot ∨
+    (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ Some a ≼ Some a') ∨
+    (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ Some b ≼ Some b').
+Proof.
+  repeat setoid_rewrite Some_included. rewrite csum_included. split.
+  - intros [Hxy|?]; [inversion Hxy|]; naive_solver.
+  - naive_solver by f_equiv.
+Qed.
+
 (** Internalized properties *)
 Lemma csum_validI {M} (x : csum A B) :
   ✓ x ⊣⊢@{uPredI M} match x with

theories/algebra/gmap.v

@@ -537,13 +537,23 @@ Proof.
   - by rewrite lookup_insert_ne // !lookup_op lookup_insert_ne.
 Qed.
 
+Lemma singleton_local_update_any m i y x' y' :
+  (∀ x, m !! i = Some x → (x, y) ~l~> (x', y')) →
+  (m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
+Proof.
+  intros. rewrite /singletonM /map_singleton -(insert_insert ∅ i y' y).
+  apply local_update_total_valid0=>_ _ /singleton_includedN_l [x0 [/dist_Some_inv_r Hlk0 _]].
+  edestruct Hlk0 as [x [Hlk _]]; [done..|].
+  eapply insert_local_update; [|eapply lookup_insert|]; eauto.
+Qed.
+
 Lemma singleton_local_update m i x y x' y' :
   m !! i = Some x →
   (x, y) ~l~> (x', y') →
   (m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
 Proof.
-  intros. rewrite /singletonM /map_singleton -(insert_insert ∅ i y' y).
-  by eapply insert_local_update; [|eapply lookup_insert|].
+  intros Hmi ?. apply singleton_local_update_any.
+  intros x2. rewrite Hmi=>[=<-]. done.
 Qed.
 
 Lemma delete_local_update m1 m2 i x `{!Exclusive x} :

theories/algebra/ofe.v

@@ -1041,6 +1041,13 @@ Instance option_mjoin_ne {A : ofeT} n:
   Proper (dist n ==> dist n) (@mjoin option _ A).
 Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
 
+Lemma fmap_Some_dist {A B : ofeT} (f : A → B) (mx : option A) (y : B) n :
+  f <$> mx ≡{n}≡ Some y ↔ ∃ x : A, mx = Some x ∧ y ≡{n}≡ f x.
+Proof.
+  split; [|by intros (x&->&->)].
+  intros (?&?%fmap_Some&?)%dist_Some_inv_r'; naive_solver.
+Qed.
+
 Definition optionO_map {A B} (f : A -n> B) : optionO A -n> optionO B :=
   OfeMor (fmap f : optionO A → optionO B).
 Instance optionO_map_ne A B : NonExpansive (@optionO_map A B).