Commit 3966de5d authored by charguer's avatar charguer

wp_while

parent b10b958e
......@@ -168,34 +168,34 @@ Qed.
(** These auxiliary definitions give the characteristic formula
associated with each term construct. *)
Definition WP_fail : formula := fun Q =>
Definition wp_fail : formula := fun Q =>
\[False].
Definition WP_val (v:val) : formula := fun Q =>
Definition wp_val (v:val) : formula := fun Q =>
Q v.
Definition WP_seq (F1 F2:formula) : formula := fun Q =>
Definition wp_seq (F1 F2:formula) : formula := fun Q =>
F1 (fun r => \[r = val_unit] \* F2 Q).
Definition WP_let (F1:formula) (F2of:val->formula) : formula := fun Q =>
Definition wp_let (F1:formula) (F2of:val->formula) : formula := fun Q =>
F1 (fun X => F2of X Q).
Definition WP_if_val (v:val) (F1 F2:formula) : formula := fun Q =>
Hexists (b:bool), \[v = val_bool b] \* (If b then F1 Q else F2 Q).
Definition wp_if_val (v:val) (F1 F2:formula) : formula := fun Q =>
Hexists (b:bool), \[v = val_bool b] \* (if b then F1 Q else F2 Q).
Definition WP_if (F0 F1 F2 : formula) : formula :=
WP_let F0 (fun v => WP_if_val v F1 F2).
Definition wp_if (F0 F1 F2 : formula) : formula :=
wp_let F0 (fun v => local (wp_if_val v F1 F2)).
Definition WP_while (F1 F2:formula) : formula := fun Q =>
Definition wp_while (F1 F2:formula) : formula := fun Q =>
Hforall (R:formula),
let F := (local (WP_if F1 (local (WP_seq F2 R)) (local (WP_val val_unit)))) in
let F := (local (wp_if F1 (local (wp_seq F2 R)) (local (wp_val val_unit)))) in
\[ is_local R /\ F ===> R] \--* (R Q).
Definition WP_for (v1 v2:val) (F3:int->formula) : formula := fun Q =>
Definition wp_for (v1 v2:val) (F3:int->formula) : formula := fun Q =>
Hexists n1 n2, \[v1 = val_int n1 /\ v2 = val_int n2] \*
Hforall (S:int->formula),
let F i := local (If (i <= n2) then (WP_seq (F3 i) (S (i+1)))
else (WP_val val_unit)) in
let F i := local (If (i <= n2) then (wp_seq (F3 i) (S (i+1)))
else (wp_val val_unit)) in
\[ is_local_pred S /\ (forall i, F i ===> S i)] \--* (S n1 Q).
......@@ -203,48 +203,52 @@ Definition WP_for (v1 v2:val) (F3:int->formula) : formula := fun Q =>
(* ** Definition of the CF generator *)
(** The CF generator is a recursive function, defined using the
optimal fixed point combinator (from TLC). [WP_def] gives the
function, and [cf] is then defined as the fixpoint of [WP_def].
optimal fixed point combinator (from TLC). [wp_def] gives the
function, and [cf] is then defined as the fixpoint of [wp_def].
Subsequently, the fixed-point equation is established. *)
Definition WP_def WP (t:trm) :=
Definition wp_def wp (t:trm) :=
match t with
| trm_val v => local (WP_val v)
| trm_var x => local (WP_fail) (* unbound variable *)
| trm_fun x t1 => local (WP_val (val_fun x t1))
| trm_fix f x t1 => local (WP_val (val_fix f x t1))
| trm_if t0 t1 t2 => local (WP_if (WP t0) (WP t1) (WP t2))
| trm_seq t1 t2 => local (WP_seq (WP t1) (WP t2))
| trm_let x t1 t2 => local (WP_let (WP t1) (fun X => WP (subst x X t2)))
| trm_val v => local (wp_val v)
| trm_var x => local (wp_fail) (* unbound variable *)
| trm_fun x t1 => local (wp_val (val_fun x t1))
| trm_fix f x t1 => local (wp_val (val_fix f x t1))
| trm_if t0 t1 t2 => local (wp_if (wp t0) (wp t1) (wp t2))
| trm_seq t1 t2 => local (wp_seq (wp t1) (wp t2))
| trm_let x t1 t2 => local (wp_let (wp t1) (fun X => wp (subst x X t2)))
| trm_app t1 t2 => local (weakestpre (triple t))
| trm_while t1 t2 => local (WP_fail) (* TODO *)
| trm_for x t1 t2 t3 => local (WP_fail) (* TODO *)
| trm_while t1 t2 => local (wp_while (wp t1) (wp t2))
| trm_for x t1 t2 t3 => local (
match t1, t2 with
| trm_val v1, trm_val v2 => local (wp_for v1 v2 (fun X => wp (subst x X t3)))
| _, _ => wp_fail
end)
end.
Definition WP := FixFun WP_def.
Definition wp := FixFun wp_def.
Ltac fixfun_auto := try solve [
try fequals; auto; try apply fun_ext_1; auto ].
Lemma WP_unfold_iter : forall n t,
WP t = func_iter n WP_def WP t.
Lemma wp_unfold_iter : forall n t,
wp t = func_iter n wp_def wp t.
Proof using.
applys~ (FixFun_fix_iter (measure trm_size)). auto with wf.
intros f1 f2 t IH. unfold WP_def.
intros f1 f2 t IH. unfold wp_def.
destruct t; fequals.
{ fequals~. }
{ fequals~. }
{ fequals~. applys~ fun_ext_1. }
(*
{ fequals~. }
{ destruct t1; fequals~. destruct t2; fequals~.
applys~ fun_ext_1. }
*)
{ destruct t1; fequals~.
destruct t2; fequals~.
fequals. applys~ fun_ext_1. }
Qed.
Lemma WP_unfold : forall t,
WP t = WP_def WP t.
Proof using. applys (WP_unfold_iter 1). Qed.
Lemma wp_unfold : forall t,
wp t = wp_def wp t.
Proof using. applys (wp_unfold_iter 1). Qed.
(* ********************************************************************** *)
......@@ -254,9 +258,9 @@ Proof using. applys (WP_unfold_iter 1). Qed.
(* ** Soundness of the WP generator *)
Lemma is_local_cf : forall t,
is_local (WP t).
is_local (wp t).
Proof.
intros. rewrite WP_unfold. destruct t; try apply is_local_local.
intros. rewrite wp_unfold. destruct t; try apply is_local_local.
Qed.
Definition sound_for (t:trm) (F:formula) :=
......@@ -274,33 +278,271 @@ Proof using.
{ hchanges qwand_cancel. }
Qed.
Definition sound_for' (t:trm) (F:formula) :=
forall Q, triple t (F Q) Q.
Lemma sound_for_eq_sound_for' :
sound_for = sound_for'.
Proof using.
applys pred_ext_2. intros t f.
unfold sound_for, sound_for'. intros. iff M.
{ intros Q. applys M. auto. }
{ intros H Q N. applys* rule_consequence N M. }
Qed.
Lemma sound_for'_local : forall t (F:formula),
sound_for' t F ->
sound_for' t (local F).
Proof using. introv. rewrite <- sound_for_eq_sound_for'. applys sound_for_local. Qed.
Lemma sound_for'_local' : forall t (F:formula) Q,
(forall Q, triple t (F Q) Q) ->
triple t (local F Q) Q.
Proof using. introv M. applys sound_for'_local. applys M. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Soundness of the WP generator *)
Lemma triple_of_WP : forall (t:trm) H Q,
H ==> WP t Q ->
(* TODO *)
Lemma himpl_hforall_r : forall A (J:A->hprop) H,
(forall x, H ==> J x) ->
H ==> (hforall J).
Proof using. introv M. intros h Hh x. apply~ M. Qed.
Lemma himpl_hforall_l : forall A (J:A->hprop) H,
(exists x, J x ==> H) ->
(hforall J) ==> H.
Proof using. introv (x&M). intros h Hh. apply~ M. Qed.
(* LATER
Lemma hpull_hforall : forall A H1 H2 H' (J:A->hprop),
(exists x, H1 \* J x \* H2 ==> H') ->
H1 \* (hforall J \* H2) ==> H'.
Proof using.
introv (x&M). rewrite hstar_comm_assoc.
applys himpl_trans. applys hstar_hforall.
applys himpl_hforall_l. exists x.
rewrite~ <- hstar_comm_assoc.
Qed.
*)
(* partial support for hforall
Ltac hpull_step tt ::=
match goal with |- _ \* ?HN ==> _ =>
match HN with
| ?H \* _ =>
match H with
| \[] => apply hpull_empty
| \[_] => apply hpull_hprop; intros
| hexists _ => apply hpull_hexists; intros
| hforall _ => apply hpull_hforall
| _ \* _ => apply hpull_assoc
| _ => apply hpull_keep
end
| \[] => fail 1
| ?H => apply hpull_starify
end end.
*)
(** Extraction of foralls below a star from [local] *)
Lemma local_extract_hforall : forall B (F:~~B) H A (J:A->hprop) Q,
SepBasicSetup.is_local F ->
(exists x, F ((J x) \* H) Q) ->
F (hforall J \* H) Q.
Proof using.
introv L (x&M). rewrite L. unfold SepBasicSetup.local.
hchange hstar_hforall. rew_heap. applys himpl_hforall_l.
exists x. hsimpl (J x \* H) Q. split~. hsimpl.
Qed.
Lemma rule_extract_hforall : forall t (A:Type) (J:A->hprop) Q,
(exists x, triple t (J x) Q) ->
triple t (hforall J) Q.
Proof using.
introv (x&M). intros HF h N. lets N': hstar_hforall (rm N) x.
applys* M.
Qed.
Lemma rule_extract_hwand_hpure_l : forall t (P:Prop) H Q,
(P /\ triple t H Q) ->
triple t (\[P] \--* H) Q.
Proof using.
introv (HP&M). intros HF h N.
lets N': hstar_hwand (rm N).
lets U: (conj (rm HP) (rm N')). rewrite <- hstar_pure in U.
lets U': hwand_cancel (rm U).
applys* M.
Qed.
Lemma local_extract_false : forall F Q,
(forall Q', F Q' ==> \[False]) ->
(local F Q ==> \[False]).
Proof using.
introv M. unfold local. hpull ;=> Q'. hchanges (M Q').
Qed.
(* LATER
Lemma xpull_hforall : forall B (F:~~B) H1 H2 A (J:A->hprop) Q,
SepBasicSetup.is_local F ->
(exists x, F (H1 \* ((J x) \* H2)) Q) ->
F (H1 \* (hforall J \* H2)) Q.
Proof using.
intros. rewrite hstar_comm_assoc. apply~ local_extract_hexists.
intros. rewrite~ hstar_comm_assoc.
Qed.
*)
(* Hint Resolve is_local_triple. *)
Lemma weakestpre_pre : forall B (F:~~B) Q,
SepBasicSetup.is_local F ->
F (weakestpre F Q) Q.
Proof using. intros. unfold weakestpre. xpull ;=> H'. auto. Qed.
(* corollary of weakestpre_pre. *)
Lemma triple_weakestpre_pre : forall t Q,
triple t (weakestpre (triple t) Q) Q.
Proof using.
intros. unfold weakestpre. xpull ;=> H. auto.
Qed.
Lemma local_erase' : forall H F Q,
H ==> F Q ->
H ==> local F Q.
Proof using.
introv M. hchanges M. applys local_erase.
Qed.
(** Ramified frame rule with top *)
Lemma local_ramified_frame_htop : forall (Q1:val->hprop) H1 F H Q,
SepBasicSetup.is_local F ->
F H1 Q1 ->
H ==> H1 \* (Q1 \---* Q \*+ \Top) ->
F H Q.
Proof using.
introv L M W. applys~ SepBasicSetup.local_frame_htop (Q1 \---* Q \*+ \Top) M.
hchanges qwand_cancel.
Qed.
(*
Lemma is_local_weakestpre : forall B (F:~~B) Q,
SepBasicSetup.is_local F ->
is_local (weakestpre F).
Proof using. intros. unfold weakestpre. xpull ;=> H'. auto. Qed.
*)
Lemma rule_ramified_frame_htop_pre : forall t H Q Q',
triple t H Q' ->
triple t (H \* (Q' \---* Q \*+ \Top)) Q.
Proof using.
introv M. applys local_ramified_frame_htop M.
applys is_local_triple. hsimpl.
Qed.
(* TODO: stays here *)
Lemma is_local_weakestpre_triple : forall t,
is_local (weakestpre (triple t)).
Proof using.
intros. unfold is_local, weakestpre. applys fun_ext_1 ;=> Q.
applys himpl_antisym.
{ apply~ local_erase'. }
{ unfold local. hpull ;=> Q' H M. hsimpl (H \* (Q' \---* Q \*+ \Top)).
applys~ rule_ramified_frame_htop_pre. }
Qed.
Lemma weaken_formula_trans : forall (F1 F2:formula),
(forall H' Q', (H' ==> F1 Q') -> (H' ==> F2 Q')) ->
F1 ===> F2.
Proof using. introv M. intros Q. applys~ M (F1 Q). Qed.
Lemma weakestpre_intro : forall B (F:~~B) H Q,
F H Q ->
H ==> weakestpre F Q.
Proof using. introv M. unfold weakestpre. hsimpl~ H. Qed.
(*
Lemma triple_local_pre : forall t F Q,
triple t (F Q) Q ->
triple t (local F Q) Q.
Proof using.
introv M. applys sound_for_local F. hnf.
introv N.
auto.
Qed.
*)
(*
introv M. unfold local. xpull ;=> Q'.
lets N: rule_ramified_frame_htop_pre Q' M.
rewrite~ hstar_comm.
*)
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;
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. }
{ unfolds WP_val. applys~ rule_fix. }
{ unfolds WP_if, WP_if_val. applys rule_if.
{ unfolds wp_val. applys~ rule_val. }
{ unfolds wp_fail. xchanges (rm P). intros; false. }
{ unfolds wp_val. applys~ rule_fun. }
{ unfolds wp_val. applys~ rule_fix. }
{ unfolds wp_if. applys rule_if.
{ applys* IH. }
{ intros b. xpull ;=> v E. inverts E.
case_if; case_if; tryfalse*.
{ intros b. simpl. applys sound_for'_local'. clears Q. intros Q.
unfold wp_if_val. xpull ;=> b' E. inverts E. case_if.
{ applys* IH. }
{ applys* IH. } }
{ intros v N. hpull ;=> v' E. inverts E. false* N. hnfs*. } }
{ unfolds WP_seq. applys rule_seq'. { applys* IH. } { applys* IH. } }
{ unfolds WP_let. applys rule_let. { applys* IH. } { intros X. applys* IH. } }
{ simpl. intros v N. applys local_extract_false. intros Q'.
unfold wp_if_val. hpull ;=> v' E. inverts E. false* N. hnfs*. } }
{ unfolds wp_seq. applys rule_seq'. { applys* IH. } { applys* IH. } }
{ unfolds wp_let. applys rule_let. { applys* IH. } { intros X. applys* IH. } }
{ unfolds weakestpre. xchanges~ P. }
{ unfolds WP_fail. xchanges P. intros; false. }
{ unfolds WP_fail. xchanges P. intros; false. }
(*
{ unfolds wp_while. xchange (rm P); rew_heap.
apply rule_extract_hforall. exists (weakestpre (triple (trm_while t1 t2))).
apply rule_extract_hwand_hpure_l. split; [ split | ].
{ apply~ is_local_weakestpre_triple. }
{ clear H Q. set (R := weakestpre (triple (trm_while t1 t2))).
applys weaken_formula_trans. intros H Q P.
unfold R. apply weakestpre_intro. applys rule_while_raw.
applys sound_for_local (rm P). clear H Q. intros H Q P.
applys rule_if.
{ applys* IH. }
{ intros b. simpl. applys sound_for'_local'. clears Q. intros Q.
unfold wp_if_val. xpull ;=> v' E. inverts E. case_if.
{ applys sound_for'_local'. clears Q. intros Q.
unfold wp_seq. applys rule_seq'.
{ applys* IH. }
{ unfold R. apply weakestpre_pre. apply is_local_triple. } }
{ applys sound_for'_local'. clears Q. intros Q.
unfold wp_val. applys~ rule_val. } }
{ simpl. intros v N. applys local_extract_false. intros Q'.
unfold wp_if_val. hpull ;=> v' E. inverts E. false* N. hnfs*. } }
{ apply weakestpre_pre. apply is_local_triple. } }
{ skip. }
(*
{ hnf in P. simpls. applys P. { xlocal. } clears H Q. intros H Q P.
applys rule_while_raw. applys sound_for_local (rm P).
clears H Q. intros H Q (Q1&P1&P2). applys rule_if.
......@@ -330,11 +572,11 @@ Proof using.
*)
Qed.
Lemma triple_trm_of_WP_iter : forall (n:nat) t H Q,
H ==> func_iter n WP_def WP t Q ->
Lemma triple_trm_of_wp_iter : forall (n:nat) t H Q,
H ==> func_iter n wp_def wp t Q ->
triple t H Q.
Proof using.
introv M. rewrite <- WP_unfold_iter in M. applys* triple_of_WP.
introv M. rewrite <- wp_unfold_iter in M. applys* triple_of_wp.
Qed.
......@@ -346,24 +588,24 @@ Qed.
(* ** Notation for computd WP *)
Notation "'`Val' v" :=
(local (WP_val v))
(local (wp_val v))
(at level 69) : charac.
Notation "'`LetIf' F0 'Then' F1 'Else' F2" :=
(local (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" :=
(local (WP_if_val v F1 F2))
(local (wp_if_val v F1 F2))
(at level 69) : charac.
Notation "'`Seq' F1 ;;; F2" :=
(local (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" :=
(local (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.
......@@ -372,18 +614,18 @@ Notation "'`App' t " :=
(at level 68, t at level 0) : charac.
Notation "'`Fail'" :=
(local (WP_fail))
(local (wp_fail))
(at level 69) : charac.
(*
Notation "'`While' F1 'Do' F2 'Done'" :=
(local (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'" :=
(local (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.
......@@ -400,24 +642,24 @@ Implicit Types n : nat.
Implicit Types F : val.
Implicit Types f x : var.
Lemma triple_apps_funs_of_WP_iter : forall n F (vs:vals) xs t H Q,
Lemma triple_apps_funs_of_wp_iter : forall n F (vs:vals) xs t H Q,
F = val_funs xs t ->
var_funs_exec (length vs) xs ->
H ==> func_iter n WP_def WP (substs xs vs t) Q ->
H ==> func_iter n wp_def wp (substs xs vs t) Q ->
triple (trm_apps F vs) H Q.
Proof using.
introv EF N M. rewrite var_funs_exec_eq in N. rew_istrue in N.
applys* rule_apps_funs. applys* triple_trm_of_WP_iter.
applys* rule_apps_funs. applys* triple_trm_of_wp_iter.
Qed.
Lemma triple_apps_fixs_of_WP_iter : forall n f F (vs:vals) xs t H Q,
Lemma triple_apps_fixs_of_wp_iter : forall n f F (vs:vals) xs t H Q,
F = val_fixs f xs t ->
var_fixs_exec f (length vs) xs ->
H ==> func_iter n WP_def WP (subst f F (substs xs vs t)) Q ->
H ==> func_iter n wp_def wp (subst f F (substs xs vs t)) Q ->
triple (trm_apps F vs) H Q.
Proof using.
introv EF N M. rewrite var_fixs_exec_eq in N. rew_istrue in N.
applys* rule_apps_fixs. applys* triple_trm_of_WP_iter.
applys* rule_apps_fixs. applys* triple_trm_of_wp_iter.
Qed.
End LemmasCf.
......@@ -474,16 +716,16 @@ Ltac xcf_post tt :=
simpl.
Ltac xcf_trm n ::=
applys triple_trm_of_WP_iter n; [ xcf_post tt ].
applys triple_trm_of_wp_iter n; [ xcf_post tt ].
Ltac xcf_basic_fun n f' ::=
let f := xcf_get_fun tt in
match f with
| val_funs _ _ => (* TODO: use (apply (@..)) instead of applys? same in cflifted *)
applys triple_apps_funs_of_WP_iter n;
applys triple_apps_funs_of_wp_iter n;
[ reflexivity | reflexivity | xcf_post tt ]
| val_fixs _ _ _ =>
applys triple_apps_fixs_of_WP_iter n f';
applys triple_apps_fixs_of_wp_iter n f';
[ try unfold f'; rew_nary; try reflexivity (* TODO: how in LambdaCF? *)
(* reflexivity *)
| reflexivity
......@@ -498,22 +740,16 @@ Definition val_incr :=
Let 'm := 'n '+ 1 in
val_set 'p 'm.
Lemma local_erase' : forall H F Q,
H ==> F Q ->
H ==> local F Q.
Proof using.
introv M. hchanges M. applys local_erase.
Qed.
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.
H ==> local (wp_let F1 F2) Q.
Proof using.
introv L M1 M2. applys local_erase'.
unfold WP_let. applys~ local_weaken M1.
unfold wp_let. applys~ local_weaken M1.
Qed.
Ltac xlet_core tt ::=
......@@ -578,7 +814,7 @@ Ltac xif_core tt ::=
(* ** Tactic [xfail] *)
Ltac xfail_core tt ::=
applys local_erase; unfold WP_fail.
applys local_erase; unfold wp_fail.
(* ---------------------------------------------------------------------- *)
......@@ -618,9 +854,9 @@ Ltac xapps_let_cont tt ::=
Ltac xapp_template xlet_tactic xapp_tactic xlet_cont ::=
match goal with
| |- local (WP_let _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
| |- local (WP_if _ _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
| |- local (WP_seq _ _) _ _ => xseq; [ xapp_tactic tt | ]
| |- local (wp_let _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
| |- local (wp_if _ _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
| |- local (wp_seq _ _) _ _ => xseq; [ xapp_tactic tt | ]
| _ => xapp_tactic tt
end.
......@@ -669,16 +905,16 @@ Ltac xapp_basic E cont_post tt ::=
(* ** Tactic [xval] and [xvals] *)
Ltac xval_nohtop_core tt :=
applys local_erase; unfold WP_val.
applys local_erase; unfold wp_val.
Tactic Notation "xval_nohtop" :=
xval_nohtop_core tt.
Lemma xval_htop_lemma : forall v H Q,
H ==> Q v \* \Top ->
local (WP_val v) H Q.
local (wp_val v) H Q.
Proof using.
intros v H Q M. unfold WP_val.
intros v H Q M. unfold wp_val.
applys~ local_htop_post (Q \*+ \Top).
applys local_erase. intros x.
hpull. intro_subst. hchanges~ M.
......@@ -686,13 +922,13 @@ Qed.
Lemma xval_htop_as_lemma : forall v H Q,
(forall x, x = v -> H ==> Q x \* \Top) ->
local (WP_val v) H Q.
local (wp_val v) H Q.
Proof using. intros v H Q M. applys~ xval_htop_lemma. Qed.
Ltac xval_template xlet_tactic xval_tactic xlet_cont :=
match goal with
| |- local (WP_let _ _) _ _ => xlet_tactic tt; [ xval_tactic tt | xlet_cont tt ]
| |- local (WP_if _ _ _) _ _ => xlet_tactic tt; [ xval_tactic tt | xlet_cont tt ]
| |- local (wp_let _ _) _ _ => xlet_tactic tt; [ xval_tactic tt | xlet_cont tt ]
| |- local (wp_if _ _ _) _ _ => xlet_tactic tt; [ xval_tactic tt | xlet_cont tt ]
| _ => xval_tactic tt
end.
......@@ -713,13 +949,13 @@ Ltac xval_core tt ::=
Ltac xval_as_core X ::=
match goal with
| |- local (WP_val _) _ _ => let EX := fresh "E" X in xval_as_basic X EX
| |- local (wp_val _) _ _ => let EX := fresh "E" X in xval_as_basic X EX
| _ => xval_template ltac:(fun tt => xlet as X) ltac:(xval_basic) ltac:(xapp_as_let_cont)
end.
Ltac xvals_core tt ::=
match goal with
| |- local (WP_val _) _ _ => xval_basic tt; hsimpl
| |- local (wp_val _) _ _ => xval_basic tt; hsimpl
| _ => xval_template ltac:(fun tt => xlet) ltac:(xval_basic) ltac:(xapps_let_cont)
end.
......@@ -730,7 +966,7 @@ Ltac xvals_core tt ::=
(*
Ltac xwhile_template xwhile_tactic xseq_cont :=
match goal with
| |- local (WP_seq _ _) _ _ => xseq; [ xwhile_tactic tt | xseq_cont tt ]
| |- local (wp_seq _ _) _ _ => xseq; [ xwhile_tactic tt | xseq_cont tt ]
| _ => xwhile_tactic tt
end.
......
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