From 6ee7c69eb526e7274b8b3740955ed584c02e7a98 Mon Sep 17 00:00:00 2001
From: Simon Spies <simonspies@icloud.com>
Date: Mon, 4 Nov 2024 14:12:34 +0100
Subject: [PATCH] add derived rules for termination

---
 _CoqProject                             |  3 +-
 theories/examples/termination/derived.v | 88 +++++++++++++++++++++++++
 2 files changed, 90 insertions(+), 1 deletion(-)
 create mode 100644 theories/examples/termination/derived.v

diff --git a/_CoqProject b/_CoqProject
index 08cde9de..9aae01c8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -135,6 +135,7 @@ theories/examples/transfinite.v
 
 # derived Hoare triples
 theories/examples/refinements/derived.v
+theories/examples/termination/derived.v
 
 # key ideas
 theories/examples/keyideas/simulations.v
@@ -150,7 +151,7 @@ theories/examples/safety/ticket_lock.v
 theories/examples/safety/nondet_bool.v
 theories/examples/safety/counter.v
 theories/examples/safety/lazy_coin.v
-theories/examples/safety/clairvoyant_coin.v 
+theories/examples/safety/clairvoyant_coin.v
 
 theories/examples/safety/barrier/barrier.v
 theories/examples/safety/barrier/proof.v
diff --git a/theories/examples/termination/derived.v b/theories/examples/termination/derived.v
new file mode 100644
index 00000000..5d19453a
--- /dev/null
+++ b/theories/examples/termination/derived.v
@@ -0,0 +1,88 @@
+
+From iris.program_logic.refinement Require Export ref_weakestpre ref_adequacy seq_weakestpre.
+From iris.examples.refinements Require Export refinement.
+From iris.algebra Require Import auth.
+From iris.heap_lang Require Import proofmode notation.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+
+(* We illustrate here how to derive the rules shown in the paper *)
+
+
+Section derived.
+  Context {SI} {Σ: gFunctors SI} `{Hheap: !heapG Σ} `{Htc: !tcG Σ} `{Hseq: !seqG Σ}.
+
+  Definition seq_rswp E e φ : iProp Σ := (na_own seqG_name E -∗ RSWP e at 0 ⟨⟨ v, na_own seqG_name E ∗ φ v ⟩⟩)%I.
+  Notation "⟨⟨ P ⟩ ⟩ e ⟨⟨ v , Q ⟩ ⟩" := (□ (P -∗ (seq_rswp ⊤ e (λ v, Q))))%I
+  (at level 20, P, e, Q at level 200, format "⟨⟨  P  ⟩ ⟩  e  ⟨⟨  v ,  Q  ⟩ ⟩") : stdpp_scope.
+  Notation "{{ P } } e {{ v , Q } }" := (□ (P -∗ SEQ e ⟨⟨ v, Q ⟩⟩))%I
+  (at level 20, P, e, Q at level 200, format "{{  P  } }  e  {{  v ,  Q  } }") : stdpp_scope.
+
+
+  (* Extended Refinement Program Logic of Transfinite Iris *)
+  Lemma value_term (v: val): (⊢ {{True}} v {{w, ⌜v = w⌝}})%I.
+  Proof.
+    iIntros "!> _ $". by iApply rwp_value.
+  Qed.
+
+
+  Lemma bind_term (e: expr) K P Q R:
+    ({{P}} e {{v, Q v}} ∗ (∀ v: val, ({{Q v}} fill K (Val v) {{w, R w}}))
+    ⊢ {{P}} fill K e {{v, R v}})%I.
+  Proof.
+    iIntros "[#H1 #H2] !> P Hna".
+    iApply rwp_bind. iSpecialize ("H1" with "P Hna").
+    iApply (rwp_strong_mono with "H1 []"); auto.
+    iIntros (v) "[Hna Q] !>". iApply ("H2" with "Q Hna").
+  Qed.
+
+  Lemma pure_term (e e': expr) P Q: pure_step e e' → ({{P}} e' {{v, Q v}} ⊢ ⟨⟨P⟩⟩ e ⟨⟨v, Q v⟩⟩)%I.
+  Proof.
+    iIntros (Hstep) "#H !> P Hna".
+    iApply (ref_lifting.rswp_pure_step_later _ _ _ _ _ True); [|done|by iApply ("H" with "P Hna")].
+    intros _. apply nsteps_once, Hstep.
+  Qed.
+
+  Lemma store_term l (v1 v2: val): (True ⊢ ⟨⟨l ↦ v1⟩⟩ #l <- v2 ⟨⟨w, ⌜w = #()⌝ ∗ l ↦ v2⟩⟩)%I.
+  Proof.
+    iIntros "_ !> Hl $". iApply (rswp_store with "[$Hl]").
+    by iIntros "$".
+  Qed.
+
+  Lemma load_term l v: (True ⊢ ⟨⟨l ↦ v⟩⟩ ! #l ⟨⟨w, ⌜w = v⌝ ∗ l ↦ v⟩⟩)%I.
+  Proof.
+    iIntros "_ !> Hl $". iApply (rswp_load with "[$Hl]").
+    by iIntros "$".
+  Qed.
+
+  Lemma ref_term (v: val): (True ⊢ ⟨⟨ True ⟩⟩ ref v ⟨⟨w, ∃ l: loc, ⌜w = #l⌝ ∗ l ↦ v⟩⟩)%I.
+  Proof.
+    iIntros "_ !> _ $". iApply (rswp_alloc with "[//]").
+    iIntros (l) "[Hl _]". iExists l. by iFrame.
+  Qed.
+
+  Lemma flip_term (e: expr) P Q: to_val e = None → (⟨⟨P⟩⟩ e ⟨⟨v, Q v⟩⟩ ⊢ {{P}} e {{v, Q v}})%I.
+  Proof.
+    iIntros (H) "#H !> P Hna". iApply rwp_no_step; first done.
+    by iApply ("H" with "P Hna").
+  Qed.
+
+  Lemma spend_cred_term P et Q α β :
+    to_val et = None →
+    ord_lt β α →
+    ⟨⟨ $ β ∗ P ⟩⟩ et ⟨⟨ v, Q v ⟩⟩ ⊢  {{ $α ∗ ▷ P}} et {{v, Q v}}.
+  Proof.
+    iIntros (He Hlt) "#H !> [Hc P]  Hna". iApply (rwp_take_step with "[Hna P] [Hc]"); first done; last first.
+    - iApply (@auth_src_update _ _ (ordA SI) with "Hc"). apply Hlt.
+    - iIntros "Hβ". iApply rswp_do_step. iNext.
+      iApply ("H" with "[$P $Hβ] Hna").
+  Qed.
+
+  Lemma split_cred_term α β :
+    $ (α ⊕ β) ⊣⊢ $ α ∗ $ β.
+  Proof.
+    rewrite srcF_split //.
+  Qed.
+
+End derived.
-- 
GitLab