Solve Admits.

model/ExampleROProofMode.v

@@ -122,10 +122,7 @@ Qed.
 
 Lemma RO_Box_fold : forall p q n,
   RO (p ~~~> q \* q ~~~> n) ==> RO (p ~> Box n).
-Proof using.
-  intros. xunfold Box. rewrite RO_hexists. hsimpl.
-  (* TODO: use proof mode *)
-Qed.
+Proof using. iIntros (???) "?". xunfold Box. by iExists _. Qed.
 
 Arguments Box_fold : clear implicits.
 Arguments Box_unfold : clear implicits.
@@ -140,13 +137,10 @@ Definition val_box_get :=
     val_get 'q.
 
 Tactic Notation "xletapp" constr(M) :=
-  ram_apply_let M; 
-  [ solve [ auto 20 with iFrame ] 
+  ram_apply_let M;
+  [ solve [ auto 20 with iFrame ]
   | unlock; xpull; simpl ].
 
-Tactic Notation "xapp" constr(M) :=
-  apply rule_htop_post; ram_apply M.
-
 Lemma rule_box_get : forall p n,
   triple (val_box_get p)
     PRE (RO (p ~> Box n))
@@ -154,9 +148,8 @@ Lemma rule_box_get : forall p n,
 Proof using.
   intros. xdef. xchanges (RO_Box_unfold p) ;=> q.
   xletapp rule_get_ro => ? ->.
-  xapp rule_get_ro.
-  iIntros. iFrame. iIntros. admit. (* TODO: complete proof *)
-Qed.
+  ram_apply rule_get_ro. admit. (* TODO: complete proof *)
+Admitted.
 
   (* detailed proof (to keep somewhere for debugging):
   intros. xdef. xchange (RO_Box_unfold p). xpull ;=> q.
@@ -227,9 +220,9 @@ Qed.
 Arguments RO_Box_fold : clear implicits.
 
 Lemma rule_box_twice : forall (F:int->int) n (f:val) p,
-  (forall (x:int) (H:hprop), triple (f x)
-      PRE (RO(p ~> Box n) \* H)
-      POST (fun r => \[r = val_int (F x)] \* H)) ->
+  (forall (x:int), triple (f x)
+      PRE (RO(p ~> Box n))
+      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)).
@@ -237,44 +230,28 @@ Proof using.
   introv M. xdef. xchange (Box_unfold p). xpull ;=> q.
   xletapp rule_get_ro => ? ->.
   xletapp rule_get_ro => ? ->.
-  (* details of above: 
-     ram_apply_let rule_get_ro. { auto with iFrame. }
-     unlock. move=>? /=. xpull=>->. *)
-  applys rule_let' __ (q ~~~> n \* p ~~~> q). hsimpl.
-  { applys rule_frame_read_only_conseq (q ~~~> n \* p ~~~> q).
-    { hsimpl. }
-    { typeclass. }
-    { xchange (RO_Box_fold p q n). rewrite hstar_comm. hsimpl.
-      applys M. }
-    { applys refl_rel_incl'. } }
-  xpull => /= a1 ->. 
+  ram_apply_let M.
+  { rewrite -RO_Box_fold. iIntros "Hq Hp". iCombine "Hp Hq" as "H".
+    auto with iFrame. }
+  unlock. xpull => /= a1 ->.
   xletapp rule_get_ro => ? ->.
-  applys rule_let' __ (q ~~~> n \* p ~~~> q). hsimpl.
-  { applys rule_frame_read_only_conseq (q ~~~> n \* p ~~~> q).
-    { hsimpl. }
-    { typeclass. }
-    { xchange (RO_Box_fold p q n). rewrite hstar_comm. hsimpl.
-      applys M. }
-    { applys refl_rel_incl'. } }
-  xpull => /= a2 ->.
-  xletapp rule_add => ? ->. 
-  xapp rule_set. 
- admit.
-  (* todo {
-    iIntros "$ Hp !> % -> Hq". iSplitR; [done|].
-    math_rewrite (2 * F n = F n + F n)%Z. iApply Box_fold. iFrame. } *)
-Admitted.
+  ram_apply_let M.
+  { rewrite -RO_Box_fold. iIntros "Hq Hp". iCombine "Hp Hq" as "H".
+    auto with iFrame. }
+  unlock. xpull => /= a2 ->.
+  xletapp rule_add => ? ->.
+  ram_apply rule_set.
+  iIntros "Hp $ !> % -> Hq". iSplitR; [done|]. iApply Box_fold. iFrame.
+  by math_rewrite (2 * F n = F n + F n)%Z.
+Qed.
 
 Arguments rule_box_twice : clear implicits.
 
-
-
-
 Definition val_box_demo :=
   ValFun 'n :=
     Let 'q := val_ref 'n in
     Let 'p := val_ref 'q in
-    LetFun 'f 'x := 
+    LetFun 'f 'x :=
       Let 'a := val_box_get 'p in
       'x '+ 'a in
     Let 'u := val_box_twice 'f 'p in
@@ -286,7 +263,6 @@ Definition val_box_demo :=
   but requires proving rule_seq, similar to rule_let.
 *)
 
-
 Tactic Notation "xletfun" :=
   applys rule_letfun; simpl; xpull.
 
@@ -304,9 +280,6 @@ Tactic Notation "xdef'" := (* todo: this replaces xdef *)
   end
  end.
 
-
-
-
 Lemma rule_box_demo : forall (n:int),
   triple (val_box_demo n)
     PRE \[]
@@ -317,17 +290,15 @@ Proof using.
   xletapp rule_ref => ? p ->.
   xletfun => F HF.
   ram_apply_let (rule_box_twice (fun (x:int) => (x + n)%Z) n).
-  { intros. xdef'. clear HF.
-    xletapp rule_box_get => m ->.
-    xapp rule_add. { iIntros. iFrame. admit. (* todo *) } }
-  { admit. (* todo *) }
-  { intros u. simpl.  (* auto *)
-    instantiate (1 := (fun (u:val) => p ~> Box (4*n))). 
-    xapp rule_box_get.  { admit. } (* todo *) }
-Admitted.
-
-
-
-
+  { intros. xdef'. xletapp rule_box_get => m ->.
+    ram_apply rule_add. { iIntros. admit. (* todo *) } }
+  { iIntros "Hq Hp". iDestruct (Box_fold with "[$Hq $Hp]") as "$".
+    auto with iFrame. }
+  unlock. xpull=> u /= _. ram_apply rule_box_get.
 
+assert (forall x, Normal (p ~> Box x)). admit.
 
+math_rewrite (2 * (n + n) = 4 * n)%Z.
+iIntros "$".
+admit.
+Qed.

model/LambdaSepRO.v

@@ -1791,10 +1791,11 @@ Proof.
   apply bi.forall_elim.
 Qed.
 
-Instance ROFrame_from_sep (P Q : hprop) : FromSep (ROFrame P Q) P Q.
+(* We do not wnad this instance to be picked by iCombine => low priority. *)
+Instance ROFrame_from_sep (P Q : hprop) : FromSep (ROFrame P Q) P Q | 1000.
 Proof. apply ROFrame_intro. Qed.
 Instance ROFrame_from_and (P Q : hprop) :
-  FromAnd (P ∗ Q) P Q → FromAnd (ROFrame P Q) P Q.
+  FromAnd (P ∗ Q) P Q → FromAnd (ROFrame P Q) P Q | 1000.
 Proof. rewrite /FromAnd=>->. apply ROFrame_intro. Qed.
 
 (** Frame instances *)