From ca9a1a828795407ad6aaaef7f488affe42857811 Mon Sep 17 00:00:00 2001
From: Simon Spies <simonspies@icloud.com>
Date: Sat, 18 Jan 2025 14:53:50 +0100
Subject: [PATCH] curry the first function
---
theories/examples/refinements/examples.v | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/theories/examples/refinements/examples.v b/theories/examples/refinements/examples.v
index 700a04c2..da95b200 100644
--- a/theories/examples/refinements/examples.v
+++ b/theories/examples/refinements/examples.v
@@ -10,8 +10,8 @@ Set Default Proof Using "Type".
Section implementation.
(* first examples *)
- Definition first (p: val) : val :=
- rec: "first" "x" := if: p "x" then "x" else "first" ("x" + #1).
+ Definition first : val :=
+ rec: "first" "p" "x" := if: "p" "x" then "x" else "first" "p" ("x" + #1).
Definition f_ex : val :=
λ: "x", #41 ≤ "x" - #1.
@@ -60,8 +60,9 @@ Section first_proofs.
intros Hfg. iStartProof. iRevert (m). iLöb as "IH".
iIntros (m K) "!# Hsrc Hna".
iApply (rwp_take_step with "[Hna]"); first done; last first.
- { rewrite /first. src_pure _ in "Hsrc". fold (first g). iApply weak_src_update_return. iExact "Hsrc". }
- iIntros "Hsrc". wp_rec. wp_bind (f _).
+ { rewrite /first. src_pure _ in "Hsrc". fold (first). iApply weak_src_update_return. iExact "Hsrc". }
+ iIntros "Hsrc". wp_rec. wp_pures. wp_bind (f _).
+ do 2 src_pure _ in "Hsrc".
src_bind (g _) in "Hsrc".
iPoseProof (Hfg with "Hsrc Hna") as "Hfg".
iApply (rwp_wand with "Hfg"). iIntros (v) "[Hna [Hsrc H]]".
--
GitLab