CHANGELOG.md

@@ -3,6 +3,16 @@ way the logic is used on paper.  We also document changes in the Coq
 development; every API-breaking change should be listed, but not every new
 lemma.
 
+## Iris master
+
+**Changes in `algebra`:**
+
+* Add lemma `ufrac_auth_update_surplus_cancel`. 
+
+**Changes in `heap_lang`:**
+
+* Add `Inhabited lock_name` to `lock` class. (by Daniel Nezamabadi)
+
 ## Iris 4.3.0 (2024-10-30)
 
 This Iris release mostly features quality-of-life improvements, such as

README.md

@@ -178,10 +178,9 @@ Getting along with Iris in Coq:
 
 Contacting the developers:
 
-* Discussion about the Iris Coq development happens on the mailing list
-  [iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club)
-  and in the [Iris Chat](https://iris-project.org/chat.html).  This is also the
-  right place to ask questions.
+* Discussion about the Iris Coq development happens in the [Iris
+  Chat](https://iris-project.org/chat.html). This is also the right place to ask
+  questions.
 * If you want to report a bug, please use the
   [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which requires
   an MPI-SWS GitLab account. The [chat page](https://iris-project.org/chat.html)

iris/algebra/lib/ufrac_auth.v

@@ -144,14 +144,34 @@ Section ufrac_auth.
   Qed.
 
   Lemma ufrac_auth_update_surplus p q a b :
-   ✓ (a ⋅ b) → ●U_p a ~~> ●U_(p+q) (a ⋅ b) ⋅ ◯U_q b.
+    ✓ (a ⋅ b) → ●U_p a ~~> ●U_(p+q) (a ⋅ b) ⋅ ◯U_q b.
   Proof.
-    intros Hconsistent. apply: auth_update_alloc.
-    intros n m; simpl; intros [Hvalid1 Hvalid2] Heq.
+    intros Hconsistent. apply: auth_update_alloc. apply local_update_unital.
+    intros n mpa; simpl; intros [Hvalid1 Hvalid2] Heq; simplify_eq/=.
     split.
     - split; by apply cmra_valid_validN.
     - rewrite pair_op Some_op Heq comm.
-      destruct m; simpl; [rewrite left_id | rewrite right_id]; done.
+      destruct mpa; simpl; [rewrite left_id | rewrite right_id]; done.
+  Qed.
+
+  Lemma ufrac_auth_update_surplus_cancel p q a b :
+    Cancelable b →
+    ●U_(p+q) (a ⋅ b) ⋅ ◯U_q b ~~> ●U_p a.
+  Proof.
+    intros. apply: auth_update_dealloc. apply local_update_unital.
+    intros n mpa; simpl; intros [Hvalid1 Hvalid2] Heq; simplify_eq/=.
+    split.
+    { split; by eapply cmra_validN_op_l. }
+    rewrite (comm _ p) (comm _ a) in Heq.
+    destruct mpa as [[p' a']|]; simplify_eq/=.
+    - rewrite -Some_op in Heq.
+      apply (inj _) in Heq as [Hp%leibniz_equiv Ha]; simplify_eq/=.
+      apply (inj _) in Hp as ->.
+      apply (cancelableN _) in Ha; last by rewrite comm.
+      by repeat constructor.
+    - rewrite right_id in Heq.
+      apply (inj _) in Heq as [Hp%leibniz_equiv _]; simplify_eq/=.
+      by apply Qp.add_id_free in Hp.
   Qed.
 End ufrac_auth.
 

iris/base_logic/bupd_alt.v

@@ -18,9 +18,9 @@ of the day (via [bupd_alt (■ P) ⊢ ■ P]).
 We show that:
 
 1. [bupd_alt] enjoys the usual rules of the basic update modality.
-2. [bupd_alt] entails any other modality that enjoys the laws of a basic update
-   modality (see [bupd_bupd_alt]).
-3. The ordinary basic update modality [|==>] on [uPred] entails [bupd_alt]
+2. Any other modality that enjoys the laws of a basic update modality
+   entails [bupd_alt] (see [bupd_bupd_alt]).
+3. [bupd_alt] entails the ordinary basic update modality [|==>] on [uPred] 
    (see [bupd_alt_bupd]). This result is proven in the model of [uPred].
 
 The first two points are shown for any BI with a plain modality. *)

iris_heap_lang/lib/lock.v

@@ -26,6 +26,7 @@ Class lock := Lock {
   lockG : gFunctors → Type;
   (** [name] is used to associate [locked] with [is_lock] *)
   lock_name : Type;
+  #[global] lock_name_inhabited :: Inhabited lock_name;
   (** * Predicates *)
   (** No namespace [N] parameter because we only expose program specs, which
   anyway have the full mask. *)

tex/pftools.sty

@@ -10,6 +10,7 @@
 \RequirePackage{Tabbing}	% Avoid the standard tabbing environment. Its \< conflicts with the semantic package.
 \RequirePackage{xparse}
 \RequirePackage{xcolor}
+\RequirePackage{mathpartir}
 
 %% COLOR DEFINITIONS
 \definecolor{rescolor}{HTML}{005504}