experiment: use coq's ability to infer more canonical structures

iris/base_logic/lib/iprop.v

@@ -32,6 +32,8 @@ Global Arguments GFunctor _ {_}.
 Global Existing Instance gFunctor_map_contractive.
 Add Printing Constructor gFunctor.
 
+Notation GFunctorConst F := (GFunctor (constRF F)).
+
 (** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
 of [gFunctor]s.
 

iris_heap_lang/lib/rw_spin_lock.v

@@ -33,10 +33,10 @@ Local Definition acquire_writer : val :=
 Local Definition release_writer : val :=
   λ: "l", "l" <- #0.
 
-Class rwlockG Σ := RwLockG { rwlock_tokG : inG Σ (authR (gmultisetUR Qp)) }.
+Class rwlockG Σ := RwLockG { rwlock_tokG : inG Σ (auth (gmultiset Qp)) }.
 Local Existing Instance rwlock_tokG.
 
-Local Definition rwlockΣ : gFunctors := #[GFunctor (authR (gmultisetUR Qp)) ].
+Local Definition rwlockΣ : gFunctors := #[GFunctorConst (auth (gmultiset Qp)) ].
 Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
 Proof. solve_inG. Qed.
 

iris_heap_lang/lib/spawn.v

@@ -19,10 +19,10 @@ Definition join : val :=
 
 (** The CMRA & functor we need. *)
 (* Not bundling heapGS, as it may be shared with other users. *)
-Class spawnG Σ := SpawnG { spawn_tokG : inG Σ (exclR unitO) }.
+Class spawnG Σ := SpawnG { spawn_tokG : inG Σ (excl ()) }.
 Local Existing Instance spawn_tokG.
 
-Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
+Definition spawnΣ : gFunctors := #[GFunctorConst (excl ())].
 
 Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. solve_inG. Qed.

iris_heap_lang/lib/spin_lock.v

@@ -14,10 +14,10 @@ Definition release : val := λ: "l", "l" <- #false.
 
 (** The CMRA we need. *)
 (* Not bundling heapGS, as it may be shared with other users. *)
-Class lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
+Class lockG Σ := LockG { lock_tokG : inG Σ (excl ()) }.
 Local Existing Instance lock_tokG.
 
-Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
+Definition lockΣ : gFunctors := #[GFunctorConst (excl ())].
 
 Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.

iris_heap_lang/lib/ticket_lock.v

@@ -28,11 +28,11 @@ Definition release : val :=
 
 (** The CMRAs we need. *)
 Class tlockG Σ :=
-  tlock_G : inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
+  tlock_G : inG Σ (auth (excl' nat * gset_disj nat)).
 Local Existing Instance tlock_G.
 
 Definition tlockΣ : gFunctors :=
-  #[ GFunctor (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))) ].
+  #[ GFunctorConst (auth (excl' nat * gset_disj nat)) ].
 
 Global Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. solve_inG. Qed.
@@ -45,14 +45,14 @@ Section proof.
     ∃ o n : nat,
       lo ↦ #o ∗ ln ↦ #n ∗
       own γ (● (Excl' o, GSet (set_seq 0 n))) ∗
-      ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε, GSet {[ o ]}))).
+      ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε : excl' _, GSet {[ o ]}))).
 
   Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
     ∃ lo ln : loc,
       ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R).
 
   Definition issued (γ : gname) (x : nat) : iProp Σ :=
-    own γ (◯ (ε, GSet {[ x ]})).
+    own γ (◯ (ε : excl' _, GSet {[ x ]})).
 
   Definition locked (γ : gname) : iProp Σ := ∃ o, own γ (◯ (Excl' o, GSet ∅)).