Update the counter increment atomic rule

theories/examples/counter.v

@@ -126,10 +126,10 @@ Section CG_Counter.
   Lemma bin_log_FG_increment_logatomic R P Γ E K x t τ  :
     P -∗
     □ (|={⊤,E}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗
-       ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E,⊤}=∗ True) ∧
-        (∀ m, x ↦ᵢ # (S m) ∗ R m -∗ P -∗
-            {E;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ))
-    -∗ ({Δ;Γ} ⊨ fill K (FG_increment #x) ≤log≤ t : τ).
+       ((x ↦ᵢ #n ∗ R n ={E,⊤}=∗ True) ∧
+        (x ↦ᵢ #(S n) ∗ R n -∗ P -∗
+            {E;Δ;Γ} ⊨ fill K #n ≤log≤ t : τ)))
+    -∗ {Δ;Γ} ⊨ fill K (FG_increment #x) ≤log≤ t : τ.
   Proof.
     iIntros "HP #H".
     iLöb as "IH".
@@ -140,18 +140,15 @@ Section CG_Counter.
     iMod "H" as (n) "[Hx [HR Hrev]]".  iModIntro.
     iExists #n. iFrame. iNext. iIntros "Hx".
     iDestruct "Hrev" as "[Hrev _]".
-    iMod ("Hrev" with "[HR Hx]") as "_".
-    { iExists _. iFrame. } simpl.
-    rel_rec_l.
-    rel_op_l.
-    rel_cas_l_atomic.
+    iMod ("Hrev" with "[HR Hx]") as "_"; first iFrame.
+    rel_rec_l. rel_op_l. rel_cas_l_atomic.
     iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
     destruct (decide (n = n')); subst.
     - iExists #n'. iFrame.
       iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
       iIntros "_ !> Hx". simpl.
       iDestruct "HQ" as "[_ HQ]".
-      iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
+      iSpecialize ("HQ" with "[$Hx $HR]").
       rel_if_true_l. by iApply "HQ".
     - iExists #n'. iFrame. 
       iSplitL; eauto; last first.
@@ -159,8 +156,7 @@ Section CG_Counter.
       iIntros "_ !> Hx". simpl.
       rel_if_false_l.
       iDestruct "HQ" as "[HQ _]".
-      iMod ("HQ" with "[Hx HR]").
-      { iExists _; iFrame. }
+      iMod ("HQ" with "[$Hx $HR]").
       rewrite /FG_increment. unlock. simpl.
       by iApply "IH".
   Qed.
@@ -169,15 +165,14 @@ Section CG_Counter.
   Lemma bin_log_counter_read_atomic_l R P Γ E K x t τ :
     P -∗
     □ (|={⊤,E}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗
-       ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E,⊤}=∗ True) ∧
-        (∀ m : nat, x ↦ᵢ #m ∗ R m -∗ P -∗
-            {E;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ))
+       (x ↦ᵢ #n ∗ R n ={E,⊤}=∗ True) ∧
+        (x ↦ᵢ #n ∗ R n -∗ P -∗
+            {E;Δ;Γ} ⊨ fill K #n ≤log≤ t : τ))
     -∗ {Δ;Γ} ⊨ fill K ((counter_read $/ LitV (Loc x)) #()) ≤log≤ t : τ.
   Proof.
     iIntros "HP #H".
     unfold counter_read. unlock. simpl.
-    rel_rec_l.
-    rel_load_l_atomic.
+    rel_rec_l. rel_load_l_atomic.
     iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
     iExists _; iFrame "Hx". iNext.
     iIntros "Hx".
@@ -196,12 +191,12 @@ Section CG_Counter.
               True%I); first done.
     iAlways. iInv counterN as ">Hcnt" "Hcl". iModIntro.
     iDestruct "Hcnt" as (n) "(Hl & Hcnt & Hcnt')".
-    iExists _; iFrame. clear n.
+    iExists _; iFrame.
     iSplit.
-    - iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')".
+    - iIntros "(Hcnt & Hl & Hcnt')".
       iApply ("Hcl" with "[-]").
       iNext. iExists _. iFrame.
-    - iIntros (m) "(Hcnt & Hl & Hcnt') _".
+    - iIntros "(Hcnt & Hl & Hcnt') _".
       rel_apply_r (bin_log_related_CG_increment_r with "Hcnt' Hl").
       { solve_ndisj. }
       iIntros "Hcnt' Hl".
@@ -229,11 +224,11 @@ Section CG_Counter.
          True%I); first done.
     iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose". 
     iModIntro. 
-    iExists n. iFrame "Hcnt Hcnt' Hl". clear n.
+    iExists n. iFrame "Hcnt Hcnt' Hl".
     iSplit.
-    - iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')". iApply "Hclose".
+    - iIntros "(Hcnt & Hl & Hcnt')". iApply "Hclose".
       iNext. iExists n. by iFrame.
-    - iIntros (m) "(Hcnt & Hl & Hcnt') _ /=".
+    - iIntros "(Hcnt & Hl & Hcnt') _ /=".
       rel_apply_r (bin_log_counter_read_r with "Hcnt'").
       { solve_ndisj. }
       iIntros "Hcnt'".

theories/examples/ticket_lock.v

@@ -196,8 +196,8 @@ Section refinement.
   Lemma acquire_l_logatomic R P γ Δ Γ E K lo ln t τ :
     P -∗
     □ (|={⊤,E}=> ∃ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o ∗
-       ((∃ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o) ={E,⊤}=∗ True) ∧
-        (∀ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ ticket γ o ∗ R o -∗ P -∗
+       (∀ o : nat, (∃ n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o) ={E,⊤}=∗ True) ∧
+        (∀ o : nat, (∃ n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ ticket γ o ∗ R o) -∗ P -∗
             {E;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ))
     -∗ ({Δ;Γ} ⊨ fill K (acquire (#lo, #ln)) ≤log≤ t : τ).
   Proof.
@@ -213,33 +213,32 @@ Section refinement.
     { iExists _. iFrame. }
     iSplit.
     - iDestruct "Hrest" as "[H _]".
-      iDestruct 1 as (n') "[Hln Ho]".
+      iIntros "[Hln Ho]".
       iDestruct "Ho" as (o') "[Ho HR]".
       iApply "H".
-      iExists _, _. iFrame.
+      iExists _. iFrame.
     - iDestruct "Hrest" as "[H _]".
-      iIntros (n') "[Hln Ho] HP".
+      iIntros "[Hln Ho] HP".
       iDestruct "Ho" as (o') "[Ho [Hissued HR]]".
       iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
       iMod ("H" with "[-HP Hm]") as "_".
-      { iExists _,_. iFrame. }
-      rel_let_l. clear o n o'.
-      rel_rec_l.
+      { iExists _. iFrame. } clear o o'.
+      rel_let_l. rel_rec_l.
       iLöb as "IH".
       unlock wait_loop. simpl.
       rel_rec_l. rel_proj_l.
       rel_load_l_atomic.
-      iMod "H2" as (o n) "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
+      iMod "H2" as (o n') "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
       iExists _. iFrame. iNext. iIntros "Hlo".
       rel_op_l.
       case_decide; subst; rel_if_l.
       (* Whether the ticket is called out *)
       + iDestruct "Hrest" as "[_ H]".
         iApply ("H" with "[-HP] HP").
-        { iFrame. }
+        { iExists _. iFrame. }
       + iDestruct "Hrest" as "[H _]".
         iMod ("H" with "[-HP Hm]") as "_".
-        { iExists _,_; iFrame. }
+        { iExists _. iFrame. }
         rel_rec_l. iApply ("IH" with "HP Hm").
   Qed.
 
@@ -263,12 +262,12 @@ Section refinement.
     { iExists _. iFrame. }
     clear b o n.
     iSplit.
-    - iDestruct 1 as (o' n') "(Hlo & Hln & Hissued & Hrest)".
+    - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Hrest)".
       iDestruct "Hrest" as (b) "[Hl' Ht]".
       iApply ("Hcl" with "[-]").
       iNext. iExists _,_,_. by iFrame.
-    - iIntros (o n) "(Hlo & Hln & Hissued & Ht & Hrest) _".
-      iDestruct "Hrest" as (b) "[Hl' Ht']".
+    - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Ht & Hrest)".
+      iIntros "_". iDestruct "Hrest" as (b) "[Hl' Ht']".
       destruct b.
       { iDestruct (ticket_nondup with "Ht Ht'") as %[]. }
       rel_apply_r (bin_log_related_acquire_r with "Hl'").
@@ -293,10 +292,10 @@ Section refinement.
     openI.
     iModIntro. iExists _; iFrame.
     iSplit.
-    - iDestruct 1 as (m) "[Hln ?]".
+    - iIntros "[Hln ?]".
       iApply ("Hcl" with "[-]").
       iNext. iExists _,_,_; by iFrame.
-    - iIntros (m) "[Hln Hissued] _".
+    - iIntros "[Hln Hissued] _".
       iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
       iMod ("Hcl" with "[-Hm]") as "_".
       { iNext. iExists _,_,_; by iFrame. }

theories/examples/various.v

@@ -395,21 +395,21 @@ Section refinement.
     - iSplitL "Hc2 Ht".
       { iLeft. iFrame. }
       iSplit.
-      { iDestruct 1 as (m) "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
+      { iIntros "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
         iApply ("Hcl" with "[-]"); iNext.
-        + iExists m. iLeft. iFrame.
-        + iExists (m-1). iRight.
+        + iExists n. iLeft. iFrame.
+        + iExists (n-1). iRight.
           rewrite minus_Sn_m // /= -minus_n_O.
           iFrame. }
-      { iIntros (m) "[Hc1 Hc] _".
+      { iIntros "[Hc1 Hc] _".
         iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
           (rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
           iIntros "Hc2".
         - iMod ("Hcl" with "[-]") as "_".
-          { iNext. iExists (S m). iFrame. iLeft; iFrame. }
+          { iNext. iExists (S n). iFrame. iLeft; iFrame. }
           rel_finish.
         - iMod ("Hcl" with "[-]") as "_".
-          { iNext. iExists m.
+          { iNext. iExists n.
             rewrite minus_Sn_m // /= -minus_n_O.
             iFrame. iRight; iFrame. }
           rel_finish. }
@@ -418,23 +418,21 @@ Section refinement.
         iDestruct "Ht" as "[$ $]".
         iPureIntro. omega. }
       iSplit.
-      { iDestruct 1 as (m) "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
+      { iIntros "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
         iApply ("Hcl" with "[-]"); iNext.
-        + iExists m. iLeft. iFrame.
-        + iExists (m-1). iRight.
-          rewrite minus_Sn_m // /= -minus_n_O.
-          iFrame. }
-      { iIntros (m) "[Hc1 Hc] _".
+        + iExists (S n). iLeft. iFrame.
+        + iExists n. iRight. iFrame.
+          assert (S n - 1 = n) as -> by omega. done. }
+      { iIntros "[Hc1 Hc] _".
         iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
           (rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
           iIntros "Hc2".
         - iMod ("Hcl" with "[-]") as "_".
-          { iNext. iExists (S m). iFrame. iLeft; iFrame. }
+          { iNext. iExists (S (S n)). iFrame. iLeft; iFrame. }
           rel_finish.
         - iMod ("Hcl" with "[-]") as "_".
-          { iNext. iExists m.
-            rewrite minus_Sn_m // /= -minus_n_O.
-            iFrame. iRight; iFrame. }
+          { iNext. iExists (S n). iRight. iFrame.
+            by rewrite -minus_n_O. }
           rel_finish. }
   Qed.
 
@@ -560,16 +558,18 @@ Section refinement.
     { iSplitL "Hc2 Ht Ht'2".
       { iRight. simpl. rewrite -minus_n_O. iFrame. iPureIntro. omega. }
       iSplit.
-      - iIntros. iApply "Hcl". by iApply close_i6.
-      - iIntros (m) "[Hc1 Hc2] Ht".
+      - iIntros. iApply "Hcl". iApply close_i6.
+        iNext. iExists _; iFrame.
+      - iIntros "[Hc1 Hc2] Ht".
         rel_seq_l.
         iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
     }
     { iSplitL "Hc2 Ht".
       { iLeft. by iFrame. }
       iSplit.
-      - iIntros. iApply "Hcl". by iApply close_i6.
-      - iIntros (m) "[Hc1 Hc2] Ht".
+      - iIntros. iApply "Hcl". iApply close_i6.
+        iNext. iExists _; iFrame.
+      - iIntros  "[Hc1 Hc2] Ht".
         rel_seq_l.
         iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
     }