an attempt at fixing the proof of `debit_force`, but `debit_pay` is now broken

theories/Debits.v

@@ -16,7 +16,8 @@ Section Debits.
   Definition debitN : namespace := nroot .@ "debit".
 
   Definition DebitInv γ Q : iProp Σ :=
-    ∃ n, own γ (● MinNat' n) ∗ (TC n ==∗ □ Q). (* TODO: should probably be a fupd *)
+    ∃ n, own γ (● MinNat' n) ∗ ((⌜n ≠ 0⌝ ∗ (TC n ==∗ □ Q)) ∨ □ Q).
+    (* TODO: should probably be a fupd *)
   Definition Debit n Q : iProp Σ :=
     ∃ γ, inv debitN (DebitInv γ Q) ∗ own γ (◯ MinNat' n).
 
@@ -28,7 +29,13 @@ Section Debits.
     iIntros "HQ".
     iMod (own_alloc (● MinNat' n ⋅ ◯ MinNat' n)) as (γ) "[H● H◯]";
       first by apply auth_both_valid_2.
-    iExists γ. iFrame. iApply inv_alloc. iNext. iExists n. by iFrame.
+    iExists γ. iFrame.
+    destruct n as [|n'].
+    (* case: n = 0, we obtain the postcondition □Q (consume the ==∗) right now: *)
+    { iMod zero_TC as "Htc0"; iMod ("HQ" with "Htc0") as "HQ".
+      iApply inv_alloc. iNext. iExists 0. by auto with iFrame. }
+    (* case: n ≥ 1, we keep the postcondition suspended: *)
+    { iApply inv_alloc. iNext. iExists (S n'). by auto with iFrame. }
   Qed.
 
   Lemma debit_weaken n₁ n₂ Q :
@@ -48,11 +55,36 @@ Section Debits.
     iMod (inv_acc with "Hinv") as "[Hinner Hclose]"; first done.
     iDestruct "Hinner" as (m) "[>H● HQ]".
     iDestruct (auth_min_nat_update_decr with "H● H◯") as ">[H● H◯]".
-    iMod ("Hclose" with "[H● Htc HQ]") as "_".
-    { iNext. iExists (m-k). iFrame "H●". iIntros "Htc'". iApply "HQ".
-      iCombine "Htc Htc'" as "Htc". iApply (TC_weaken with "Htc"). lia. }
-    { iModIntro. iExists γ. by iFrame. }
-  Qed.
+    destruct (decide (m - k ≠ 0)%nat).
+    (* case: m > k: *)
+    {
+      iExists γ. iFrame "#∗". iApply "Hclose".
+      iNext. iExists (m-k). iFrame "H●".
+      iDestruct "HQ" as "[[% Hupd]|HQ]".
+      (* case: m ≥ 1, we just decrease the remaining time cost of the ==∗ : *)
+      { iLeft. iFrame "%". iIntros "Htc'". iApply "Hupd".
+        iCombine "Htc Htc'" as "Htc". iApply (TC_weaken with "Htc"). lia. }
+      (* case: m = 0 (spurious but provable), the postcond was already obtained: *)
+      { iRight. by auto with iFrame. }
+    }
+    (* case: m ≤ k *)
+    {
+      assert (m-k = 0)%nat as -> by lia.
+      iExists γ. iFrame "#∗".
+      iDestruct "HQ" as "[[Hnonzero Hupd]|HQ]".
+      (* case: m ≥ 1, the cost just felt to zero
+         and we obtain the poscondition (consume the ==∗) right now: *)
+      {
+        (* FIXME: cannot prove this *)
+        admit.
+      }
+      (* case: m = 0, the cost was already zero
+         and the postcondition was already obtained: *)
+      { iApply "Hclose".
+        iNext. iExists 0. iFrame "H●". iRight. done.
+      }
+    }
+  Admitted.
 
   Lemma debit_force Q E :
     ↑debitN ⊆ E →
@@ -62,19 +94,11 @@ Section Debits.
     iMod (inv_acc with "Hinv") as "[Hinner Hclose]"; first done.
     iDestruct "Hinner" as (m) "[>H● HQ]".
     iDestruct (own_auth_min_nat_le with "H● H◯") as % ->%Nat.le_0_r. iClear "H◯".
-    iDestruct (bi.later_wand with "HQ") as "HQ". iMod zero_TC as "Htc0".
-    iDestruct ("HQ" with "Htc0") as "HQ".
-    rewrite /DebitInv.
-    (* FIXME: how to duplicate ▷ (|==> □ Q) ?
-        "H●" : own γ (● MinNat' 0)
-        "Hclose" : ▷ (∃ n, own γ (● MinNat' n) ∗ (TC n ==∗ □ Q)) ={E∖↑debitN,E}=∗ True
-        "HQ" : ▷ (|==> □ Q)
-        --------------------------------------∗
-        |={E∖↑debitN,E}=> ▷ □ Q
-    *)
-    iMod ("Hclose" with "[H● HQ]") as "_".
-    { iNext. iExists 0. by auto with iFrame. }
-    { admit. }
-  Admitted.
+    iDestruct "HQ" as "[[#Habsurd _]|#HQ]".
+    (* case: m ≥ 1, absurd: *)
+    { by iMod ("Hclose" with "[]"); [|iModIntro]; iNext; iDestruct "Habsurd" as %?. }
+    (* case: m = 0, we have the postcondition at hand: *)
+    { iFrame "HQ". iApply "Hclose". iNext. iExists 0. by auto with iFrame. }
+  Qed.
 
 End Debits.