From 2936f766d3492d07b5142f2ab31982c14034b760 Mon Sep 17 00:00:00 2001
From: Simon Spies <simonspies@icloud.com>
Date: Mon, 18 Nov 2024 15:49:43 +0100
Subject: [PATCH] instantiate fib memoization

---
 theories/examples/refinements/memoization.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/theories/examples/refinements/memoization.v b/theories/examples/refinements/memoization.v
index fd28c055..d2d520fb 100644
--- a/theories/examples/refinements/memoization.v
+++ b/theories/examples/refinements/memoization.v
@@ -850,6 +850,22 @@ Section fibonacci.
     - iModIntro. iIntros (e v Hexec K).
       iApply exec_src_update. apply exec_frame, Hexec.
   Qed.
+
+
+  Corollary fib_deep_memoized_instantiate (n: nat) K:
+    src (fill K (fib #n)) ⊢ SEQ (mem_rec eq_heaplang fib_template #n) ⟨⟨ w, ∃ (m: nat), ⌜w = #m⌝ ∗ src (fill K (Val #m)) ⟩⟩.
+  Proof.
+    iStartProof. iIntros "Hsrc Hna".
+    wp_bind (mem_rec eq_heaplang fib_template).
+    iApply (rwp_wand with "[Hna]").
+    { iApply fib_deep_memoized. iFrame. }
+    iIntros (f) "[Hna Himpl]". rewrite /implements.
+    iSpecialize ("Himpl" $! #n #n K with "[] Hsrc Hna").
+    { iExists _; done. }
+    iApply (rwp_wand with "Himpl").
+    iIntros (v) "($&H)". iDestruct "H" as (w) "(Hrel & Hsrc & _)".
+    iDestruct "Hrel" as %[? [-> ->]]. iExists _. by iFrame.
+  Qed.
 End fibonacci.
 
 Section levenshtein.
-- 
GitLab