From 72be456a178bcc93c1d8258b0fd1fda661180c70 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 Mar 2020 19:03:36 +0100
Subject: [PATCH] `skipN` function.

---
 _CoqProject           |  1 +
 theories/utils/skip.v | 11 +++++++++++
 2 files changed, 12 insertions(+)
 create mode 100644 theories/utils/skip.v

diff --git a/_CoqProject b/_CoqProject
index 5539986..bc90218 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,6 @@
 -Q theories actris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths
+theories/utils/skip.v
 theories/utils/llist.v
 theories/utils/compare.v
 theories/utils/contribution.v
diff --git a/theories/utils/skip.v b/theories/utils/skip.v
new file mode 100644
index 0000000..6d154de
--- /dev/null
+++ b/theories/utils/skip.v
@@ -0,0 +1,11 @@
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+
+Definition skipN : val :=
+  rec: "go" "n" := if: #0 < "n" then "go" ("n" - #1) else #().
+
+Lemma skipN_spec `{heapG Σ} Φ (n : nat) : ▷^n (Φ #()) -∗ WP skipN #n {{ Φ }}.
+Proof.
+  iIntros "HΦ". iInduction n as [|n] "IH"; wp_rec; wp_pures; [done|].
+  rewrite Z.sub_1_r Nat2Z.inj_succ Z.pred_succ. by iApply "IH".
+Qed.
-- 
GitLab