Commit 652229b2 authored by charguer's avatar charguer

wp_sound

parent de777ecd
......@@ -176,9 +176,9 @@ Proof using.
case_if; applys* IH. }
{ intros v N. specializes P2 v. applys local_extract_false P2.
intros H' Q' (b&E&S1&S2). subst. applys N. hnfs*. } }
{ destruct P as (H1&P1&P2). applys rule_seq' H1.
{ admit. (* destruct P as (H1&P1&P2). applys rule_seq H1.
{ applys~ IH. }
{ intros X. applys~ IH. } }
{ intros X. applys~ IH. } *) }
{ destruct P as (Q1&P1&P2). applys rule_let Q1.
{ applys~ IH. }
{ intros X. applys~ IH. } }
......
......@@ -4195,4 +4195,171 @@ Ltac xwhile_core xwhile_tactic ::=
*)
*)
\ No newline at end of file
*)
Definition sound_for t :=
forall E Q, triple (substs E t) (wp E t Q) Q.
Lemma triple_wp_val : forall v,
sound_for (trm_val v).
Proof using.
intros. intros E Q. remove_local. rewrite substs_val. applys~ rule_val.
Qed.
Lemma triple_wp_fun : forall x t,
sound_for (trm_fun x t).
Proof using.
intros. intros E Q. remove_local. rewrite substs_fun. applys~ rule_fun.
Qed.
Lemma triple_wp_fix : forall f x t,
sound_for (trm_fix f x t).
Proof using.
intros. intros E Q. remove_local. rewrite substs_fix. applys~ rule_fix.
Qed.
Lemma triple_wp_var : forall x,
sound_for (trm_var x).
Proof using.
intros. intros E Q. remove_local.
rewrite substs_var. destruct (ctx_lookup x E).
{ apply~ rule_val. }
{ xpull ;=> F. false. }
Qed.
Lemma triple_wp_if : forall t1 t2 t3,
sound_for t1 ->
sound_for t2 ->
sound_for t3 ->
sound_for (trm_if t1 t2 t3).
Proof using.
introv M1 M2 M3. intros E Q. remove_local.
rewrite substs_if. applys rule_if.
{ applys* M1. }
{ intros b. simpl. remove_local ;=> b' M. inverts M. case_if.
{ applys* M2. }
{ applys* M3. } }
{ intros. applys~ wp_if_val_false. }
Qed.
Lemma triple_wp_seq : forall t1 t2,
sound_for t1 ->
sound_for t2 ->
sound_for (trm_seq t1 t2).
Proof using.
introv M1 M2. intros E Q. remove_local.
rewrite substs_seq. applys rule_seq.
{ applys* M1. }
{ intros X. applys* M2. }
Qed.
Lemma triple_wp_let : forall x t1 t2,
sound_for t1 ->
sound_for t2 ->
sound_for (trm_let x t1 t2).
Proof using.
introv M1 M2. intros E Q. remove_local.
rewrite substs_let. applys rule_let.
{ applys* M1. }
{ intros X. rewrite subst_substs_ctx_rem_same. applys M2. }
Qed.
Lemma triple_wp_app : forall t1 t2,
sound_for t1 ->
sound_for t2 ->
sound_for (trm_app t1 t2).
Proof using.
introv M1 M2. intros E Q. remove_local.
rewrite substs_app. apply triple_weakestpre_pre.
Qed.
Lemma triple_wp_while : forall t1 t2,
sound_for t1 ->
sound_for t2 ->
sound_for (trm_while t1 t2).
Proof using.
introv M1 M2. intros E Q. remove_local.
rewrite substs_while. applys rule_extract_hforall.
set (R := weakestpre (triple (trm_while (substs E t1) (substs E t2)))). (* *)
(* set (R := wp E (trm_while t1 t2)).*)
exists R. simpl. applys rule_extract_hwand_hpure_l. (*todo rename *)
{ split.
{ (* applys is_local_wp *) applys is_local_weakestpre_triple. }
{ clears Q. applys qimpl_weakestpre_triple. intros Q.
(*
set (t1' := substs E t1) in *.
set (t2' := substs E t2) in *.
*)
applys rule_while_raw. rewrite <- substs_while. rewrite <- substs_seq.
rewrite <- (substs_val E). rewrite <- substs_if.
applys triple_wp_if'. skip.
unfold we.
applys qimpl_weakestpre_triple. intros Q'.
applys triple_wp_seq'.
skip.
unfold R. unfold we. rewrite substs_while. auto.
auto.
applys weakestpre_elim.
applys triple_wp_seq'.
forwards M: triple_wp_if'' E t1 (trm_seq t2 (trm_while t1 t2)) val_unit.
skip. skip. skip.
{ skip. }
{ hnf. intros Q'.
applys himpl_trans. applys triple_wp_seq'. skip.
hnf. applys triple_wp_
intros E'. forwards: triple_wp_seq. skip. skip.
Search weakestpre. applys weakestpre_elim.
applys triple_wp_if''.
subst R. simpl. unfold wp_while at 2. apply local_erase'.
apply himpl_hforall_r. intros R. applys hwand_move_l. hpull.
intros (LR&MR).
Search hwand.
applys rule_while_raw.
forwards M: triple_wp_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit.
auto.
applys triple_wp_seq.
(substs E t1) (trm_seq (substs E t2) (trm_while (substs E t1) (substs E t2))
applys triple_wp_if.
Qed.
Lemma triple_wp : forall t E Q,
triple (substs E t) (wp E t Q) Q.
Proof using.
intros t. induction t; intros.
{ applys triple_wp_val. }
{ applys triple_wp_var. }
{ applys triple_wp_fun. }
{ applys triple_wp_fix. }
{ applys* triple_wp_if. }
{ applys* triple_wp_seq. }
{ applys* triple_wp_let. }
{ applys* triple_wp_app. }
{ applys* triple_wp_while. }
{ admit. }
Qed.
......@@ -136,8 +136,8 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m1 t0 m2 (val_bool b) ->
red m2 (if b then t1 else t2) m3 r ->
red m1 (trm_if t0 t1 t2) m3 r
| red_seq : forall m1 m2 m3 t1 t2 r,
red m1 t1 m2 val_unit ->
| red_seq : forall m1 m2 m3 t1 t2 v1 r,
red m1 t1 m2 v1 ->
red m2 t2 m3 r ->
red m1 (trm_seq t1 t2) m3 r
| red_let : forall m1 m2 m3 x t1 t2 v1 r,
......@@ -649,6 +649,17 @@ Fixpoint substs (E:ctx) (t:trm) :=
(* ---------------------------------------------------------------------- *)
(** Properties of iterated substitution *)
(** Simplification equalities for [ctx_rem] *)
Lemma ctx_rem_same : forall x v E,
ctx_rem x ((x,v)::E) = ctx_rem x E.
Proof using. intros. simpl. case_if~. Qed.
Lemma ctx_rem_neq : forall x y v E,
x <> y ->
ctx_rem x ((y,v)::E) = (y,v)::(ctx_rem x E).
Proof using. intros. simpl. case_if~. Qed.
(** Auxiliary results *)
Lemma ctx_rem_fresh : forall x E,
......
......@@ -307,6 +307,7 @@ Ltac hcancel_hook H ::=
Definition is_val_bool (v:val) : Prop :=
exists b, v = val_bool b.
(* todo: deprecated *)
Definition is_val_unit (v:val) : Prop :=
v = val_unit.
......@@ -741,6 +742,7 @@ Proof using.
{ intros v' N. hpull. intros E. inverts~ E. false N. hnfs*. }
Qed.
(* todo: deprecated
Lemma rule_seq : forall t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]) ->
......@@ -761,6 +763,20 @@ Proof using.
{ applys~ red_seq R2. }
{ rewrite <- htop_hstar_htop. hhsimpl. }
Qed.
*)
Lemma rule_seq : forall t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple t2 (Q1 X) Q) ->
triple (trm_seq t1 t2) H Q.
Proof using.
introv M1 M2. intros HF h N.
lets~ (h1'&v1&R1&K1): (rm M1) HF h.
subst. forwards* (h2'&v2&R2&K2): (rm M2) (\Top \* HF) h1'.
exists h2' v2. splits~.
{ applys~ red_seq R1 R2. }
{ rewrite <- htop_hstar_htop. hhsimpl. }
Qed.
Lemma rule_let : forall x t1 t2 H Q Q1,
triple t1 H Q1 ->
......@@ -1220,7 +1236,8 @@ Proof using.
{ applys* red_if_bool. } }
Qed.
(** An alternative statement for [rule_seq] *)
(** An alternative statement for [rule_seq]
todo deprecated
Lemma rule_seq' : forall t1 t2 H Q H1,
triple t1 H (fun r => \[r = val_unit] \* H1) ->
......@@ -1232,7 +1249,7 @@ Proof using.
{ intros v E. hpull; false. }
{ applys rule_extract_hprop. intros. applys M2. }
Qed.
*)
(* ---------------------------------------------------------------------- *)
(** Reformulation of the rule for N-ary functions *)
......
......@@ -176,8 +176,12 @@ Definition wp_fail : formula := local (fun Q =>
Definition wp_val (v:val) : formula := local (fun Q =>
Q v).
(* deprecated
Definition wp_seq (F1 F2:formula) : formula := local (fun Q =>
F1 (fun r => \[r = val_unit] \* F2 Q)).
*)
Definition wp_seq (F1 F2:formula) : formula := local (fun Q =>
F1 (fun X => F2 Q)).
Definition wp_let (F1:formula) (F2of:val->formula) : formula := local (fun Q =>
F1 (fun X => F2of X Q)).
......@@ -222,8 +226,8 @@ Fixpoint wp (E:ctx) (t:trm) : formula :=
match t with
| trm_val v => wp_val v
| trm_var x => wp_var E x
| trm_fun x t1 => wp_val (val_fun x (substs E t1)) (* todo remove x from E *)
| trm_fix f x t1 => wp_val (val_fix f x (substs E t1)) (* todo remove x,f from E *)
| trm_fun x t1 => wp_val (val_fun x (substs (ctx_rem x E) t1))
| trm_fix f x t1 => wp_val (val_fix f x (substs (ctx_rem x (ctx_rem f E)) t1))
| trm_if t0 t1 t2 => wp_if (aux t0) (aux t1) (aux t2)
| trm_seq t1 t2 => wp_seq (aux t1) (aux t2)
| trm_let x t1 t2 => wp_let (aux t1) (fun X => wp (ctx_add x X E) t2)
......@@ -306,7 +310,7 @@ Qed. (* TODO: simplify proof? *)
(** All [wp] are trivially local by construction *)
Lemma is_local_cf : forall E t,
Lemma is_local_wp : forall E t,
is_local (wp E t).
Proof.
intros. destruct t; try solve [ apply is_local_local ].
......@@ -315,43 +319,187 @@ Qed.
(** [remove_local] applies to goal of the form [triple t (local F Q) Q]
and turns it into [triple t (F Q) Q] for a fresh [Q], then calls [xpull] *)
Lemma substs_fun : forall E x t,
substs E (trm_fun x t) = trm_fun x (substs (ctx_rem x E) t).
Proof using. substs_simpl_proof. { fequals; case_if~. } Qed.
Lemma substs_fix : forall E f x t,
substs E (trm_fix f x t) = trm_fix f x (substs (ctx_rem x (ctx_rem f E)) t).
Proof using.
substs_simpl_proof.
{ fequals. case_if~. case_if~.
{ subst. rewrite~ ctx_rem_same. }
{ rewrite~ ctx_rem_neq. } }
Qed.
Lemma substs_seq : forall E t1 t2,
substs E (trm_seq t1 t2)
= trm_seq (substs E t1) (substs E t2).
Proof using. substs_simpl_proof. Qed.
(*todo move*)
Lemma substs_while : forall E t1 t2,
substs E (trm_while t1 t2)
= trm_while (substs E t1) (substs E t2).
Proof using. substs_simpl_proof. Qed.
(*todo move*)
Ltac remove_local :=
match goal with |- triple _ _ ?Q =>
applys triple_local_pre; try (clear Q; intros Q); xpull end.
applys triple_local_pre; try (clear Q; intros Q); xpull; fold wp end.
Lemma weakestpre_elim' : forall F H Q t,
F ===> weakestpre (triple t) ->
H ==> F Q ->
triple t H Q.
Proof using.
introv M N. lets G: triple_weakestpre_pre t Q.
applys~ rule_consequence G. hchanges N. applys M.
Qed.
Lemma weakestpre_elim : forall H Q t,
H ==> weakestpre (triple t) Q ->
triple t H Q.
Proof using.
introv M. lets G: triple_weakestpre_pre t Q.
applys~ rule_consequence G.
Qed.
Definition we E t :=
weakestpre (triple (substs E t)).
Definition wp_sound t := forall E,
wp E t ===> we E t.
Lemma triple_wp_if : forall F1 F2 F3 E t1 t2 t3,
F1 ===> we E t1 ->
F2 ===> we E t2 ->
F3 ===> we E t3 ->
wp_if F1 F2 F3 ===> we E (trm_if t1 t2 t3).
Proof using.
introv M1 M2 M3. applys qimpl_weakestpre_triple. intros Q.
remove_local. rewrite substs_if. applys rule_if.
{ unfolds in M1. applys weakestpre_elim. applys* M1. }
{ intros b. simpl. remove_local ;=> b' M. inverts M. case_if.
{ applys weakestpre_elim. applys* M2. }
{ applys weakestpre_elim. applys* M3. } }
{ intros. applys~ wp_if_val_false. }
Qed.
Lemma triple_wp_seq : forall F1 F2 E t1 t2,
F1 ===> we E t1 ->
F2 ===> we E t2 ->
wp_seq F1 F2 ===> we E (trm_seq t1 t2).
Proof using.
introv M1 M2. applys qimpl_weakestpre_triple. intros Q.
remove_local. rewrite substs_seq. applys rule_seq.
{ applys weakestpre_elim. applys* M1. }
{ intros X. applys weakestpre_elim. applys* M2. }
Qed.
Lemma triple_wp_let : forall F1 F2 E x t1 t2,
F1 ===> we E t1 ->
(forall X, F2 X ===> we (ctx_add x X E) t2) ->
wp_let F1 F2 ===> we E (trm_let x t1 t2).
Proof using.
introv M1 M2. applys qimpl_weakestpre_triple. intros Q.
remove_local. rewrite substs_let. applys rule_let.
{ applys weakestpre_elim. applys* M1. }
{ intros X. applys weakestpre_elim.
rewrite subst_substs_ctx_rem_same. applys* M2. }
Qed.
Lemma triple_wp_val : forall v,
wp_sound (trm_val v).
Proof using.
intros. intros E. simpl. applys qimpl_weakestpre_triple.
intros Q. remove_local.
rewrite substs_val. applys~ rule_val.
Qed.
Lemma triple_wp_fun : forall x t,
wp_sound (trm_fun x t).
Proof using.
intros. intros E. simpl. applys qimpl_weakestpre_triple.
intros Q. remove_local.
rewrite substs_fun. applys~ rule_fun.
Qed.
Lemma triple_wp_fix : forall f x t,
wp_sound (trm_fix f x t).
Proof using.
intros. intros E. simpl. applys qimpl_weakestpre_triple.
intros Q. remove_local.
rewrite substs_fix. applys~ rule_fix.
Qed.
Lemma triple_wp_var : forall x,
wp_sound (trm_var x).
Proof using.
intros. intros E. simpl. applys qimpl_weakestpre_triple.
intros Q. remove_local.
rewrite substs_var. destruct (ctx_lookup x E).
{ apply~ rule_val. }
{ xpull ;=> F. false. }
Qed.
Lemma triple_wp_app : forall t1 t2,
wp_sound (trm_app t1 t2).
Proof using.
intros. intros E. simpl. applys qimpl_weakestpre_triple.
intros Q. remove_local.
rewrite substs_app. applys triple_weakestpre_pre.
Qed.
Lemma triple_wp_while : forall F1 F2 E t1 t2,
F1 ===> we E t1 ->
F2 ===> we E t2 ->
wp_while F1 F2 ===> we E (trm_while t1 t2).
Proof using.
introv M1 M2. applys qimpl_weakestpre_triple. intros Q.
remove_local. rewrite substs_while. applys rule_extract_hforall.
set (R := weakestpre (triple (trm_while (substs E t1) (substs E t2)))).
exists R. simpl. applys rule_extract_hwand_hpure_l.
{ split.
{ applys is_local_weakestpre_triple. }
{ clears Q. applys qimpl_weakestpre_triple. intros Q.
applys rule_while_raw. rewrite <- substs_while. rewrite <- substs_seq.
rewrite <- (substs_val E). rewrite <- substs_if.
applys weakestpre_elim. applys~ triple_wp_if.
{ applys~ triple_wp_seq. { unfold we. rewrite~ substs_while. } }
{ applys triple_wp_val. } } }
{ applys~ weakestpre_elim. }
Qed.
Lemma wp_sound_all : forall t,
wp_sound t.
Proof using.
intros t. induction t; intros E Q.
{ applys triple_wp_val. }
{ applys triple_wp_var. }
{ applys triple_wp_fun. }
{ applys triple_wp_fix. }
{ applys* triple_wp_if. }
{ applys* triple_wp_seq. }
{ applys* triple_wp_let. }
{ applys* triple_wp_app. }
{ applys* triple_wp_while. }
{ admit. }
Qed.
Lemma triple_wp : forall t E Q,
triple (substs E t) (wp E t Q) Q.
Proof using.
intros t. induction t; intros; simpl.
{ remove_local. rewrite substs_val. applys~ rule_val. }
{ remove_local. rename v into x.
rewrite substs_var. destruct (ctx_lookup x E).
{ apply~ rule_val. }
{ xpull ;=> F. false. } }
{ remove_local.
(* TODO: handle binder *)
skip_rewrite (substs E (trm_fun v t) = trm_fun v (substs E t)).
applys~ rule_fun. }
{ remove_local.
(* TODO: handle binder *)
skip_rewrite (substs E (trm_fix v v0 t) = trm_fix v v0 (substs E t)).
applys~ rule_fix. }
{ remove_local. rewrite substs_if. applys rule_if.
{ applys* IHt1. }
{ intros b. simpl. remove_local ;=> b' M. inverts M. case_if.
{ applys* IHt2. }
{ applys* IHt3. } }
{ intros. applys~ wp_if_val_false. } }
admit.
(** will be handled differently
{ remove_local. applys rule_seq'. { applys* IH. } { applys* IH. } }
*)
{ remove_local. rewrite substs_let. applys rule_let.
{ applys* IHt1. }
{ intros X. simpl. rewrite subst_substs_ctx_rem_same. applys IHt2. } }
{ remove_local. rewrite substs_app. apply triple_weakestpre_pre. }
{ admit. } (** will be handled differently *)
{ admit. }
intros. applys weakestpre_elim. applys wp_sound_all.
Qed.
Lemma triple_substs_of_wp : forall t E H Q,
......
......@@ -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 LambdaSemantics LambdaSep SepGPM LambdaSepProofMode LambdaCF LambdaCFTactics LambdaWP LambdaStruct LambdaSepRO LambdaSepROProofMode ExampleROProofMode ExampleListProofMode LambdaSepCredits LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
SRC := TLCbuffer Fmap SepFunctor LambdaSemantics LambdaSep LambdaCFTactics LambdaWP LambdaCF SepGPM LambdaSepProofMode LambdaStruct LambdaSepRO LambdaSepROProofMode ExampleROProofMode ExampleListProofMode LambdaSepCredits LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
# LambdaCFRO
......
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