Progress on ExampleROProofMode.v

model/ExampleROProofMode.v

@@ -47,6 +47,13 @@ Hint Resolve var_funs_exec_elim.
 (* ********************************************************************** *)
 (* * Formalisation of higher-order iterator on a reference *)
 
+Tactic Notation "xdef" :=
+  rew_nary; rew_vals_to_trms;
+  match goal with |- triple (trm_apps (trm_val ?f) _) _ _ =>
+   applys rule_apps_funs;
+   [unfold f; rew_nary; reflexivity | auto | simpl]
+  end.
+
 (* ---------------------------------------------------------------------- *)
 (** Apply a function to the contents of a reference *)
 
@@ -64,10 +71,7 @@ Lemma rule_ref_apply : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
     PRE (RO(p ~~~> v) \* H)
     POST Q).
 Proof using.
-  introv M.
-  rew_nary; rew_vals_to_trms; applys rule_apps_funs;
-    [unfold val_ref_apply; rew_nary; reflexivity| auto | simpl].
-  ram_apply_let rule_get_ro. { auto with iFrame. }
+  introv M. xdef. ram_apply_let rule_get_ro. { auto with iFrame. }
   move=>X /=. unlock. xpull=>->. done.
 Qed.
 
@@ -90,10 +94,93 @@ Lemma rule_ref_update : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
     PRE (p ~~~> v \* H)
     POST (fun r => \[r = val_unit] \* Hexists w, (p ~~~> w) \* (Q w))).
 Proof using.
-  introv N M.
-  rew_nary; rew_vals_to_trms; applys rule_apps_funs;
-    [unfold val_ref_update; rew_nary; reflexivity| auto | simpl].
-  ram_apply_let rule_get_ro. { auto with iFrame. }
+  introv N M. xdef. ram_apply_let rule_get_ro. { auto with iFrame. }
   unlock. move=>x /=. xpull=>->. ram_apply_let M. { auto with iFrame. }
   unlock. move=>y /=. ram_apply rule_set. { auto 10 with iFrame. }
 Qed.
+
+(* ---------------------------------------------------------------------- *)
+(** In-place update of a reference by invoking a function, with representation predicate  *)
+
+Definition Box (n:int) (p:loc) :=
+  Hexists (q:loc), (p ~~~> q) \* (q ~~~> n).
+
+Lemma Box_unfold : forall p n,
+  (p ~> Box n) ==> Hexists (q:loc), (p ~~~> q) \* (q ~~~> n).
+Proof using. xunfold Box. auto. Qed.
+
+Lemma Box_fold : forall p q n,
+  (p ~~~> q) \* (q ~~~> n) ==> (p ~> Box n).
+Proof using. xunfold Box. auto. Qed.
+
+Lemma RO_Box_unfold : forall p n,
+  RO (p ~> Box n) ==> RO (p ~> Box n) \* Hexists (q:loc), RO (p ~~~> q) \* RO (q ~~~> n).
+Proof using.
+  iIntros (p n) "H". iDestruct (RO_duplicatable with "H") as "[$ H]". xunfold Box.
+  iDestruct "H" as (q) "[??]". auto with iFrame.
+Qed.
+
+Arguments Box_fold : clear implicits.
+Arguments Box_unfold : clear implicits.
+Arguments RO_Box_unfold : clear implicits.
+
+(*---*)
+
+Definition val_box_get :=
+  ValFun 'p :=
+    Let 'q := val_get 'p in
+    val_get 'q.
+
+Lemma rule_box_get : forall p n,
+  triple (val_box_get p)
+    PRE (RO (p ~> Box n))
+    POST (fun r => \[r = val_int n]).
+Proof using.
+  intros. xdef. xchange (RO_Box_unfold p). xpull ;=> q.
+  ram_apply_let rule_get_ro. { auto with iFrame. }
+  unlock. move=>/= ?. xpull=> ->. apply rule_htop_post.
+  ram_apply rule_get_ro. { iIntros. iFrame. iIntros. admit. }
+Qed.
+
+(*---*)
+
+(* let box_twice f p =
+      let q = !p in
+      q := f !q + f !q
+*)
+
+Definition val_box_twice :=
+  ValFun 'f 'p :=
+    Let 'q := val_get 'p in
+    Let 'n1 := val_get 'q in
+    Let 'a1 := 'f 'n1 in
+    Let 'n2 := val_get 'q in
+    Let 'a2 := 'f 'n2 in
+    Let 'm := 'a1 '+ 'a2 in
+    val_set 'q 'm.
+
+Lemma rule_box_twice : forall (f:val) p n (F:int->int),
+  (forall (x:int), triple (f x)
+      PRE (\[])
+      POST (fun r => \[r = val_int (F x)])) ->
+  triple (val_box_twice f p)
+    PRE (p ~> Box n)
+    POST (fun r => \[r = val_unit] \* p ~> Box (2 * F n)).
+Proof using.
+  introv M. xdef. xchange (Box_unfold p). xpull ;=> q.
+  ram_apply_let rule_get_ro. { auto with iFrame. }
+  unlock. move=>? /=. xpull=>->.
+  ram_apply_let rule_get_ro. { auto with iFrame. }
+  unlock. move=>? /=. xpull=>->.
+  ram_apply_let M. { auto with iFrame. }
+  unlock. move=>? /=. xpull=>->.
+  ram_apply_let rule_get_ro. { auto with iFrame. }
+  unlock. move=>? /=. xpull=>->.
+  ram_apply_let M. { auto with iFrame. }
+  unlock. move=>? /=. xpull=>->.
+  ram_apply_let rule_add. { auto with iFrame. }
+  unlock. move=>? /=. xpull=>->.
+  ram_apply rule_set. {
+    iIntros "$ Hp !> % -> Hq". iSplitR; [done|].
+    math_rewrite (2 * F n = F n + F n)%Z. iApply Box_fold. iFrame. }
+Qed.