Better log. atomic spec. for weak increment

theories/examples/ticket_lock.v

@@ -319,13 +319,13 @@ Section refinement.
      cf wkIncr specification from (da Rocha Pinto, Dinsdale-Young, Gardner)
      Parameter type: nat
      Precondition: λn, x ↦ᵢ n
-     Postcondition λ_, ∃ n, x ↦ᵢ n
+     Postcondition λ_, ∃ n, x ↦ᵢ (n+1)
  *)
   Lemma wkincr_atomic_l R1 R2 Δ Γ E K x t τ  :
     R2 -∗
     □ (|={⊤,E}=> ∃ n : nat, x ↦ᵢ #n ∗ R1 n ∗
-       ((∃ n : nat, x ↦ᵢ #n ∗ R1 n) ={E,⊤}=∗ True) ∧
-        (∀ m, (∃ n : nat, x ↦ᵢ #n) ∗ R1 m -∗ R2 -∗
+       (x ↦ᵢ #n ∗ R1 n ={E,⊤}=∗ True) ∧
+        ((∃ n : nat, x ↦ᵢ #(n + 1)) ∗ R1 n -∗ R2 -∗
             {E;Δ;Γ} ⊨ fill K Unit ≤log≤ t : τ))
     -∗ ({Δ;Γ} ⊨ fill K (wkincr #x) ≤log≤ t : τ).
   Proof.
@@ -337,7 +337,7 @@ Section refinement.
     iMod "H" as (n) "[Hx [HR1 [Hrev _]]]". iModIntro.
     iExists _; iFrame. iNext. iIntros "Hx".
     iMod ("Hrev" with "[HR1 Hx]") as "_"; simpl.
-    { iExists _. iFrame. }
+    { iFrame. }
     rel_op_l.
     rel_store_l_atomic.
     iMod "H2" as (m) "[Hx [HR1 [_ Hmod]]]". iModIntro.
@@ -364,15 +364,15 @@ Section refinement.
     openI.
     iModIntro. iExists _; iFrame.
     rewrite {1}/R. iSplitR "Hcl".
-    { iExists _,_; by iFrame. } clear o n b.
+    { iExists _,_; by iFrame. }
     iSplit.
-    - iDestruct 1 as (o) "[Hlo HR]".
-      unfold R. iDestruct "HR" as (n b) "HR".
+    - iIntros "[Hlo HR]".
+      unfold R. iDestruct "HR" as (n' b') "HR".
       iApply "Hcl".
       iNext. iExists _,_,_; by iFrame.
-    - iIntros (?) "[Hlo HR] _".
-      iDestruct "Hlo" as (o) "Hlo".
-      unfold R. iDestruct "HR" as (n b) "(Hln & Hissued & Hl' & Hticket)".
+    - iIntros "[Hlo HR] _".
+      iDestruct "Hlo" as (o') "Hlo".
+      unfold R. iDestruct "HR" as (n' b') "(Hln & Hissued & Hl' & Hticket)".
       rel_apply_r (bin_log_related_release_r with "Hl'").
       { solve_ndisj. }
       iIntros "Hl'".