Mutex non-expansive, MutexGuard contractive

theories/lang/lib/lock.v

@@ -27,7 +27,7 @@ Section proof.
 
   Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
 
-  Global Instance lock_inv_ne γ l : NonExpansive (lock_proto γ l).
+  Global Instance lock_proto_ne γ l : NonExpansive (lock_proto γ l).
   Proof. solve_proper. Qed.
 
   Global Instance locked_timeless γ : TimelessP (locked γ).

theories/typing/lib/mutex/mutex.v

@@ -87,7 +87,19 @@ Section mutex.
   Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
     { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
 
-  (* TODO: Non-expansiveness, compat with eqtype, Send+Sync if ty is Send. *)
+  Global Instance mutex_type_ne : TypeNonExpansive mutex.
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance mutex_ne : NonExpansive mutex.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
+  (* TODO: compat with eqtype, Send+Sync if ty is Send. *)
 
 End mutex.
 

theories/typing/lib/mutex/mutexguard.v

@@ -79,7 +79,16 @@ Section mguard.
   Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
     { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
 
-  (* TODO: Contractivity, compat with lft_incl and eqtype.
+  Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv
+                                    || exact: type_dist2_S).
+  Qed.
+  Global Instance mutexguard_ne α : NonExpansive (mutexguard α).
+  Proof. apply type_contractive_ne, _. Qed.
+
+  (* TODO: compat with lft_incl and eqtype.
      MutexGuard is Sync if T is Send. *)
 
 End mguard.