proof using wp

model/LambdaCF.v

@@ -142,10 +142,10 @@ Proof using. applys (cf_unfold_iter 1). Qed.
 (* ---------------------------------------------------------------------- *)
 (* ** Soundness of the CF generator *)
 
-Lemma is_local_cf : forall T,
-  is_local (cf T).
+Lemma is_local_cf : forall t,
+  is_local (cf t).
 Proof.
-  intros. rewrite cf_unfold. destruct T; try apply is_local_local.
+  intros. rewrite cf_unfold. destruct t; try apply is_local_local.
 Qed.
 
 Definition sound_for (t:trm) (F:formula) :=

model/LambdaExtra.v

@@ -3589,3 +3589,102 @@ Proof using.
 Qed.
 
 ---
+
+
+
+
+(* todo: already exist under different names 
+
+Lemma hexists_weaken : forall A (J J' : A -> hprop),
+  J ===> J' ->
+  hexists J ==> hexists J'.
+Proof using. introv W. intros h (x&Hh). exists x. applys* W. Qed.
+
+Lemma hforall_weaken : forall A (J J' : A -> hprop),
+  J ===> J' ->
+  hforall J ==> hforall J'.
+Proof using. introv W. intros h Hh x. applys* W. Qed.
+
+Lemma hwand_extend : forall H3 H1 H2,
+  (H1 \--* H2) \* H3 ==> (H1 \--* (H2 \* H3)).
+Proof using. intros. unfold hwand. hpull ;=> H4 M. hsimpl. hchanges M. Qed.
+
+Arguments hwand_extend : clear implicits.
+
+*)
+
+(* false if H1 is not habited
+Lemma hwand_same_part : forall H1 H2 H3,
+  (H1 \* H2 \--* H1 \* H3) ==> (H2 \--* H3).
+Proof using. intros. unfold hwand. hpull ;=> H4 M. hsimpl. 
+
+
+Lemma regular_regular_transformer : forall F,
+  regular (regular_transformer F).
+Proof using.
+  intros F H Q Q' M.
+  unfold regular_transformer.
+  do 2 hchange hstar_hforall. rew_heap.
+  unfolds hforall. simpl. intros h Hh H'.
+  specializes Hh (H \* H'). hhsimpl.
+  hchanges (hwand_cancel_part H (H' \* \Top) (F (Q \*+ (H \* H')))).  
+  rewrite (hstar_comm H' \Top).
+  apply hwand_move_part_r.
+  rewrite <- hstar_assoc. rewrite htop_hstar_htop. 
+  asserts_rewrite (Q \*+ (H \* H') = (fun x : val => (Q x \* H) \* H')).
+  { apply fun_ext_1. intros x. rewrite~ hstar_assoc. }
+
+  pattern \Top at 3; rewrite <- 
+
+  applys himpl_trans. Focus 2. applys hwand_move_part_l. 
+
+  hchanges (hwand_cancel_part \Top (H' \* \Top) (F (Q \*+ (H \* H')))).  
+  
+  hchange (hwand_extend \Top (H' \* \Top) (F (Q \*+ (H \* H')))). rew_heap.
+
+ 
+  hchanges (hwand_extend (H \* \Top) (H \* H' \* \Top) (F (Q \*+ (H \* H')))).
+  hchanges (
+
+Lemma hwand_cancel_part : forall H1 H2 H3,
+  H1 \* ((H1 \* H2) \--* H3) ==> (H2 \--* H3).
+
+
+  do 2 hchange hstar_hforall. rew_heap.
+  applys hforall_weaken. intros H'.
+  hsimpl.
+  unfold hforall.
+  intros h Hh.
+Qed.
+
+
+Lemma regular_weaken : forall Q' F H Q,
+  regular F ->
+  H ==> F Q ->
+  Q ===> Q' ->
+  H ==> F Q'.
+Proof using.
+  introv R M W. hchanges M. forwards~ N: R \[] W. hchanges N.
+Qed.
+
+Lemma regular_frame_top : forall H1 H2 F H Q,
+  regular F ->
+  H ==> H1 \* H2 \* \Top ->
+  H1 ==> F (fun x => H2 \--* Q x) -> (* todo: notation *)
+  H ==> F Q.
+Proof using.
+  introv R W M. hchanges W. hchanges M.
+  forwards~ N: R H2 (fun x : val => H2 \--* Q x). hsimpl. hchanges N.
+  applys~ regular_weaken. intros x. hchanges (hwand_cancel H2).
+Qed.
+
+Lemma regular_frame : forall H1 H2 F H Q,
+  regular F ->
+  H ==> H1 \* H2 ->
+  H1 ==> F (fun x => H2 \--* Q x) ->
+  H ==> F Q.
+Proof using.
+  introv R W M. applys~ regular_frame_top H1 H2. { hchanges W. } 
+Qed.
+
+*)
\ No newline at end of file

