Merge branch 'ralf/update' into 'master'

provide a lemma to update only the authoritative part, ignoring the fragments entirely

See merge request iris/iris!284

theories/algebra/auth.v

@@ -366,6 +366,12 @@ Qed.
 Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
 Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
 
+Lemma auth_update_auth a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a'.
+Proof.
+  intros. etrans; first exact: auth_update_alloc.
+  exact: cmra_update_op_l.
+Qed.
+
 Lemma auth_update_core_id a b `{!CoreId b} :
   b ≼ a → ● a ~~> ● a ⋅ ◯ b.
 Proof.

theories/algebra/updates.v

@@ -47,6 +47,11 @@ Qed.
 Lemma cmra_updateP_weaken (P Q : A → Prop) x :
   x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
 Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
+Lemma cmra_update_exclusive `{!Exclusive x} y:
+  ✓ y → x ~~> y.
+Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
+
+(** Updates form a preorder. *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof.
   split.
@@ -54,9 +59,6 @@ Proof.
   - intros x y z. rewrite !cmra_update_updateP.
     eauto using cmra_updateP_compose with subst.
 Qed.
-Lemma cmra_update_exclusive `{!Exclusive x} y:
-  ✓ y → x ~~> y.
-Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
 
 Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
   x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) →