...
 
Commits (6)
...@@ -4195,4 +4195,70 @@ Ltac xwhile_core xwhile_tactic ::= ...@@ -4195,4 +4195,70 @@ Ltac xwhile_core xwhile_tactic ::=
*) *)
*) *)
\ No newline at end of file (** Encoding of sequences *)
Definition trm_seq (t1:trm) (t2:trm) : trm :=
trm_tag tag_seq (trm_let "$_" t1 (trm_unbind "$_" t2)).
(** Encoding of while loops *)
Definition trm_while (t1:trm) (t2:trm) : trm :=
let F : var := "$f" in
let U : var := "$_" in
let P t := trm_unbind F (trm_unbind U t) in
let X : val := val_fix F U (trm_if (P t1) (trm_seq (P t2) (F val_unit)) val_unit) in
trm_tag tag_while (X val_unit).
(*
Lemma red_app_fun : forall m1 m2 v1 v2 x t r,
var_special x = false ->
v1 = val_fun x t ->
red m1 (subst x v2 t) m2 r ->
red m1 (trm_app v1 v2) m2 r.
Proof using. intros. applys* red_app_fun_precise. Qed.
*)
(* todo: deprecated
Lemma red_seq_unit : forall m1 m2 m3 t1 t2 r,
red m1 t1 m2 val_unit ->
red m2 t2 m3 r ->
red m1 (trm_seq t1 t2) m3 r.
Proof using.
introv M1 M2. applys* red_let.
simpl. applys* red_unbind.
Qed.
*)
(* todo: deprecated
Lemma red_seq' : forall m1 m2 t1 t2 r,
let x : var := "$_" in
red m1 (trm_let x t1 (trm_unbind x t2)) m2 r ->
red m1 (trm_seq t1 t2) m2 r.
Proof using.
introv M. inverts M as. intros m3 r1 M1 M2.
inverts M2 as. intros M3. applys* red_seq.
Qed.
*)
(* todo: deprecated
Lemma red_while' : forall t1 t2 m1 m2 r,
let F : var := "$f" in
let U : var := "$_" in
let P t := trm_unbind F (trm_unbind U t) in
red m1 ((val_fix F U (trm_if (P t1) (trm_seq (P t2) (F val_unit)) val_unit)) val_unit) m2 r ->
red m1 (trm_while t1 t2) m2 r.
Proof using.
introv M1. applys red_while. ...
Qed.
*)
This diff is collapsed.
...@@ -529,6 +529,21 @@ Qed. ...@@ -529,6 +529,21 @@ Qed.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(* ** Term rules *) (* ** Term rules *)
Lemma rule_red : forall t1 t2 H Q,
(forall m m' r, red m t1 m' r -> red m t2 m' r) ->
triple t1 H Q ->
triple t2 H Q.
Proof using.
introv T M. intros Hf h N. lets~ (h'&v&R&K): (rm M) Hf h.
exists h' v. splits~.
Qed.
Lemma rule_unbind : forall x t1 H Q,
triple t1 H Q ->
triple (trm_unbind x t1) H Q.
Proof using. introv M. applys rule_red M. applys red_unbind. Qed.
Lemma rule_val : forall v H Q, Lemma rule_val : forall v H Q,
H ==> Q v -> H ==> Q v ->
triple (trm_val v) H Q. triple (trm_val v) H Q.
...@@ -587,7 +602,8 @@ Proof using. ...@@ -587,7 +602,8 @@ Proof using.
{ intros v' N. hpull. intros E. inverts~ E. false N. hnfs*. } { intros v' N. hpull. intros E. inverts~ E. false N. hnfs*. }
Qed. Qed.
Lemma rule_seq : forall t1 t2 H Q Q1, (* todo: deprecated
Lemma rule_seq_unit : forall t1 t2 H Q Q1,
triple t1 H Q1 -> triple t1 H Q1 ->
(forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]) -> (forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]) ->
triple t2 (Q1 val_unit) Q -> triple t2 (Q1 val_unit) Q ->
...@@ -604,16 +620,18 @@ Proof using. ...@@ -604,16 +620,18 @@ Proof using.
(* LATER: shorten this, and factorize with rule_if *) (* LATER: shorten this, and factorize with rule_if *)
subst. forwards* (h2'&v2&R2&K2): (rm M3) (\Top \* HF) h1'. subst. forwards* (h2'&v2&R2&K2): (rm M3) (\Top \* HF) h1'.
exists h2' v2. splits~. exists h2' v2. splits~.
{ applys~ red_seq R2. } { applys~ red_seq_unit R2. }
{ rewrite <- htop_hstar_htop. hhsimpl. } { rewrite <- htop_hstar_htop. hhsimpl. }
Qed. Qed.
*)
Lemma rule_let : forall x t1 t2 H Q Q1, Lemma rule_let_general : forall x t1 t2 H Q Q1,
x <> var_special "_" ->
triple t1 H Q1 -> triple t1 H Q1 ->
(forall (X:val), triple (subst x X t2) (Q1 X) Q) -> (forall (X:val), triple (subst x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q. triple (trm_let x t1 t2) H Q.
Proof using. Proof using.
introv M1 M2. intros HF h N. introv F M1 M2. intros HF h N.
lets~ (h1'&v1&R1&K1): (rm M1) HF h. lets~ (h1'&v1&R1&K1): (rm M1) HF h.
forwards* (h2'&v2&R2&K2): (rm M2) (\Top \* HF) h1'. forwards* (h2'&v2&R2&K2): (rm M2) (\Top \* HF) h1'.
exists h2' v2. splits~. exists h2' v2. splits~.
...@@ -621,6 +639,24 @@ Proof using. ...@@ -621,6 +639,24 @@ Proof using.
{ rewrite <- htop_hstar_htop. hhsimpl. } { rewrite <- htop_hstar_htop. hhsimpl. }
Qed. Qed.
Lemma rule_let : forall (x:name) t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple (subst x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using. intros. applys* rule_let_general. auto. 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. applys rule_red. applys red_seq_encoded.
applys rule_let_general.
{ auto. }
{ applys M1. }
{ simpl. intros. applys rule_unbind. applys M2. }
Qed.
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q, Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) -> F = (val_funs xs t1) ->
var_funs (length Vs) xs -> var_funs (length Vs) xs ->
...@@ -628,7 +664,7 @@ Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q, ...@@ -628,7 +664,7 @@ Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
triple (trm_apps F Vs) H Q. triple (trm_apps F Vs) H Q.
Proof using. Proof using.
introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf. introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
exists h' v. splits~. { subst. applys* red_app_funs_val. } exists h' v. splits~. { subst. applys* red_app_funs_val. admit. (*todo side*) }
Qed. Qed.
Lemma rule_apps_fixs : forall xs f F (Vs:vals) t1 H Q, Lemma rule_apps_fixs : forall xs f F (Vs:vals) t1 H Q,
...@@ -638,7 +674,7 @@ Lemma rule_apps_fixs : forall xs f F (Vs:vals) t1 H Q, ...@@ -638,7 +674,7 @@ Lemma rule_apps_fixs : forall xs f F (Vs:vals) t1 H Q,
triple (trm_apps F Vs) H Q. triple (trm_apps F Vs) H Q.
Proof using. Proof using.
introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf. introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
exists h' v. splits~. { subst. applys* red_app_fixs_val. } exists h' v. splits~. { subst. applys* red_app_fixs_val. admit. (*todo side*) }
Qed. Qed.
...@@ -663,6 +699,18 @@ Proof using. ...@@ -663,6 +699,18 @@ Proof using.
introv M. applys M. introv K. applys rule_while_raw. applys K. introv M. applys M. introv K. applys rule_while_raw. applys K.
Qed. Qed.
(* todo: investigate
Lemma rule_while' : forall t1 t2 H Q,
(forall t,
(forall H' Q', triple (trm_if t1 (trm_seq t2 t) val_unit) H' Q' ->
triple t H' Q') ->
triple t H Q) ->
triple (trm_while t1 t2) H Q.
Proof using.
introv M. applys rule_red.
Qed.
*)
Lemma rule_while_inv : forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop) t1 t2 H, Lemma rule_while_inv : forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop) t1 t2 H,
let Q := (fun r => \[r = val_unit] \* Hexists Y, I false Y) in let Q := (fun r => \[r = val_unit] \* Hexists Y, I false Y) in
wf R -> wf R ->
...@@ -1025,6 +1073,7 @@ Qed. ...@@ -1025,6 +1073,7 @@ Qed.
(** Combination of [rule_let] and [rule_val] *) (** Combination of [rule_let] and [rule_val] *)
(** todo fix
Lemma rule_let_val : forall x v1 t2 H Q, Lemma rule_let_val : forall x v1 t2 H Q,
(forall (X:val), X = v1 -> triple (subst x X t2) H Q) -> (forall (X:val), X = v1 -> triple (subst x X t2) H Q) ->
triple (trm_let x (trm_val v1) t2) H Q. triple (trm_let x (trm_val v1) t2) H Q.
...@@ -1034,6 +1083,7 @@ Proof using. ...@@ -1034,6 +1083,7 @@ Proof using.
{ applys rule_val. hsimpl~. } { applys rule_val. hsimpl~. }
{ intros X. applys rule_extract_hprop. intro_subst. applys M'. } { intros X. applys rule_extract_hprop. intro_subst. applys M'. }
Qed. Qed.
*)
(** A rule of conditionals with case analysis already done *) (** A rule of conditionals with case analysis already done *)
...@@ -1066,19 +1116,19 @@ Proof using. ...@@ -1066,19 +1116,19 @@ Proof using.
{ applys* red_if_bool. } } { applys* red_if_bool. } }
Qed. Qed.
(** An alternative statement for [rule_seq] *) (** An alternative statement for [rule_seq_unit] -- deprecated *)
(* todo fix
Lemma rule_seq' : forall t1 t2 H Q H1, Lemma rule_seq_unit' : forall t1 t2 H Q H1,
triple t1 H (fun r => \[r = val_unit] \* H1) -> triple t1 H (fun r => \[r = val_unit] \* H1) ->
triple t2 H1 Q -> triple t2 H1 Q ->
triple (trm_seq t1 t2) H Q. triple (trm_seq t1 t2) H Q.
Proof using. Proof using.
introv M1 M2. applys rule_seq. introv M1 M2. applys rule_seq_unit.
{ applys M1. } { applys M1. }
{ intros v E. hpull; false. } { intros v E. hpull; false. }
{ applys rule_extract_hprop. intros. applys M2. } { applys rule_extract_hprop. intros. applys M2. }
Qed. Qed.
*)
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** Reformulation of the rule for N-ary functions *) (** Reformulation of the rule for N-ary functions *)
......
...@@ -18,6 +18,7 @@ Implicit Types t : trm. ...@@ -18,6 +18,7 @@ Implicit Types t : trm.
(* ********************************************************************** *) (* ********************************************************************** *)
(* * WP generator *) (* * WP generator *)
...@@ -170,6 +171,8 @@ Proof using. intros. unfolds. rewrite~ local_local. Qed. ...@@ -170,6 +171,8 @@ Proof using. intros. unfolds. rewrite~ local_local. Qed.
(** These auxiliary definitions give the characteristic formula (** These auxiliary definitions give the characteristic formula
associated with each term construct. *) associated with each term construct. *)
Definition wp_tag (g:tag) (F:formula) : formula := F.
Definition wp_fail : formula := local (fun Q => Definition wp_fail : formula := local (fun Q =>
\[False]). \[False]).
...@@ -179,6 +182,9 @@ Definition wp_val (v:val) : formula := local (fun Q => ...@@ -179,6 +182,9 @@ Definition wp_val (v:val) : formula := local (fun Q =>
Definition wp_seq (F1 F2:formula) : formula := local (fun Q => Definition wp_seq (F1 F2:formula) : formula := local (fun Q =>
F1 (fun r => \[r = val_unit] \* F2 Q)). F1 (fun r => \[r = val_unit] \* F2 Q)).
Definition wp_seq' (F1 F2:formula) : formula := local (fun Q =>
F1 (fun r => F2 Q)).
Definition wp_let (F1:formula) (F2of:val->formula) : formula := local (fun Q => Definition wp_let (F1:formula) (F2of:val->formula) : formula := local (fun Q =>
F1 (fun X => F2of X Q)). F1 (fun X => F2of X Q)).
...@@ -217,6 +223,7 @@ Definition wp_var (E:ctx) (x:var) : formula := ...@@ -217,6 +223,7 @@ Definition wp_var (E:ctx) (x:var) : formula :=
| Some v => (fun Q => Q v) | Some v => (fun Q => Q v)
end). end).
Fixpoint wp (E:ctx) (t:trm) : formula := Fixpoint wp (E:ctx) (t:trm) : formula :=
let aux := wp E in let aux := wp E in
match t with match t with
...@@ -225,15 +232,30 @@ Fixpoint wp (E:ctx) (t:trm) : formula := ...@@ -225,15 +232,30 @@ Fixpoint wp (E:ctx) (t:trm) : formula :=
| trm_fun x t1 => wp_val (val_fun x (substs E t1)) (* todo remove x from E *) | 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_fix f x t1 => wp_val (val_fix f x (substs E t1)) (* todo remove x,f from E *)
| trm_if t0 t1 t2 => wp_if (aux t0) (aux t1) (aux t2) | 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) | trm_let x t1 t2 => wp_let (aux t1) (fun X => wp (ctx_add x X E) t2)
| trm_app t1 t2 => local (weakestpre (triple (substs E t))) | trm_app t1 t2 => local (weakestpre (triple (substs E t)))
| trm_while t1 t2 => wp_while (aux t1) (aux t2)
| trm_for x t1 t2 t3 => wp_for' (aux t1) (aux t2) (fun X => wp (ctx_add x X E) t3) | trm_for x t1 t2 t3 => wp_for' (aux t1) (aux t2) (fun X => wp (ctx_add x X E) t3)
| trm_protect x t1 => wp (ctx_rem x E) t1
| trm_tag g t0 =>
match g, t0 with
(*| tag_seq, trm_let "$_" t1 (trm_protect "$_" t2) =>
wp_seq' (aux t1) (wp (ctx_rem "$_" E) t2) *)
| tag_seq, trm_let x t1 (trm_protect y t2) =>
if eq_var_dec x y
then wp_seq' (aux t1) (wp (ctx_rem x E) t2)
else wp_fail
(*
| tag_while, trm_app (val_fix "$f" "$_" (trm_if (trm_protect "$f" (trm_protect "$_" t1))
(trm_let "$_" (trm_protect "$f" (trm_protect U t2))
((trm_protect "$_" t2 (trm_app "$f" val_unit)))
val_unit)) val_unit =>
let aux := wp (ctx_rem "$_" (ctx_rem "$f" E)) in
wp_while (aux t1) (aux t2)*)
| _,_ => wp_fail
end
end. end.
(* ********************************************************************** *) (* ********************************************************************** *)
(* * Soundness proof *) (* * Soundness proof *)
...@@ -309,9 +331,18 @@ Qed. (* TODO: simplify proof? *) ...@@ -309,9 +331,18 @@ Qed. (* TODO: simplify proof? *)
Lemma is_local_cf : forall E t, Lemma is_local_cf : forall E t,
is_local (wp E t). is_local (wp E t).
Proof. Proof.
intros. destruct t; try solve [ apply is_local_local ]. intros. gen E. induction t; intros;
try solve [ apply is_local_local | eauto ].
{ simpl. rename t into g.
destruct g; try apply is_local_local.
destruct t0; try applys is_local_local.
destruct t0_2; try applys is_local_local.
case_if; try applys is_local_local. }
Qed. Qed.
(** [remove_local] applies to goal of the form [triple t (local F Q) Q] (** [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] *) and turns it into [triple t (F Q) Q] for a fresh [Q], then calls [xpull] *)
...@@ -319,6 +350,13 @@ Ltac remove_local := ...@@ -319,6 +350,13 @@ Ltac remove_local :=
match goal with |- triple _ _ ?Q => 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 end.
(** Triples with [wp_fail] as precondition are always valid. *)
Lemma triple_wp_fail : forall t Q,
triple t (wp_fail Q) Q.
Proof using. intros. remove_local. intros. false. Qed.
Lemma triple_wp : forall t E Q, Lemma triple_wp : forall t E Q,
triple (substs E t) (wp E t Q) Q. triple (substs E t) (wp E t Q) Q.
Proof using. Proof using.
...@@ -342,16 +380,21 @@ Proof using. ...@@ -342,16 +380,21 @@ Proof using.
{ applys* IHt2. } { applys* IHt2. }
{ applys* IHt3. } } { applys* IHt3. } }
{ intros. applys~ wp_if_val_false. } } { 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. { remove_local. rewrite substs_let. applys rule_let.
{ applys* IHt1. } { applys* IHt1. }
{ intros X. simpl. rewrite subst_substs_ctx_rem_same. applys IHt2. } } { intros X. simpl. rewrite subst_substs_ctx_rem_same. applys IHt2. } }
{ remove_local. rewrite substs_app. apply triple_weakestpre_pre. } { remove_local. rewrite substs_app. apply triple_weakestpre_pre. }
{ admit. } (** will be handled differently *) { admit. } (** will be handled differently *)
{ admit. } { admit. }
{ rewrite substs_protect. applys rule_protect. applys IHt. }
{ rename t into g. destruct g; try apply triple_wp_fail.
destruct t0; try apply triple_wp_fail.
destruct t0_2; try apply triple_wp_fail.
case_if; try apply triple_wp_fail. subst.
renames v0 to x, t0_1 to t1, t0_2 to t2.
rewrite substs_tag. applys rule_tag.
simpl in IHt. case_if. unfolds wp_let.
unfold wp_seq'. apply IHt. }
Qed. Qed.
Lemma triple_substs_of_wp : forall t E H Q, Lemma triple_substs_of_wp : forall t E H Q,
...@@ -368,44 +411,13 @@ Proof using. introv M. xchanges M. applys triple_wp. Qed. ...@@ -368,44 +411,13 @@ Proof using. introv M. xchanges M. applys triple_wp. Qed.
(* ********************************************************************** *) (* ********************************************************************** *)
(* * Alternative definition of the CF generator *) (* * Alternative definition of the CF generator *)
(*
Module WP2. Module WP2.
(* ********************************************************************** *) (* ********************************************************************** *)
(* * Size of a term *) (* * Size of a term *)
(* ---------------------------------------------------------------------- *)
(** Size of a term, where all values counting for one unit. *)
Fixpoint trm_size (t:trm) : nat :=
match t with
| trm_var x => 1
| trm_val v => 1
| trm_fun x t1 => 1 + trm_size t1
| trm_fix f x t1 => 1 + trm_size t1
| trm_if t0 t1 t2 => 1 + trm_size t0 + trm_size t1 + trm_size t2
| trm_seq t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_let x t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_app t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_while t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_for x t1 t2 t3 => 1 + trm_size t1 + trm_size t2 + trm_size t3
end.
Lemma trm_size_subst : forall t x v,
trm_size (subst x v t) = trm_size t.
Proof using.
intros. induction t; simpl; repeat case_if; auto.
Qed.
(** Hint for induction on size. Proves subgoals of the form
[measure trm_size t1 t2], when [t1] and [t2] may have some
structure or involve substitutions. *)
Ltac solve_measure_trm_size tt :=
unfold measure in *; simpls; repeat rewrite trm_size_subst; math.
Hint Extern 1 (measure trm_size _ _) => solve_measure_trm_size tt.
(** The CF generator is a recursive function, defined using the (** The CF generator is a recursive function, defined using the
optimal fixed point combinator (from TLC). [wp_def] gives the optimal fixed point combinator (from TLC). [wp_def] gives the
function, and [cf] is then defined as the fixpoint of [wp_def]. function, and [cf] is then defined as the fixpoint of [wp_def].
...@@ -522,6 +534,8 @@ Qed. ...@@ -522,6 +534,8 @@ Qed.
End WP2. End WP2.
*)
(* ********************************************************************** *) (* ********************************************************************** *)
(* * Practical proofs using characteristic formulae *) (* * Practical proofs using characteristic formulae *)
...@@ -542,7 +556,7 @@ Notation "'`If' v 'Then' F1 'Else' F2" := ...@@ -542,7 +556,7 @@ Notation "'`If' v 'Then' F1 'Else' F2" :=
(at level 69) : charac. (at level 69) : charac.
Notation "'`Seq' F1 ;;; F2" := Notation "'`Seq' F1 ;;; F2" :=
((wp_seq F1 F2)) ((wp_seq' F1 F2))
(at level 68, right associativity, (at level 68, right associativity,
format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac. format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac.
...@@ -603,7 +617,7 @@ Qed. ...@@ -603,7 +617,7 @@ Qed.
(*
Module WP2Aux. Module WP2Aux.
Import WP2. Import WP2.
...@@ -635,6 +649,7 @@ Qed. ...@@ -635,6 +649,7 @@ Qed.
End LemmasCf. End LemmasCf.
End WP2Aux. End WP2Aux.
*)
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** ** Database of lemmas *) (** ** Database of lemmas *)
...@@ -771,15 +786,56 @@ Definition val_incr := ...@@ -771,15 +786,56 @@ Definition val_incr :=
Lemma rule_incr : forall (p:loc) (n:int), Lemma rule_incr : forall (p:loc) (n:int),
triple (val_incr p) triple (val_incr p)
(p ~~~> n) (p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))). (fun r => (p ~~~> (n+1))).
Proof using. Proof using.
intros. xcf. intros. xcf.
xlet. { xapp. xapplys rule_get. } xlet. { xapp. xapplys rule_get. }
intros x. hpull ;=> E. subst. intros x. hpull ;=> E. subst.
xlet. { xapp. xapplys rule_add. } xlet. { xapp. xapplys rule_add. }
intros y. hpull ;=> E. subst. intros y. hpull ;=> E. subst.
xapp. xapplys rule_set. auto. xapp. xapplys rule_set.
Qed. Qed.
Definition val_incr2 :=
ValFun 'p :=
val_incr 'p ;;;
val_incr 'p.
Lemma rule_incr2 : forall (p:loc) (n:int),
triple (val_incr2 p)
(p ~~~> n)
(fun r => (p ~~~> (n+2))).
Proof using.
intros. xcf.
xlet. { xapp. xapplys rule_incr. }
hnf. intros _.
xapp. xapplys rule_incr.
hnf. intros _.
math_rewrite (n+2 = n+1+1). hsimpl.
Qed.
......
...@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term ...@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
# Compilation. # Compilation.
# Note: double space below is important for export.sh # 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 SepGPM LambdaSepProofMode LambdaCF LambdaStruct LambdaSepRO LambdaSepROProofMode ExampleROProofMode ExampleListProofMode LambdaSepCredits LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
# LambdaCFRO # LambdaCFRO
......