Use the most general rule for FAI in the ticket lock proof

theories/tests/relatomic.v

@@ -71,9 +71,9 @@ Section contents.
   Lemma FAI_atomic R1 R2 Γ E1 E2 K x t τ Δ :
     R2 -∗
     □ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R1 n ∗
-       (x ↦ᵢ #n ∗ R1 n ={E2,E1}=∗ True) ∧
-        (x ↦ᵢ #(S n) ∗ R1 n -∗ R2 -∗
-            {E2,E1;Δ;Γ} ⊨ fill K #n ≤log≤ t : τ))
+       ((∃ (m: nat), x ↦ᵢ #m ∗ R1 m) ={E2,E1}=∗ True) ∧
+        (∀ m, x ↦ᵢ #(S m) ∗ R1 m -∗ R2 -∗
+            {E2,E1;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ))
     -∗ ({E1;Δ;Γ} ⊨ fill K (FAI #x) ≤log≤ t : τ).
   Proof.
     iIntros "HR2 #H".
@@ -87,7 +87,7 @@ Section contents.
     iExists #n. iFrame. iNext. iIntros "Hx".
     iDestruct "Hrev" as "[Hrev _]".
     iMod ("Hrev" with "[HR Hx]") as "_".
-    { by iFrame. }
+    { iExists _. by iFrame. }
     rel_rec_l. rel_op_l.
     rel_cas_l_atomic.
     iMod "H" as (n') "[Hx [HR HQ]]". iModIntro.
@@ -104,7 +104,7 @@ Section contents.
       rel_if_l.
       iDestruct "HQ" as "[HQ _]".
       iMod ("HQ" with "[Hx HR]") as "_".
-      { by iFrame. }
+      { iExists _. by iFrame. }
       unlock FAI.
       by iApply "IH".
   Qed.
@@ -225,7 +225,7 @@ Section contents.
     rel_let_l. repeat rel_proj_l.
     (* rel_apply_l (FAI_atomic). *)
     rel_bind_l (FAI #ln).
-    iApply (FAI_atomic (fun _ => True)%I True%I); first done.
+    iApply (FAI_atomic (fun n => own γ (● GSet (seq_set 0 n)))%I True%I); first done.
     iAlways.
     iInv N as (P) "[>HP Hpool]" "Hcl".
     iDestruct (lockPool_lookup with "HP Hls") as %Hls.
@@ -233,17 +233,15 @@ Section contents.
     rewrite {1}/lockInv.
     iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & >Hseq & Hl' & Hrest)".
     iModIntro. iExists _; iFrame.
-    iSplitR; first done.
     iSplit.
-    - iIntros "[Hln ?]".
-      iMod ("Hcl" with "[-]") as "_".
-      { iNext. iExists P; iFrame.
-        iApply "Hpool". iExists _,_,_; iFrame. iFrame "Hrest". }
-      done.
-    - iIntros "[Hln ?] _".
+    - iDestruct 1 as (m) "[Hln ?]".
+      iApply ("Hcl" with "[-]").
+      iNext. iExists P; iFrame.
+      iApply "Hpool". iExists _,_,_; by iFrame.
+    - iIntros (m) "[Hln Hseq] _".
       iMod (own_update with "Hseq") as "[Hseq Hticket]".
       { eapply auth_update_alloc.
-        eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
+        eapply (gset_disj_alloc_empty_local_update _ {[ m ]}).
         apply (seq_set_S_disjoint 0). }
       rewrite -(seq_set_S_union_L 0).
       iMod ("Hcl" with "[-Hticket]") as "_".