From e5d7df97f45abecfa0a4200a97620ec4fbc3899b Mon Sep 17 00:00:00 2001
From: jihgfee <jkas@itu.dk>
Date: Thu, 27 Jun 2019 10:19:08 +0200
Subject: [PATCH] Moved list sort instance to separate file

---
 _CoqProject                             |  1 +
 theories/examples/list_sort.v           | 37 -------------------
 theories/examples/list_sort_instances.v | 48 +++++++++++++++++++++++++
 3 files changed, 49 insertions(+), 37 deletions(-)
 create mode 100644 theories/examples/list_sort_instances.v

diff --git a/_CoqProject b/_CoqProject
index 6142db8..3c324c7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,3 +7,4 @@ theories/channel/channel.v
 theories/channel/proto_model.v
 theories/channel/proto_channel.v
 theories/examples/list_sort.v
+theories/examples/list_sort_instances.v
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 805de1b..dfb91f0 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -3,9 +3,6 @@ From osiris.channel Require Import proto_channel.
 From iris.heap_lang Require Import proofmode notation.
 From osiris.utils Require Import list.
 
-Definition compare_vals : val :=
-    λ: "x" "y", "x" ≤ "y".
-
 Definition lmerge : val :=
   rec: "go" "cmp" "hys" "hzs" :=
     match: "hys" with
@@ -216,38 +213,4 @@ Section list_sort.
     wp_pures. iApply "HΦ". iFrame.
   Qed.
 
-  (* Example: Sort of integers *)
-  Definition IZ (x : Z) (v : val) : iProp Σ :=
-    ⌜∃ w, v = LitV $ LitInt w ∧ x = w⌝%I.
-
-  Lemma compare_vals_spec : cmp_spec IZ (≤) compare_vals.
-  Proof.
-    iIntros (x x' v v' Φ) "!>".
-    iIntros ([[w [-> ->]] [w' [-> ->]]]) "HΦ".
-    wp_lam. wp_pures. iApply "HΦ". eauto 10 with iFrame.
-  Qed.
-
-  Local Arguments val_encode _ _ !_ /.
-
-  Lemma list_sort_client_le_spec l (xs : list Z) :
-    {{{ l ↦ val_encode xs }}}
-      list_sort_client compare_vals #l
-    {{{ ys, RET #(); ⌜Sorted (≤) ys⌝ ∗ ⌜ ys ≡ₚ xs⌝ ∗ l ↦ val_encode ys }}}.
-  Proof.
-    assert (∀ zs : list Z, val_encode zs = val_encode (LitV ∘ LitInt <$> zs)) as Henc.
-    { intros zs. induction zs; f_equal/=; auto with f_equal. }
-    iIntros (Φ) "Hl HΦ".
-    iApply (list_sort_client_spec IZ (≤) _ _ (LitV ∘ LitInt <$> xs) xs with "[] [Hl] [HΦ]").
-    { iApply compare_vals_spec. }
-    { rewrite -Henc. iFrame "Hl".
-      iInduction xs as [|x xs] "IH"; csimpl; first by iFrame.
-      iFrame "IH". by iExists x. }
-    iIntros "!>" (ys ws) "(?&?&?&HI)".
-    iAssert ⌜ ws = (LitV ∘ LitInt) <$> ys ⌝%I with "[HI]" as %->.
-    { iInduction ys as [|y ys] "IH" forall (ws);
-        destruct ws as [|w ws]; csimpl; try done.
-      iDestruct "HI" as "[HI1 HI2]"; iDestruct "HI1" as %(?&->&->).
-      by iDestruct ("IH" with "HI2") as %->. }
-    rewrite -Henc. iApply ("HΦ" $! ys with "[$]").
-  Qed.
 End list_sort.
diff --git a/theories/examples/list_sort_instances.v b/theories/examples/list_sort_instances.v
new file mode 100644
index 0000000..acfdbfc
--- /dev/null
+++ b/theories/examples/list_sort_instances.v
@@ -0,0 +1,48 @@
+From stdpp Require Import sorting.
+From osiris.channel Require Import proto_channel.
+From iris.heap_lang Require Import proofmode notation.
+From osiris.utils Require Import list.
+From osiris.examples Require Import list_sort.
+
+Section list_sort_instances.
+  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
+
+  (* Example: Sort of integers *)
+  Definition IZ (x : Z) (v : val) : iProp Σ :=
+    ⌜∃ w, v = LitV $ LitInt w ∧ x = w⌝%I.
+
+  Definition compareZ : val :=
+    λ: "x" "y", "x" ≤ "y".
+
+  Lemma compareZ_spec : cmp_spec IZ (≤) compareZ.
+  Proof.
+    iIntros (x x' v v' Φ) "!>".
+    iIntros ([[w [-> ->]] [w' [-> ->]]]) "HΦ".
+    wp_lam. wp_pures. iApply "HΦ". eauto 10 with iFrame.
+  Qed.
+  
+  Local Arguments val_encode _ _ !_ /.
+
+  Lemma list_sort_client_le_spec l (xs : list Z) :
+    {{{ l ↦ val_encode xs }}}
+      list_sort_client compareZ #l
+      {{{ ys, RET #(); ⌜Sorted (≤) ys⌝ ∗ ⌜ ys ≡ₚ xs⌝ ∗ l ↦ val_encode ys }}}.
+  Proof.
+    assert (∀ zs : list Z, val_encode zs = val_encode (LitV ∘ LitInt <$> zs)) as Henc.
+    { intros zs. induction zs; f_equal/=; auto with f_equal. }
+    iIntros (Φ) "Hl HΦ".
+    iApply (list_sort_client_spec N IZ (≤) _ _ (LitV ∘ LitInt <$> xs) xs with "[] [Hl] [HΦ]").
+    { iApply compareZ_spec. }
+    { rewrite -Henc. iFrame "Hl".
+      iInduction xs as [|x xs] "IH"; csimpl; first by iFrame.
+      iFrame "IH". by iExists x. }
+    iIntros "!>" (ys ws) "(?&?&?&HI)".
+    iAssert ⌜ ws = (LitV ∘ LitInt) <$> ys ⌝%I with "[HI]" as %->.
+    { iInduction ys as [|y ys] "IH" forall (ws);
+      destruct ws as [|w ws]; csimpl; try done.
+      iDestruct "HI" as "[HI1 HI2]"; iDestruct "HI1" as %(?&->&->).
+      by iDestruct ("IH" with "HI2") as %->. }
+    rewrite -Henc. iApply ("HΦ" $! ys with "[$]").
+  Qed.
+
+End list_sort_instances.
-- 
GitLab