Merge branch 'ralf/Z_local_update' into 'master'

make Z_local_update statement more intuitive

See merge request iris/iris!1010

CHANGELOG.md

@@ -16,6 +16,9 @@ lemma.
   assumption that follows from the other assumptions.
 * Add `inj_cmra_mixin_restrict_validity` as a more general version of
   `iso_cmra_mixin_restrict_validity`.
+* Change statement of [Z_local_update] to be more intuitive. It now says
+  [x - y = x' - y' → (x,y) ~l~> (x',y')], i.e., the difference between the
+  authoritative element and the fragment must stay the same.
 
 ## Iris 4.1.0 (2023-10-11)
 

iris/algebra/numbers.v

@@ -32,6 +32,8 @@ Section nat.
   Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
 
   Lemma nat_local_update (x y x' y' : nat) :
+    (** Morally [x - y = x' - y']: the difference between auth and frag must
+    stay the same with this update. Written using [+] due to underflow. *)
     x + y' = x' + y → (x,y) ~l~> (x',y').
   Proof.
     intros ??; apply local_update_unital_discrete=> z _.
@@ -221,8 +223,9 @@ Section Z.
   Global Instance Z_cancelable (x : Z) : Cancelable x.
   Proof. by intros ???? ?%Z.add_cancel_l. Qed.
 
+  (** The difference between auth and frag must stay the same with this update. *)
   Lemma Z_local_update (x y x' y' : Z) :
-    x + y' = x' + y → (x,y) ~l~> (x',y').
+    x - y = x' - y' → (x,y) ~l~> (x',y').
   Proof.
     intros. rewrite local_update_unital_discrete=> z _.
     compute -[Z.sub Z.add]; lia.