add an example instance

theories/examples/refinements/memoization.v

@@ -20,6 +20,16 @@ Proof.
   intros ? % IHK. by eapply fill_item_injective.
 Qed.
 
+
+Lemma pure_exec_pure_step (e1 e2: expr) φ:
+  PureExec φ 1 e1 e2 →
+  φ →
+  pure_step e1 e2.
+Proof.
+  intros Hpure Hφ. eapply nsteps_once_inv, Hpure, Hφ.
+Qed.
+
+
 Definition eq_heaplang : val := (λ: "n1" "n2", "n1" = "n2").
 
 Notation exec := (tc (@pure_step heap_lang)).
@@ -1910,5 +1920,37 @@ Section levenshtein.
       }
       iApply "H".
   Qed.
+
+
+  Definition lev_mem : val :=
+    λ: "x",
+      (let: "strlen" := mem_rec eq_heaplang strlen_template in
+      mem_rec eq_pair (lev_template "strlen")) "x".
+
+  Definition lev_src : val :=
+    λ: "x", lev "x".
+
+
+  Lemma lev_deep_memoized_refinement K (x y: val) :
+    src (fill K (lev_src y)) ∗ pair_imm_stringRel x y ⊢
+    SEQ (lev_mem x)
+    ⟨⟨ w, ∃ w', src (fill K (Val w')) ∗ natRel w w' ⟩⟩.
+  Proof using Sync Fin.
+    iIntros "[Hsrc Himm] Hna". iApply (rwp_take_step with "[Himm Hna] [Hsrc]"); first done; last first.
+    { iApply (step_pure_cred with "Hsrc"). apply: pure_step_ctx. rewrite /lev_src. apply: pure_exec_pure_step. done. }
+    simpl.
+    iIntros "[Hsrc Hc]". wp_rec. wp_bind ((let: "strlen" := mem_rec eq_heaplang strlen_template in mem_rec eq_pair (lev_template "strlen")))%E.
+    iApply (rwp_wand with "[Hc Hna]").
+    { iApply (lev_deep_memoized with "[Hc] Hna"). iDestruct "Hc" as "[Hc1 Hc2]". iFrame "Hc1 Hc2". }
+    iIntros (w) "[Hna Himpl]".
+    rewrite /tf_implements.
+    iSpecialize ("Himpl" $! _ _ 0 with "Himm Hsrc Hna").
+    iApply (rwp_wand with "Himpl").
+    iIntros (u) "[Hna Hrel]". iDestruct "Hrel" as (w') "[Hnat [_ [Hsrc _]]]".
+    iFrame. iExists _. iFrame.
+  Qed.
+
+
+
 End levenshtein.