model/LambdaWP.v

@@ -55,6 +55,61 @@ Definition is_local (F:formula) :=
 (* ---------------------------------------------------------------------- *)
 (* ** Properties of [local] for WP *)
 
+(** The [local] operator can be freely erased from a conclusion *)
+
+Lemma local_erase : forall F Q,
+  F Q ==> local F Q.
+Proof using.
+  intros. unfold local. hsimpl. hchanges (qwand_of_qimpl Q). hsimpl.
+Qed.
+
+(** [local] is a covariant transformer w.r.t. predicate inclusion *)
+
+Lemma local_weaken_body : forall F F',
+  F ===> F' ->
+  local F ===> local F'.
+Proof using.
+  unfold local. introv M. intros Q. hpull ;=> Q'. hsimpl~ Q'.
+Qed.
+
+(** [local] is idempotent, i.e. nested applications
+   of [local] are redundant *)
+
+(* TODO: move *)
+Lemma hstar_qwand : forall A (Q1 Q2:A->hprop) H,
+  (Q1 \---* Q2) \* H ==> Q1 \---* (Q2 \*+ H).
+Proof using.
+  intros. unfold qwand. hchanges hstar_hforall.
+  applys himpl_hforall. intros x.
+  hchanges hstar_hwand.
+Qed.
+
+Arguments hstar_hwand : clear implicits.
+Arguments hstar_qwand [A]. (* H should be first *)
+
+
+Lemma local_local : forall F,
+  local (local F) = local F.
+Proof using.
+  intros F. applys fun_ext_1. intros Q. applys himpl_antisym.
+  { unfold local. hpull ;=> Q' Q''. hsimpl Q''.
+    hchanges hstar_qwand. applys qwand_himpl_r. 
+    intros x.
+    hchanges (qwand_himpl_hwand x Q' (Q \*+ \Top)).
+    hchanges (hwand_cancel (Q' x) (Q x \* \Top)). }
+  { hchanges local_erase. }
+Qed.
+
+(** A definition whose head is [local] satisfies [is_local] *)
+
+Lemma is_local_local : forall F,
+  is_local (local F).
+Proof using. intros. unfolds. rewrite~ local_local. Qed.
+
+
+(* ---------------------------------------------------------------------- *)
+(* ** Elimination rules for [local] for WP *)
+
 Lemma local_weaken : forall Q' F H Q,
   is_local F ->
   H ==> F Q ->
@@ -178,10 +233,6 @@ Proof using.
   destruct t; fequals.
   { fequals~. }
   { fequals~. }
-  { fequals~. }
-  { fequals~. }
-  { fequals~. }
-  { fequals~. }
   { fequals~. applys~ fun_ext_1. }
   (*
   { fequals~. }
@@ -201,12 +252,37 @@ Proof using. applys (WP_unfold_iter 1). Qed.
 (* ---------------------------------------------------------------------- *)
 (* ** Soundness of the WP generator *)
 
+Lemma is_local_cf : forall t,
+  is_local (WP t).
+Proof.
+  intros. rewrite WP_unfold. destruct t; try apply is_local_local.
+Qed.
+
+Definition sound_for (t:trm) (F:formula) :=
+  forall H Q, (H ==> F Q) -> triple t H Q.
+
+Lemma sound_for_local : forall t (F:formula),
+  sound_for t F ->
+  sound_for t (local F).
+Proof using.
+  unfold sound_for. introv SF. intros H Q M.
+  rewrite is_local_triple. unfold SS.local.
+  hchange M. unfold local. hpull ;=> Q'.
+  hsimpl (F Q') ((Q' \---* Q \*+ \Top)) Q'. split.
+  { applys~ SF. }
+  { hchanges qwand_cancel. }
+Qed.
+
+(* ---------------------------------------------------------------------- *)
+(* ** Soundness of the WP generator *)
+
 Lemma triple_of_WP : forall (t:trm) H Q,
   H ==> WP t Q -> 
   triple t H Q.
 Proof using.
   intros t. induction_wf: trm_size t.
-  rewrite WP_unfold. destruct t; simpl; intros H Q P.
+  rewrite WP_unfold. destruct t; simpl; 
+    try (applys sound_for_local; intros H Q P).
   { unfolds WP_val. applys~ rule_val. }
   { unfolds WP_fail. xchanges P. intros; false. }
   { unfolds WP_val. applys~ rule_fun. }
@@ -269,44 +345,44 @@ Qed.
 (* ** Notation for computd WP *)
 
 Notation "'`Val' v" :=
-  (WP_val v)
+  (local (WP_val v))
   (at level 69) : charac.
 
 Notation "'`LetIf' F0 'Then' F1 'Else' F2" :=
-  (WP_if F0 F1 F2)
+  (local (WP_if F0 F1 F2))
   (at level 69, F0 at level 0) : charac.
 
 Notation "'`If' v 'Then' F1 'Else' F2" :=
-  (WP_if_val v F1 F2)
+  (local (WP_if_val v F1 F2))
   (at level 69) : charac.
 
 Notation "'`Seq' F1 ;;; F2" :=
-  (WP_seq F1 F2)
+  (local (WP_seq F1 F2))
   (at level 68, right associativity,
    format "'[v' '`Seq'  '[' F1 ']'  ;;;  '/'  '[' F2 ']' ']'") : charac.
 
 Notation "'`Let' x ':=' F1 'in' F2" :=
-  (WP_let F1 (fun x => F2))
+  (local (WP_let F1 (fun x => F2)))
   (at level 69, x ident, right associativity,
   format "'[v' '[' '`Let'  x  ':='  F1  'in' ']'  '/'  '[' F2 ']' ']'") : charac.
 
 Notation "'`App' t " :=
-  (triple t)
+  (local (triple t))
   (at level 68, t at level 0) : charac.
 
 Notation "'`Fail'" :=
-  (WP_fail)
+  (local (WP_fail))
   (at level 69) : charac.
 
 (*
 Notation "'`While' F1 'Do' F2 'Done'" :=
-  (WP_while F1 F2)
+  (local (WP_while F1 F2))
   (at level 69, F2 at level 68,
    format "'[v' '`While'  F1  'Do'  '/' '[' F2 ']' '/'  'Done' ']'")
    : charac.
 
 Notation "'`For' x '=' v1 'To' v2 'Do' F3 'Done'" :=
-  (WP_for v1 v2 (fun x => F3))
+  (local (WP_for v1 v2 (fun x => F3)))
   (at level 69, x ident, (* t1 at level 0, t2 at level 0, *)
    format "'[v' '`For'  x  '='  v1  'To'  v2  'Do'  '/' '[' F3 ']' '/'  'Done' ']'")
   : charac.
@@ -421,146 +497,56 @@ Definition val_incr :=
     Let 'm := 'n '+ 1 in
     val_set 'p 'm.
 
-
-
-(* TODO: rename to "local" or "regular" *)
-
-Definition regular_transformer (F:formula) :=
-  fun Q => hforall (fun H => (H \* \Top) \--* F (Q \*+ H)).
-
-Definition regular_transformer'(F:formula) :=
-  fun Q => hforall (fun H => hforall (fun Q' => 
-      \[Q ===> Q'] \--* (H \* \Top) \--* F (Q' \*+ H))).
-
-
-
-(* TODO rename to is_regular *)
-
-Definition regular (F:formula) :=
-  forall H Q Q', Q ===> Q' -> (F Q \* H \* \Top ==> F (Q' \*+ H)).
-
-
-Lemma hexists_weaken : forall A (J J' : A -> hprop),
-  J ===> J' ->
-  hexists J ==> hexists J'.
-Proof using. introv W. intros h (x&Hh). exists x. applys* W. Qed.
-
-Lemma hforall_weaken : forall A (J J' : A -> hprop),
-  J ===> J' ->
-  hforall J ==> hforall J'.
-Proof using. introv W. intros h Hh x. applys* W. Qed.
-
-
-Lemma hwand_extend : forall H3 H1 H2,
-  (H1 \--* H2) \* H3 ==> (H1 \--* (H2 \* H3)).
-Proof using. intros. unfold hwand. hpull ;=> H4 M. hsimpl. hchanges M. Qed.
-
-Arguments hwand_extend : clear implicits.
-
-(* false if H1 is not habited
-Lemma hwand_same_part : forall H1 H2 H3,
-  (H1 \* H2 \--* H1 \* H3) ==> (H2 \--* H3).
-Proof using. intros. unfold hwand. hpull ;=> H4 M. hsimpl. 
-*)
-
-Lemma regular_regular_transformer : forall F,
-  regular (regular_transformer F).
+Lemma local_erase' : forall H F Q,
+  H ==> F Q ->
+  H ==> local F Q.
 Proof using.
-  intros F H Q Q' M.
-  unfold regular_transformer.
-  do 2 hchange hstar_hforall. rew_heap.
-  unfolds hforall. simpl. intros h Hh H'.
-  specializes Hh (H \* H'). hhsimpl.
-  hchanges (hwand_cancel_part H (H' \* \Top) (F (Q \*+ (H \* H')))).  
-  rewrite (hstar_comm H' \Top).
-  apply hwand_move_part_r.
-  rewrite <- hstar_assoc. rewrite htop_hstar_htop. 
-  asserts_rewrite (Q \*+ (H \* H') = (fun x : val => (Q x \* H) \* H')).
-  { apply fun_ext_1. intros x. rewrite~ hstar_assoc. }
-
-  pattern \Top at 3; rewrite <- 
-
-  applys himpl_trans. Focus 2. applys hwand_move_part_l. 
-
-  hchanges (hwand_cancel_part \Top (H' \* \Top) (F (Q \*+ (H \* H')))).  
-  
-  hchange (hwand_extend \Top (H' \* \Top) (F (Q \*+ (H \* H')))). rew_heap.
-
- 
-  hchanges (hwand_extend (H \* \Top) (H \* H' \* \Top) (F (Q \*+ (H \* H')))).
-  hchanges (
-
-Lemma hwand_cancel_part : forall H1 H2 H3,
-  H1 \* ((H1 \* H2) \--* H3) ==> (H2 \--* H3).
-
-
-  do 2 hchange hstar_hforall. rew_heap.
-  applys hforall_weaken. intros H'.
-  hsimpl.
-  unfold hforall.
-  intros h Hh.
+  introv M. hchanges M. applys local_erase.
 Qed.
 
 
-Lemma regular_weaken : forall Q' F H Q,
-  regular F ->
-  H ==> F Q ->
-  Q ===> Q' ->
-  H ==> F Q'.
+Lemma xlet_lemma : forall Q1 (F1:formula) (F2:val->formula) H Q,
+  is_local F1 ->
+  H ==> F1 Q1 ->
+  (forall X, Q1 X ==> F2 X Q) ->
+  H ==> local (WP_let F1 F2) Q.
 Proof using.
-  introv R M W. hchanges M. forwards~ N: R \[] W. hchanges N.
+  introv L M1 M2. applys local_erase'.
+  unfold WP_let. applys~ local_weaken M1.
 Qed.
 
-Lemma regular_frame_top : forall H1 H2 F H Q,
-  regular F ->
-  H ==> H1 \* H2 \* \Top ->
-  H1 ==> F (fun x => H2 \--* Q x) -> (* todo: notation *)
-  H ==> F Q.
-Proof using.
-  introv R W M. hchanges W. hchanges M.
-  forwards~ N: R H2 (fun x : val => H2 \--* Q x). hsimpl. hchanges N.
-  applys~ regular_weaken. intros x. hchanges (hwand_cancel H2).
-Qed.
+Ltac xlet_core tt ::=
+  applys xlet_lemma; [ try apply is_local_local | | ].
 
-Lemma regular_frame : forall H1 H2 F H Q,
-  regular F ->
-  H ==> H1 \* H2 ->
-  H1 ==> F (fun x => H2 \--* Q x) ->
-  H ==> F Q.
-Proof using.
-  introv R W M. applys~ regular_frame_top H1 H2. { hchanges W. } 
+Lemma xapp_lemma : forall t H Q,
+  triple t H Q ->
+  H ==> local (wp (triple t)) Q.
+Proof using. 
+  introv M. applys local_erase'. unfold wp. hsimpl~ H.
 Qed.
 
+Ltac xapp_core tt ::=
+  applys xapp_lemma.
+
 
-(*
 
-Lemma xlet_lemma : forall Q1 (F1:formula) (F2:val->formula) H Q,
-  regular F1 ->
-  H ==> F1 Q1 ->
-  (forall X, Q1 X ==> F2 X Q) ->
-  H ==> (WP_let F1 F2) Q.
-Proof using.
-  intros. unfold WP_let.
-Qed.
 
-Lemma rule_incr_3 : forall (p:loc) (n:int),
+Lemma rule_incr : forall (p:loc) (n:int),
   triple (val_incr p)
     (p ~~~> n)
     (fun r => \[r = val_unit] \* (p ~~~> (n+1))).
 Proof using.
   intros. xcf.
-  
-  { applys local_erase. xapplys rule_get. }
-  intros x. xpull. intros E. subst.
-  applys local_erase. esplit. split.
-  { applys local_erase. xapplys rule_add. }
-  intros y. xpull. intros E. subst.
-  applys local_erase. xapplys rule_set. auto.
-Qed.
-
+  xlet. { xapp. xapplys rule_get. }
+  intros x. hpull ;=> E. subst.
+  xlet. { xapp. xapplys rule_add. }
+  intros y. hpull ;=> E. subst.
+  xapp. xapplys rule_set. auto.
+Qed. (* woouha *)
 
 
 
+(* ===================
 
 
 (* ---------------------------------------------------------------------- *)

model/Makefile

@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
 # Compilation.
 
 # Note: double space below is important for export.sh
-SRC  := TLCbuffer Fmap SepFunctor SepTactics SepGPM LambdaSemantics LambdaSep LambdaSepProofMode LambdaCF LambdaCFTactics LambdaStruct ExampleListProofMode LambdaSepRO ExampleROProofMode  LambdaSepCredits   LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList  LambdaCFCredits  ExampleRO  ExampleListProofMode
+SRC  := TLCbuffer Fmap SepFunctor SepTactics SepGPM LambdaSemantics LambdaSep LambdaSepProofMode LambdaCF LambdaCFTactics LambdaWP LambdaStruct ExampleListProofMode LambdaSepRO ExampleROProofMode  LambdaSepCredits   LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList  LambdaCFCredits  ExampleRO  ExampleListProofMode
 
 # LambdaCFRO