Commit 16caa857 authored by charguer's avatar charguer

progress on example

parent 72357776
......@@ -120,9 +120,17 @@ Proof using.
iDestruct "H" as (q) "[??]". auto with iFrame.
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.
Arguments Box_fold : clear implicits.
Arguments Box_unfold : clear implicits.
Arguments RO_Box_unfold : clear implicits.
Arguments RO_Box_fold : clear implicits.
(*---*)
......@@ -131,16 +139,32 @@ Definition val_box_get :=
Let 'q := val_get 'p in
val_get 'q.
Tactic Notation "xletapp" constr(M) :=
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))
POST (fun r => \[r = val_int 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.
(* detailed proof (to keep somewhere for debugging):
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.
*)
(*---*)
......@@ -159,28 +183,151 @@ Definition val_box_twice :=
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)])) ->
(* to move to LamdaSepRo, next to rule_fix *)
Lemma rule_fun : forall x t1 H Q,
H ==> Q (val_fun x t1) ->
Normal H ->
triple (trm_fun x t1) H Q.
Proof using.
introv M HS. intros h1 h2 D P1. exists___. splits*.
{ applys red_fun. }
{ specializes M P1. applys~ on_rw_sub_base. }
Qed.
Lemma rule_let' : forall x t1 t2 H2 H1 H Q Q1,
H ==> (H1 \* H2) ->
triple t1 H1 Q1 ->
(forall (X:val), triple (subst x X t2) (Q1 X \* H2) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using. introv WP M1 M2. applys* rule_consequence WP. applys* rule_let. Qed.
Lemma rule_letfun : forall f x t1 t2 H Q,
(forall F, triple (subst f F t2) (\[F = val_fun x t1] \* H) Q) ->
triple (LetFun f x := t1 in t2) H Q.
Proof using.
introv M. applys rule_let' H (fun F => \[F = val_fun x t1]).
{ hsimpl. }
{ applys rule_fun. hsimpl~. typeclass. }
{ intros F. applys M. }
Qed.
Lemma rule_frame_read_only_conseq : forall t H1 Q1 H2 H Q,
H ==> (H1 \* H2) ->
Normal H1 ->
triple t (RO H1 \* H2) Q1 ->
(Q1 \*+ H1) ===> Q ->
triple t H Q.
Proof using.
introv WP M N WQ. applys* rule_consequence (rm WP) (rm WQ).
forwards~ R: rule_frame_read_only t H2 Q1 H1.
{ rewrite~ hstar_comm. } { rewrite~ hstar_comm. }
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)) ->
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. {
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 ->.
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. }
Qed.
math_rewrite (2 * F n = F n + F n)%Z. iApply Box_fold. iFrame. } *)
Admitted.
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 :=
Let 'a := val_box_get 'p in
'x '+ 'a in
Let 'u := val_box_twice 'f 'p in
val_box_get 'p.
(* ideally, ends with :
val_box_twice 'f 'p ;;;
val_box_get 'p.
but requires proving rule_seq, similar to rule_let.
*)
Tactic Notation "xletfun" :=
applys rule_letfun; simpl; xpull.
Tactic Notation "xdef'" := (* todo: this replaces xdef *)
rew_nary; rew_vals_to_trms;
match goal with |- triple (trm_apps (trm_val ?f) _) _ _ =>
match goal with
| H: f =_ |- _ =>
rew_nary in H;
applys rule_apps_funs;
[ applys H | auto | simpl ]
| |- _ =>
applys rule_apps_funs;
[ unfold f; rew_nary; reflexivity | auto | simpl ]
end
end.
Lemma rule_box_demo : forall (n:int),
triple (val_box_demo n)
PRE \[]
POST (fun r => \[r = val_int (4*n)]).
Proof using.
intros. xdef.
xletapp rule_ref => ? q ->.
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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment