Commit 72be456a authored by Robbert Krebbers's avatar Robbert Krebbers

`skipN` function.

parent 4dc8fc9d
-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
......
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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment