use tokens instead of auth

theories/examples/termination/logrel.v

@@ -4,29 +4,28 @@ From iris.base_logic.lib Require Export invariants na_invariants.
 From iris.heap_lang Require Export lang lifting.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation metatheory.
-From iris.algebra Require Import auth.
+From iris.algebra Require Import auth excl.
 From iris.algebra.ordinals Require Import arithmetic.
 Set Default Proof Using "Type".
 
 
 
 Section token_ra.
-  Context {SI: indexT} {Σ: gFunctors SI} `{!inG Σ (authR (unitUR SI))}.
+  (* NOTE: compared to the original submission, this version now uses the
+     more canonical exclusive resource algebra (instead of auth(unit)). *)
+  Context {SI: indexT} {Σ: gFunctors SI} `{!inG Σ (exclR (unitO SI))}.
 
-  Definition tok γ := own γ (● ()).
+  Definition tok γ := own γ (Excl ()).
 
   Lemma tok_alloc: ⊢ (|==> ∃ γ, tok γ)%I.
   Proof.
-    iStartProof. iMod (own_alloc (● ())); auto.
-    by apply auth_auth_valid.
+    iStartProof. iMod (own_alloc (Excl ())); auto. done.
   Qed.
 
   Lemma tok_unique γ: tok γ ∗ tok γ ⊢ False.
   Proof.
-    rewrite /tok -own_op own_valid -auth_auth_frac_op uPred.discrete_valid.
-    iIntros (Htok). apply ->(@auth_auth_frac_valid SI) in Htok.
-    destruct Htok as [Htok _]. apply ->(@frac_valid' SI) in Htok.
-    exfalso. by eapply Qp_not_plus_q_ge_1.
+    rewrite /tok -own_op own_valid uPred.discrete_valid.
+    iIntros (Htok). destruct Htok.
   Qed.
 
 End token_ra.
@@ -86,7 +85,7 @@ Definition get : val :=
   end.
 
 Section semantic_model.
-  Context {SI} {Σ: gFunctors SI} `{Heap: !heapG Σ} `{TimeCredits: !tcG Σ} `{Sequential: !seqG Σ} `{FBI: FiniteBoundedExistential SI} `{Tok: !inG Σ (authR (unitUR SI))}.
+  Context {SI} {Σ: gFunctors SI} `{Heap: !heapG Σ} `{TimeCredits: !tcG Σ} `{Sequential: !seqG Σ} `{FBI: FiniteBoundedExistential SI} `{Tok: !inG Σ (exclR (unitO SI))}.
 
   Implicit Types (l r: loc).
   Implicit Types (n: nat).