Commit cb27171c authored by charguer's avatar charguer

demo hsimpl

parent 02c29695
......@@ -107,15 +107,28 @@ Relevant files:
(***********************************************************************)
(** Demo: [hsimpl] *)
(**
H1 \* (r ~~~> n) \* H2 \* H3 ==> H4 \* H5 \* (r ~~~> n) \* H6
(r ~~~> 3) \* (s ~~~> 4) ==> Hexists n, (r ~~~> n) \* (s ~~~> (n+1))
Lemma demo_hsimpl_1 : forall (H1 H2 H3 H4 H5 H6:hprop) r n,
H1 \* (r ~~~> n) \* H2 \* H3 ==> H4 \* H5 \* (r ~~~> n) \* H6.
Proof using.
intros.
hsimpl.
Abort.
(Hexists n, r ~~~> n \* \[n > 0]) ==> (Hexists m, r ~~~> (m+1) \* \[m >= 0])
Lemma demo_hsimpl_2 : forall r s,
(r ~~~> 3) \* (s ~~~> 4) ==> Hexists (n:int), (r ~~~> (n+1)) \* (s ~~~> (n+2)).
Proof using.
intros. dup 2.
{ hsimpl. admit. }
{ hsimpl 2. }
Abort.
*)
Lemma demo_hsimpl_3 : forall r,
(Hexists (n:int), r ~~~> n \* \[n > 0]) ==> (Hexists (m:int), r ~~~> (m+1) \* \[m >= 0]).
Proof using.
intros. hpull. intros n Hn.
hsimpl (n-1). math_rewrite (n-1+1 = n). hsimpl. math.
Abort.
(***********************************************************************)
......@@ -312,6 +325,45 @@ Definition val_incr_twice :=
ValFun 'p :=
val_incr 'p ;;
val_incr 'p.
(* EXERCISE: specify and verify [val_incr_twice] *)
(* SOLUTION *)
Lemma rule_incr_twice : forall p n,
......@@ -350,6 +402,50 @@ Lemma rule_val_example_one_ref : forall n,
\[]
(fun r => \[r = n+2]).
Proof using.
(* EXERCISE: complete proof *)
(* SOLUTION *)
xcf.
xapp. intros; subst.
......@@ -453,6 +549,43 @@ Lemma rule_push_front : forall L v p,
(MQueue L p)
(fun r => \[r = val_unit] \* MQueue (v::L) p).
Proof using.
(* EXERCISE: complete proof *)
(* SOLUTION *)
xcf. unfold MQueue. xpull ;=> pf pb vx vy.
xapps. xapp as r. intros x. intro_subst.
......@@ -469,7 +602,49 @@ Lemma rule_pop_front' : forall L v p x,
(MQueue (x::L) p)
(fun r => \[r = x] \* MQueue L p).
Proof using.
(** Hint: use [xapply] on the right instance of [rule_pop_front] *)
(* EXERCISE: complete proof
Hint: use [xapply] on [(@rule_pop_front ...)] *)
(* SOLUTION *)
intros. xapply (@rule_pop_front (x::L)).
{ auto_false. }
......@@ -481,6 +656,57 @@ Qed.
(***********************************************************************)
(** Challenge: queue transfer *)
(* EXERCISE: define and verify the function [val_transfer]
so that is satisfies:
Lemma rule_transfer : forall L1 L2 p1 p2,
triple (val_transfer p1 p2)
(MQueue L1 p1 \* MQueue L2 p2)
(fun r => \[r = val_unit] \* MQueue (L1 ++ L2) p1 \* MQueue nil p2).
Proof hints:
- use [hchange] on [MListSeg_cons_eq], [MListSeg_last],
[MListSeg_concat], and [MListSeg_nil].
- use [rew_list] to normalize list expressions
*)
Definition val_transfer :=
(* SOLUTION *)
......@@ -504,11 +730,6 @@ Lemma rule_transfer : forall L1 L2 p1 p2,
(MQueue L1 p1 \* MQueue L2 p2)
(fun r => \[r = val_unit] \* MQueue (L1 ++ L2) p1 \* MQueue nil p2).
Proof using.
(** Hints:
- use [hchange] on [MListSeg_cons_eq], [MListSeg_last],
[MListSeg_concat], and [MListSeg_nil].
- use [rew_list] to normalize list expressions *)
(* SOLUTION *)
xcf. xapps. xapps. xif ;=> C.
{ unfold MQueue. xpull ;=> pf2 pb2 vx2 vy2 pf1 pb1 vx1 vy1.
......@@ -595,6 +816,42 @@ Lemma Rule_incr2 : forall (p:loc) (n:int),
PRE (p ~~> n)
POST (fun (r:unit) => p ~~> (n+2)).
Proof using.
(* EXERCISE: complete proof *)
(* SOLUTION *)
xcf. xapps. xapps. hsimpl~. math.
(* /SOLUTION *)
......@@ -727,7 +984,6 @@ Lemma Rule_mlist_length : forall A `{EA:Enc A} (L:list A) (p:loc),
POST (fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
intros. gen p. induction_wf: list_sub_wf L; intros. xcf.
(* fold val_mlist_length *)
xapps~. xif ;=> C.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL. subst L.
xapps. xapps~ (IH L'). xchange (MList_cons p).
......@@ -767,6 +1023,39 @@ Lemma Rule_mlist_copy : forall p (L:list int),
PRE (p ~> MList L)
POST (fun (p':loc) => (p ~> MList L) \* (p' ~> MList L)).
Proof using.
(* EXERCISE: complete proof
Hints: use [MList_null_eq], [MList_not_null_inv_cons] and [MList_cons_eq] *)
(* SOLUTION *)
intros. gen p. induction_wf IH: list_sub_wf L. xcf.
xapps~. xif ;=> C.
......
......@@ -31,7 +31,7 @@ Ltac auto_star ::= jauto.
(** A formula is a binary relation relating a pre-condition
and a post-condition. *)
Definition Formula := forall A `{Enc A}, hprop -> (A -> hprop) -> Prop.
Definition Formula := forall A (EA:Enc A), hprop -> (A -> hprop) -> Prop.
Global Instance Inhab_Formula : Inhab Formula.
Proof using. apply (Inhab_of_val (fun _ _ _ _ => True)). Qed.
......@@ -195,7 +195,7 @@ Proof.
Qed.
Definition Sound_for (t:trm) (F:Formula) :=
forall `{EA:Enc A} H (Q:A->hprop), ^F H Q -> Triple t H Q.
forall A (EA:Enc A) H (Q:A->hprop), ^F H Q -> Triple t H Q.
Lemma Sound_for_Local : forall t (F:Formula),
Sound_for t F ->
......
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