Commit 2f75a379 authored by charguer's avatar charguer

working

parent 7224defa
......@@ -53,7 +53,7 @@ Proof using.
applys rule_consequence.
{ hsimpl. }
{ applys rule_set. }
{ intros r. applys himpl_hprop_l. intros E. subst.
{ intros r. applys himpl_hpure_l. intros E. subst.
applys himpl_hprop_r. { auto. } { auto. } }
Qed.
......
......@@ -164,8 +164,8 @@ Proof using.
applys rule_consequence.
{ hsimpl. }
{ applys rule_set. }
{ intros r. applys himpl_hprop_l. intros E. subst.
applys himpl_hprop_r. { auto. } { auto. } }
{ intros r. applys himpl_hpure_l. intros E. subst.
applys himpl_hpure_r. { auto. } { auto. } }
Qed.
(** Same proof using [xapply], [xapplys] and [xpull] *)
......
......@@ -3687,4 +3687,90 @@ Proof using.
introv R W M. applys~ regular_frame_top H1 H2. { hchanges W. }
Qed.
*)
\ No newline at end of file
*)
(* 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.
*)
(* 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.
*)
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.
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 SepBasicSetup.local.
hchange M. unfold local. hpull ;=> Q'.
hsimpl (F Q') ((Q' \---* Q \*+ \Top)) Q'. split.
{ applys~ SF. }
{ 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.
......@@ -464,6 +464,9 @@ Ltac xlocal_base tt ::=
(* ---------------------------------------------------------------------- *)
(* ** Structural rules *)
(** Note: all these rules could be derived directly from the fact that
[triple] satisfies [is_local], using lemmas from [SepFunctor] *)
Lemma rule_extract_hexists : forall t (A:Type) (J:A->hprop) Q,
(forall x, triple t (J x) Q) ->
triple t (hexists J) Q.
......@@ -472,6 +475,14 @@ Proof using.
destruct N as (x&N). applys* M.
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_hprop : forall t (P:Prop) H Q,
(P -> triple t H Q) ->
triple t (\[P] \* H) Q.
......@@ -480,6 +491,18 @@ Proof using.
applys rule_extract_hexists.
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 rule_consequence : forall t H' Q' H Q,
H ==> H' ->
triple t H' Q' ->
......@@ -515,6 +538,7 @@ Proof using.
introv M. applys rule_htop_post. applys~ rule_frame.
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Term rules *)
......@@ -752,6 +776,61 @@ Proof using.
{ intros v Nv. hpull. } }
Qed.
(** Rules for for-loop not in normal form *)
Lemma rule_for_trm : forall (x:var) (t1 t2 t3:trm) H (Q:val->hprop) (Q1:val->hprop),
triple t1 H Q1 ->
(forall v1, exists Q2,
triple t2 (Q1 v1) Q2
/\ (forall v2, triple (trm_for x v1 v2 t3) (Q2 v2) Q)) ->
triple (trm_for x t1 t2 t3) H Q.
Proof using.
introv M1 M2. intros HF h Hf. forwards (h1'&v1&R1&K1): (rm M1) Hf.
lets (Q2&M2'&M3): ((rm M2) v1).
forwards* (h2'&v2&R2&K2): (rm M2') h1'.
rewrite <- (hstar_assoc \Top \Top) in K2. rewrite htop_hstar_htop in K2.
forwards* (h'&v'&R'&K'): ((rm M3) v2) h2'.
exists h' v'. splits~.
{ applys* red_for_arg. }
{ rewrite <- htop_hstar_htop. rew_heap~. }
Qed.
Definition is_val_int (v:val) :=
exists n, v = val_int n.
(* full rule, too complex *)
Lemma rule_for_trm_int : forall (x:var) (t1 t2 t3:trm) H (Q:val->hprop) (Q1:val->hprop),
triple t1 H Q1 ->
(forall v, ~ is_val_int v -> (Q1 v) ==> \[False]) ->
(forall (n1:int), exists Q2,
triple t2 (Q1 (val_int n1)) Q2
/\ (forall v, ~ is_val_int v -> (Q2 v) ==> \[False])
/\ (forall (n2:int), triple (trm_for x n1 n2 t3) (Q2 (val_int n2)) Q)) ->
triple (trm_for x t1 t2 t3) H Q.
Proof using. (* might be simplified using rule_for_trm *)
introv M1 nQ1 M2. intros HF h Hf. forwards (h1'&v1&R1&K1): (rm M1) Hf.
tests C1: (is_val_int v1).
{ destruct C1 as (n1&E). subst. lets (Q2&M2'&nQ2&M3): ((rm M2) n1).
forwards* (h2'&v2&R2&K2): (rm M2') h1'.
rewrite <- (hstar_assoc \Top \Top) in K2. rewrite htop_hstar_htop in K2.
tests C2: (is_val_int v2).
{ destruct C2 as (n2&E). subst.
forwards* (h'&v'&R'&K'): ((rm M3) n2) h2'.
exists h' v'. splits~.
{ applys* red_for_arg. }
{ rewrite <- htop_hstar_htop. rew_heap~. } }
{ specializes nQ2 C2.
asserts Z: ((\[False] \* \Top \* HF) h2').
{ applys himpl_trans K2. hchange nQ2. hsimpl. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. } } (* LATER: shorten *)
{ specializes nQ1 C1.
asserts Z: ((\[False] \* \Top \* HF) h1').
{ applys himpl_trans K1. hchange nQ1. hsimpl. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. } (* LATER: shorten *)
Qed.
(* ---------------------------------------------------------------------- *)
(** Primitive functions over the state *)
......@@ -770,7 +849,7 @@ Proof using.
exists (h1' \u h) (val_loc l). splits~.
{ applys~ red_ref. }
{ exists h1' h. split.
{ exists l. applys~ himpl_hprop_r. unfold h1'. hnfs~. }
{ exists l. applys~ himpl_hpure_r. unfold h1'. hnfs~. }
{ splits~. hhsimpl~. } }
Qed.
......@@ -818,7 +897,7 @@ Proof using. (* Note: [abs n] currently does not compute in Coq. *)
{ applys (red_alloc (abs n)); eauto.
rewrite~ abs_nonneg. }
{ exists h1' h. split.
{ exists l. applys~ himpl_hprop_r. applys~ Alloc_fmap_conseq. }
{ exists l. applys~ himpl_hpure_r. applys~ Alloc_fmap_conseq. }
{ splits~. hhsimpl~. } }
Qed.
......
......@@ -59,68 +59,7 @@ Definition is_local_pred A (S:A->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_erase' : forall H F Q,
H ==> F Q ->
H ==> local F Q.
Proof using.
introv M. hchanges M. applys local_erase.
Qed.
(* ** Elimination rules for [is_local] *)
Lemma local_weaken : forall Q' F H Q,
is_local F ->
......@@ -167,51 +106,62 @@ Proof using.
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Properties of [local] for WP *)
(** Local can be erased *)
Lemma local_erase : forall F Q,
F Q ==> local F Q.
Proof using.
intros. unfold local. hsimpl. hchanges (qwand_of_qimpl Q). hsimpl.
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.
(* TODO *)
(** Ramified frame rule with top *)
(** Contradictions can be extracted from local formulae *)
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.
Lemma local_extract_false : forall F Q,
(forall Q', F Q' ==> \[False]) ->
(local F Q ==> \[False]).
Proof using.
introv L M W. applys~ SepBasicSetup.local_frame_htop (Q1 \---* Q \*+ \Top) M.
hchanges qwand_cancel.
introv M. unfold local. hpull ;=> Q'. hchanges (M Q').
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.
*)
(** [local] is a covariant transformer w.r.t. predicate inclusion *)
Lemma rule_ramified_frame_htop_pre : forall t H Q Q',
triple t H Q' ->
triple t (H \* (Q' \---* Q \*+ \Top)) Q.
Lemma local_weaken_body : forall F F',
F ===> F' ->
local F ===> local F'.
Proof using.
introv M. applys local_ramified_frame_htop M.
applys is_local_triple. hsimpl.
unfold local. introv M. intros Q. hpull ;=> Q'. hsimpl~ Q'.
Qed.
(** [local] is idempotent, i.e. nested applications
of [local] are redundant *)
(* TODO: stays here *)
Lemma is_local_weakestpre_triple : forall t,
is_local (weakestpre (triple t)).
Lemma local_local : forall F,
local (local F) = local F.
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. }
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.
(* ---------------------------------------------------------------------- *)
......@@ -274,7 +224,7 @@ Definition wp_def wp (t:trm) :=
| trm_if t0 t1 t2 => wp_if (wp t0) (wp t1) (wp t2)
| trm_seq t1 t2 => wp_seq (wp t1) (wp t2)
| trm_let x t1 t2 => wp_let (wp t1) (fun X => wp (subst x X t2))
| trm_app t1 t2 => weakestpre (triple t)
| trm_app t1 t2 => local (weakestpre (triple t))
| trm_while t1 t2 => wp_while (wp t1) (wp t2)
| trm_for x t1 t2 t3 => wp_for' (wp t1) (wp t2) (fun X => wp (subst x X t3))
end.
......@@ -298,187 +248,14 @@ Proof using. applys (wp_unfold_iter 1). Qed.
(* * Soundness proof *)
(* ---------------------------------------------------------------------- *)
(* ** Soundness of the WP generator *)
Lemma is_local_cf : forall t,
is_local (wp t).
Proof.
intros. rewrite wp_unfold.
destruct t; try solve [ apply is_local_local ].
{ simpl. applys is_local_weakestpre_triple. }
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 SepBasicSetup.local.
hchange M. unfold local. hpull ;=> Q'.
hsimpl (F Q') ((Q' \---* Q \*+ \Top)) Q'. split.
{ applys~ SF. }
{ 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.
(*
Lemma remove_local_from_hyp : forall t (F:formula) H Q,
(H ==> local F Q) ->
(forall Q, triple t (F Q) Q) ->
triple t H Q.
Proof using. introv N M. xchanges N. applys* sound_for'_local'. Qed.
*)
(* ---------------------------------------------------------------------- *)
(* ** Soundness of the WP generator *)
(* 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.
(* ** Auxiliary lemmas for the soundness proof *)
(** Specialized results for a [weakestpre] of a [triple]. *)
Lemma triple_weakestpre_pre : forall t Q,
triple t (weakestpre (triple t) Q) Q.
Proof using. intros. applys weakestpre_pre. applys is_local_triple. 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 himpl_weakestpre : forall B (F:~~B) H Q,
F H Q ->
H ==> weakestpre F Q.
Proof using. introv M. unfold weakestpre. hsimpl~ H. Qed.
Lemma qimpl_weakestpre_triple : forall t F,
(forall Q, triple t (F Q) Q) ->
F ===> weakestpre (triple t).
......@@ -486,33 +263,30 @@ Proof using.
introv M. intros Q'. applys himpl_weakestpre. applys M.
Qed.
(** A specialized version of frame (should it remain?) *)
(*
Lemma triple_local_pre : forall t F Q,
triple t (F Q) Q ->
triple t (local F Q) Q.
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 sound_for_local F. hnf.
introv N.
auto.
introv M. applys local_ramified_frame_htop M.
applys is_local_triple. hsimpl.
Qed.
*)
(*
introv M. unfold local. xpull ;=> Q'.
lets N: rule_ramified_frame_htop_pre Q' M.
rewrite~ hstar_comm.
*)
(** Instance of [is_local] for [weakestpre]: an auxiliary
lemma useful for soundness of loops *)
(*
Lemma triple_of_wp_fail : forall t H Q,
H ==> wp_fail Q ->
triple t H Q.
Lemma is_local_weakestpre_triple : forall t,
is_local (weakestpre (triple t)).
Proof using.
introv M. xchanges M. applys sound_for'_local'. clears Q; intros Q.
xpull. intros; false.
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.
*)
(** Following lemma used to deal with if-statements not producing a boolean *)
Lemma wp_if_val_false : forall v F1 F2 Q,
~ is_val_bool v ->
......@@ -522,67 +296,40 @@ Proof using.
hpull ;=> v' E. inverts E. false* M. hnfs*.
Qed.
(** All [wp] are trivially local by construction *)
(** [remove_local] applies to goal of the form [triple t (local F Q) Q] *)
Ltac remove_local :=
match goal with |- triple _ _ ?Q =>
applys sound_for'_local'; try (clear Q; intros Q); xpull end.
Definition is_val_int (v:val) :=
exists n, v = val_int n.
Lemma rule_for_trm_int : forall (x:var) (t1 t2 t3:trm) H (Q:val->hprop) (Q1:val->hprop),
triple t1 H Q1 ->
(forall v, ~ is_val_int v -> (Q1 v) ==> \[False]) ->
(forall (n1:int), exists Q2,
triple t2 (Q1 (val_int n1)) Q2
/\ (forall v, ~ is_val_int v -> (Q2 v) ==> \[False])
/\ (forall (n2:int), triple (trm_for x n1 n2 t3) (Q2 (val_int n2)) Q)) ->
triple (trm_for x t1 t2 t3) H Q.
Proof using.
introv M1 nQ1 M2. intros HF h Hf. forwards (h1'&v1&R1&K1): (rm M1) Hf.
tests C1: (is_val_int v1).
{ destruct C1 as (n1&E). subst. lets (Q2&M2'&nQ2&M3): ((rm M2) n1).
forwards* (h2'&v2&R2&K2): (rm M2') h1'.
rewrite <- (hstar_assoc \Top \Top) in K2. rewrite htop_hstar_htop in K2.
tests C2: (is_val_int v2).
{ destruct C2 as (n2&E). subst.
forwards* (h'&v'&R'&K'): ((rm M3) n2) h2'.
exists h' v'. splits~.
{ applys* red_for_arg. }
{ rewrite <- htop_hstar_htop. rew_heap~. } }
{ specializes nQ2 C2.
asserts Z: ((\[False] \* \Top \* HF) h2').
{ applys himpl_trans K2. hchange nQ2. hsimpl. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. } } (* LATER: shorten *)
{ specializes nQ1 C1.
asserts Z: ((\[False] \* \Top \* HF) h1').
{ applys himpl_trans K1. hchange nQ1. hsimpl. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. } (* LATER: shorten *)
Lemma is_local_cf : forall t,
is_local (wp t).