Commit 0fc463db authored by charguer's avatar charguer

cleanup

parent 7e8eca0c
......@@ -19,11 +19,6 @@ Implicit Types v : val.
(* To move and factorize *)
Notation "F 'PRE' H 'POST' Q" :=
(F H Q)
(at level 69, only parsing) : heap_scope.
(* todo move *)
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
......
......@@ -16,43 +16,53 @@ Ltac auto_star ::= jauto.
Implicit Types p q : loc.
Implicit Types n : int.
Implicit Types v : val.
Implicit Types r : val.
(* ********************************************************************** *)
(* * Tactics to help in the proofs *)
(* To move and factorize *)
Notation "F 'PRE' H 'POST' Q" :=
(F H Q)
(at level 69, only parsing) : heap_scope.
(* todo move *)
(** Tactic to reason about [let y = f x in t],
where [M] is the specification lemma for [f]. *)
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) ->
var_funs (LibList.length Vs) xs ->
triple (substs xs Vs t1) H Q ->
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros h1 h2 D H1.
forwards~ (h1'&v&N1&N2&N3&N4): (rm M) h2 H1.
exists h1' v. splits~. { subst. applys~ red_app_funs_val. }
Qed.
Tactic Notation "xletapp" constr(M) :=
ram_apply_let M;
[ solve [ auto 20 with iFrame ]
| unlock; xpull; simpl ].
Lemma var_funs_exec_elim : forall (n:nat) xs,
var_funs_exec n xs -> (var_funs n xs).
Proof using. introv M. rewrite var_funs_exec_eq in M. rew_istrue~ in M. Qed.
(** Tactic to reason about [let f x = t1 in t2] *)
Hint Resolve var_funs_exec_elim.
Tactic Notation "xletfun" :=
applys rule_letfun; simpl; xpull.
(* ********************************************************************** *)
(* * Formalisation of higher-order iterator on a reference *)
(** Tactic to reason about [triple (f x) H Q], by unfolding
the definition of [f]. *)
Tactic Notation "xdef" :=
rew_nary; rew_vals_to_trms;
match goal with |- triple (trm_apps (trm_val ?f) _) _ _ =>
applys rule_apps_funs;
[unfold f; rew_nary; reflexivity | auto | simpl]
end.
match goal with
| H: f =_ |- _ =>
rew_nary in H;
applys rule_apps_funs;
[ applys H | auto | simpl ]
| |- _ =>
applys rule_apps_funs;
[ unfold f; rew_nary; reflexivity | auto | simpl ]
end
end.
(** Patch to call [unlock] automatically before [xpull] *)
Ltac xpull_main tt ::=
unlock;
xpull_setup tt;
(repeat (xpull_step tt));
xpull_cleanup tt.
(* ********************************************************************** *)
(* * Formalisation of higher-order iterator on a reference *)
(* ---------------------------------------------------------------------- *)
(** Apply a function to the contents of a reference *)
......@@ -72,9 +82,10 @@ Lemma rule_ref_apply : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
POST Q).
Proof using.
introv M. xdef. ram_apply_let rule_get_ro. { auto with iFrame. }
move=>X /=. unlock. xpull=>->. done.
move=>X /=. xpull=>->. done.
Qed.
(* ---------------------------------------------------------------------- *)
(** In-place update of a reference by applying a function *)
......@@ -99,8 +110,12 @@ Proof using.
unlock. move=>y /=. ram_apply rule_set. { auto 10 with iFrame. }
Qed.
(* ********************************************************************** *)
(* * Formalisation of the box data structure : a reference on a reference *)
(* ---------------------------------------------------------------------- *)
(** In-place update of a reference by invoking a function, with representation predicate *)
(** Representation predicate and its properties *)
Definition Box (n:int) (p:loc) :=
Hexists (q:loc), (p ~~~> q) \* (q ~~~> n).
......@@ -132,18 +147,20 @@ Arguments Box_unfold : clear implicits.
Arguments RO_Box_unfold : clear implicits.
Arguments RO_Box_fold : clear implicits.
(*---*)
(* ---------------------------------------------------------------------- *)
(** Get operation *)
(*
let get p =
! (!p)
*)
Definition val_box_get :=
ValFun 'p :=
Let 'q := val_get 'p in
val_get 'q.
Tactic Notation "xletapp" constr(M) :=
ram_apply_let M;
[ solve [ auto 20 with iFrame ]
| unlock; xpull; simpl ].
Lemma rule_box_get : forall p n,
triple (val_box_get p)
PRE (RO (p ~> Box n))
......@@ -154,22 +171,17 @@ Proof using.
ram_apply rule_get_ro. iIntros "_ $". auto. (* TODO : improve. *)
Qed.
(* detailed proof (to keep somewhere for debugging):
intros. xdef. xchange (RO_Box_unfold p). xpull ;=> q.
ram_apply_let rule_get_ro. { auto with iFrame. }
unlock. move=>/= ?. xpull=> ->. apply rule_htop_post.
ram_apply rule_get_ro. { iIntros. iFrame. iIntros. admit. }
*)
(*---*)
(* ---------------------------------------------------------------------- *)
(** Box up2 operation *)
(* let box_twice f p =
let q = !p in
q := f !q + f !q
(*
let up2 f p =
let q = !p in
q := f !q + f !q
*)
Definition val_box_twice :=
Definition val_box_up2 :=
ValFun 'f 'p :=
Let 'q := val_get 'p in
Let 'n1 := val_get 'q in
......@@ -179,54 +191,11 @@ Definition val_box_twice :=
Let 'm := 'a1 '+ 'a2 in
val_set 'q 'm.
(* to move to LamdaSepRo, next to rule_fix *)
Lemma rule_fun : forall x t1 H Q,
H ==> Q (val_fun x t1) ->
Normal H ->
triple (trm_fun x t1) H Q.
Proof using.
introv M HS. intros h1 h2 D P1. exists___. splits*.
{ applys red_fun. }
{ specializes M P1. applys~ on_rw_sub_base. }
Qed.
Lemma rule_let' : forall x t1 t2 H2 H1 H Q Q1,
H ==> (H1 \* H2) ->
triple t1 H1 Q1 ->
(forall (X:val), triple (subst x X t2) (Q1 X \* H2) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using. introv WP M1 M2. applys* rule_consequence WP. applys* rule_let. Qed.
Lemma rule_letfun : forall f x t1 t2 H Q,
(forall F, triple (subst f F t2) (\[F = val_fun x t1] \* H) Q) ->
triple (LetFun f x := t1 in t2) H Q.
Proof using.
introv M. applys rule_let' H (fun F => \[F = val_fun x t1]).
{ hsimpl. }
{ applys rule_fun. hsimpl~. typeclass. }
{ intros F. applys M. }
Qed.
Lemma rule_frame_read_only_conseq : forall t H1 Q1 H2 H Q,
H ==> (H1 \* H2) ->
Normal H1 ->
triple t (RO H1 \* H2) Q1 ->
(Q1 \*+ H1) ===> Q ->
triple t H Q.
Proof using.
introv WP M N WQ. applys* rule_consequence (rm WP) (rm WQ).
forwards~ R: rule_frame_read_only t H2 Q1 H1.
{ rewrite~ hstar_comm. } { rewrite~ hstar_comm. }
Qed.
Arguments RO_Box_fold : clear implicits.
Lemma rule_box_twice : forall (F:int->int) n (f:val) p,
Lemma rule_box_up2 : forall (F:int->int) n (f:val) p,
(forall (x:int), triple (f x)
PRE (RO(p ~> Box n))
POST (fun r => \[r = val_int (F x)])) ->
triple (val_box_twice f p)
triple (val_box_up2 f p)
PRE (p ~> Box n)
POST (fun r => \[r = val_unit] \* p ~> Box (2 * F n)).
Proof using.
......@@ -248,7 +217,11 @@ Proof using.
by math_rewrite (2 * F n = F n + F n)%Z.
Qed.
Arguments rule_box_twice : clear implicits.
Arguments rule_box_up2 : clear implicits.
(* ---------------------------------------------------------------------- *)
(** Box demo program *)
Definition val_box_demo :=
ValFun 'n :=
......@@ -257,32 +230,9 @@ Definition val_box_demo :=
LetFun 'f 'x :=
Let 'a := val_box_get 'p in
'x '+ 'a in
Let 'u := val_box_twice 'f 'p in
Let 'u := val_box_up2 'f 'p in
val_box_get 'p.
(* ideally, ends with :
val_box_twice 'f 'p ;;;
val_box_get 'p.
but requires proving rule_seq, similar to rule_let.
*)
Tactic Notation "xletfun" :=
applys rule_letfun; simpl; xpull.
Tactic Notation "xdef'" := (* todo: this replaces xdef *)
rew_nary; rew_vals_to_trms;
match goal with |- triple (trm_apps (trm_val ?f) _) _ _ =>
match goal with
| H: f =_ |- _ =>
rew_nary in H;
applys rule_apps_funs;
[ applys H | auto | simpl ]
| |- _ =>
applys rule_apps_funs;
[ unfold f; rew_nary; reflexivity | auto | simpl ]
end
end.
Lemma rule_box_demo : forall (n:int),
triple (val_box_demo n)
PRE \[]
......@@ -292,13 +242,12 @@ Proof using.
xletapp rule_ref => ? q ->.
xletapp rule_ref => ? p ->.
xletfun => F HF.
ram_apply_let (rule_box_twice (fun (x:int) => (x + n)%Z) n).
ram_apply_let (rule_box_up2 (fun (x:int) => (x + n)%Z) n).
{ intros. xdef'. xletapp rule_box_get => m ->.
ram_apply rule_add. { iModIntro. auto. } } (* TODO : improve. *)
{ iIntros "Hq Hp". iDestruct (Box_fold with "[$Hq $Hp]") as "$".
auto with iFrame. }
unlock. xpull=> u /= _. apply rule_htop_post. ram_apply rule_box_get.
math_rewrite (2 * (n + n) = 4 * n)%Z.
iIntros "$ !>". auto 10. (* TODO: improve. *)
iIntros "$ !>". auto 10. (* TODO: improve. *)
Qed.
......@@ -14,12 +14,6 @@ Set Implicit Arguments.
From TLC Require Import LibCore.
(* ********************************************************************** *)
Tactic Notation "cases" constr(E) := (* TODO For TLC *)
let H := fresh "Eq" in cases E as H.
(* ********************************************************************** *)
(** * Maps (partial functions) *)
......@@ -494,7 +488,7 @@ Lemma fmap_agree_union_l_inv : forall f1 f2 f3,
fmap_agree f1 f3
/\ fmap_agree f2 f3.
Proof using.
(* TODO: proofs redundant with others above *)
(* LATER: proofs redundant with others above *)
introv M2 M1. split.
{ intros l v1 v2 E1 E2.
specializes M1 l v1 v2 E1. applys~ M2 l v1 v2.
......@@ -829,7 +823,7 @@ Proof using.
unfold fmap_disjoint, map_disjoint. simpl.
lets (l&F): (loc_fresh_nat (null::L)).
exists l. split.
{ intros l'. case_if~. (* --TODO: fix subst *)
{ intros l'. case_if~. (* --LATER: fix TLC substitution in case_if *)
{ subst. right. applys not_not_inv. intros H. applys F.
constructor. applys~ M. } }
{ intro_subst. applys~ F. }
......@@ -847,7 +841,7 @@ Proof using.
{ rewrite fmap_conseq_succ.
destruct (IHk (S l)%nat) as [E|?].
{ intros i N. applys F (S i). applys_eq N 2. math. }
{ simpl. unfold map_union. case_if~. (* --TODO: fix subst *)
{ simpl. unfold map_union. case_if~.
{ subst. right. applys not_not_inv. intros H. applys F 0%nat.
constructor. math_rewrite (l'+0 = l')%nat. applys~ M. } }
{ auto. } } }
......
......@@ -50,14 +50,6 @@ Definition cf_seq (F1 F2:formula) : formula := fun H Q =>
F1 H (fun r => \[r = val_unit] \* H1)
/\ F2 H1 Q.
(* TODO: maybe use the following alternative, like in [LambdaCFLifted]:
Definition cf_seq (F1 : formula) (F2 : formula) : formula := fun H Q =>
exists Q1,
F1 H Q1
/\ F2 H1 Q
/\ (forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]).
*)
Definition cf_let (F1:formula) (F2of:val->formula) : formula := fun H Q =>
exists Q1,
F1 H Q1
......@@ -85,6 +77,14 @@ Definition cf_for (v1 v2:val) (F3:int->formula) : formula := fun H Q =>
(forall i H' Q', F i H' Q' -> S i H' Q') ->
S n1 H Q).
(* LATER: maybe use the following alternative, like in [LambdaCFLifted]:
Definition cf_seq (F1 : formula) (F2 : formula) : formula := fun H Q =>
exists Q1,
F1 H Q1
/\ F2 H1 Q
/\ (forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]).
*)
(* ---------------------------------------------------------------------- *)
(* ** Definition of the CF generator *)
......@@ -384,12 +384,12 @@ Ltac xcf_trm n ::=
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 *)
| val_funs _ _ => (* LATER: use (apply (@..)) instead of applys? same in cflifted *)
applys triple_apps_funs_of_cf_iter n;
[ reflexivity | reflexivity | xcf_post tt ]
| val_fixs _ _ _ =>
applys triple_apps_fixs_of_cf_iter n f';
[ try unfold f'; rew_nary; try reflexivity (* TODO: how in LambdaCF? *)
[ try unfold f'; rew_nary; try reflexivity (* LATE: how in LambdaCF? *)
(* reflexivity *)
| reflexivity
| xcf_post tt ]
......@@ -474,7 +474,7 @@ Ltac xapp_xapply E cont_post :=
match goal with
| |- ?F ?H ?Q => is_evar Q; xapplys E
| |- ?F ?H (fun r => \[r = val_unit] \* ?H') => is_evar H'; xapplys E
(* TODO: might not be needed *)
(* LATER: might not be needed *)
| _ => xapply_core E ltac:(fun tt => hcancel) ltac:(cont_post)
end.
......@@ -508,7 +508,7 @@ Ltac xapp_basic E cont_post tt ::=
xapp_with_args E ltac:(fun H =>
xapp_xapply H cont_post).
(* TODO: xapps should do hsimpl if not in a let *)
(* LATER: xapps should do hsimpl if not in a let *)
(* ---------------------------------------------------------------------- *)
......
......@@ -280,22 +280,6 @@ Proof using. intros. applys* Sound_for_Cf. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Notation for characteristic Formulae *)
(** Notation [F PRE H POST Q] for stating specifications, e.g.
[Triple t PRE H POST Q] is the same as [Triple t H Q] *)
Notation "F 'PRE' H 'POST' Q" :=
(F H Q)
(at level 69, only parsing) : charac.
(** Notation [PRE H CODE F POST Q] for displaying characteristic formulae *)
(*
Notation "'PRE' H 'CODE' F 'POST' Q" :=
(@Local F _ _ H Q) (at level 69,
format "'[v' '[' 'PRE' H ']' '/' '[' 'CODE' F ']' '/' '[' 'POST' Q ']' ']'")
: charac2.
*)
Notation "'`Fail'" :=
(Local (Cf_fail))
(at level 69) : charac.
......
Tactic Notation "xdef" :=
rew_nary; rew_vals_to_trms;
match goal with |- triple (trm_apps (trm_val ?f) _) _ _ =>
applys rule_apps_funs;
[unfold f; rew_nary; reflexivity | auto | simpl]
end.
(* detailed proof (to keep somewhere for debugging):
intros. xdef. xchange (RO_Box_unfold p). xpull ;=> q.
ram_apply_let rule_get_ro. { auto with iFrame. }
unlock. move=>/= ?. xpull=> ->. apply rule_htop_post.
ram_apply rule_get_ro. { iIntros. iFrame. iIntros. admit. }
*)
(* ideally, ends with :
val_box_up2 'f 'p ;;;
val_box_get 'p.
but requires proving rule_seq, similar to rule_let.
*)
(*
Definition is_extractible F :=
forall A (J:A->hprop) Q,
......
......@@ -145,7 +145,7 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m2 (subst x v1 t2) m3 r ->
red m1 (trm_let x t1 t2) m3 r
| red_app_arg : forall m1 m2 m3 m4 t1 t2 v1 v2 r,
(* TODO: add [not_is_val t1 \/ not_is_val t2] *)
(* LATER: add [not_is_val t1 \/ not_is_val t2] *)
red m1 t1 m2 v1 ->
red m2 t2 m3 v2 ->
red m3 (trm_app v1 v2) m4 r ->
......@@ -190,7 +190,7 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m1 (trm_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit) m2 r ->
red m1 (trm_while t1 t2) m2 r
| red_for_arg : forall m1 m2 m3 m4 v1 v2 x t1 t2 t3 r,
(* TODO: add [not_is_val t1 \/ not_is_val t2] *)
(* LATER: add [not_is_val t1 \/ not_is_val t2] *)
red m1 t1 m2 v1 ->
red m2 t2 m3 v2 ->
red m3 (trm_for x v1 v2 t3) m4 r ->
......@@ -593,8 +593,7 @@ Tactic Notation "rew_vals_to_trms" :=
(* ---------------------------------------------------------------------- *)
(** Distinct variables *)
(* TODO: use LibListExec *)
(* TODO: generalize to lists *)
(* LATER: use LibListExec and generalize to lists *)
Fixpoint var_fresh (y:var) (xs:vars) : bool :=
match xs with
......@@ -625,7 +624,7 @@ Proof using.
introv N. induction t; simpl; try solve [ fequals;
repeat case_if; simpl; repeat case_if; auto ].
repeat case_if; simpl; repeat case_if~.
Qed. (* TODO: simplify *)
Qed. (* LATER: simplify *)
Lemma subst_substs : forall x v ys ws t,
var_fresh x ys ->
......@@ -681,11 +680,12 @@ Definition var_funs (n:nat) (xs:vars) : Prop :=
/\ length xs = n
/\ xs <> nil.
(** Computable version of the above definition *)
(** Computable version of the above definition
LATER use TLC exec *)
Definition var_funs_exec (n:nat) (xs:vars) : bool := (* --todo: use exec typeclass *)
Definition var_funs_exec (n:nat) (xs:vars) : bool :=
nat_compare n (List.length xs)
&& is_not_nil xs (* --todo: rename to exec *)
&& is_not_nil xs
&& var_distinct xs.
Lemma var_funs_exec_eq : forall n xs,
......@@ -703,9 +703,9 @@ Definition var_fixs (f:var) (n:nat) (xs:vars) : Prop :=
/\ length xs = n
/\ xs <> nil.
Definition var_fixs_exec (f:var) (n:nat) (xs:vars) : bool := (* todo: use exec typeclass *)
Definition var_fixs_exec (f:var) (n:nat) (xs:vars) : bool :=
nat_compare n (List.length xs)
&& is_not_nil xs (* todo: rename to exec *)
&& is_not_nil xs
&& var_distinct (f::xs).
Lemma var_fixs_exec_eq : forall f n xs,
......
......@@ -126,8 +126,6 @@ Open Scope heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Tactic for automation *)
(* TODO: check how much is really useful *)
Hint Extern 1 (_ = _ :> heap) => fmap_eq.
Tactic Notation "fmap_disjoint_pre" :=
......@@ -419,7 +417,7 @@ Qed.
(** Tactic for helping reasoning about concrete calls to [alloc] *)
Ltac simpl_abs := (* TODO: will be removed once [abs] computes *)
Ltac simpl_abs := (* LATER: will be removed once [abs] computes *)
match goal with
| |- context [ abs 0 ] => change (abs 0) with 0%nat
| |- context [ abs 1 ] => change (abs 1) with 1%nat
......@@ -589,7 +587,7 @@ Proof using.
asserts Z: ((\[False] \* \Top \* HF) h1').
{ applys himpl_trans K1. hchange M3. hsimpl. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. } (* TODO: shorten this *)
lets: hpure_inv Z. false*. } (* LATER: shorten this *)
Qed.
Lemma rule_if_bool : forall (b:bool) t1 t2 H Q,
......@@ -617,7 +615,7 @@ Proof using.
{ applys himpl_trans K1. hchange~ M2. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. }
(* TODO: 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'.
exists h2' v2. splits~.
{ applys~ red_seq R2. }
......@@ -682,11 +680,11 @@ Qed.
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
wf R ->
(H ==> (Hexists b X, I b X) \* \Top) -> (* TODO: replace \top with H' *)
(H ==> (Hexists b X, I b X) \* \Top) -> (* LATER: replace \top with H' *)
(forall t b X,
(forall b' X', R X' X -> triple t (I b' X') Q) ->
triple (trm_if t1 (trm_seq t2 t) val_unit) (I b X) Q) ->
triple (trm_while t1 t2) H Q. (* TODO: allow for weakening on Q *)
triple (trm_while t1 t2) H Q. (* LATER: allow for weakening on Q *)
Proof using.
introv WR H0 HX. xchange (rm H0). xpull ;=> b0 X0.
rewrite hstar_comm. applys rule_htop_pre. gen b0.
......@@ -705,7 +703,7 @@ Proof using.
exists h' v. splits~. { applys~ red_for. }
Qed.
(* TODO: simplify proof using rule_for_raw *)
(* LATER: simplify proof using rule_for_raw *)
Lemma rule_for_gt : forall x n1 n2 t3 H Q,
n1 > n2 ->
(fun r => \[r = val_unit] \* H) ===> (Q \*+ \Top) ->
......@@ -716,7 +714,7 @@ Proof using.
{ hhsimpl. hchange~ M. hsimpl. }
Qed.
(* TODO: simplify proof using rule_for_raw *)
(* LATER: simplify proof using rule_for_raw *)
Lemma rule_for_le : forall Q1 x n1 n2 t3 H Q,
n1 <= n2 ->
triple (subst x n1 t3) H Q1 ->
......@@ -731,14 +729,14 @@ Proof using.
{ applys himpl_trans K1. hchange~ M3. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. }
(* TODO: shorten this, and factorize with rule_if *)
(* LATER: shorten this, and factorize with rule_if *)
subst. forwards* (h2'&v2&R2&K2): (rm M2) (\Top \* HF) h1'.
exists h2' v2. splits~.
{ applys* red_for_le. }
{ rewrite <- htop_hstar_htop. hhsimpl. }
Qed.
(* TODO: simplify proof using rule_for_raw *)
(* LATER: simplify proof using rule_for_raw *)
Lemma rule_for : forall x (n1 n2:int) t3 H Q,
(If (n1 <= n2) then
(exists Q1,
......@@ -754,7 +752,7 @@ Proof using.
{ xapplys* rule_for_gt. { math. } intros r. hchanges* M. }
Qed.
(* TODO: simplify proof using rule_for_raw *)
(* LATER: simplify proof using rule_for_raw *)
Lemma rule_for_inv : forall (I:int->hprop) H' x n1 n2 t3 H Q,
(n1 <= n2+1) ->
(H ==> I n1 \* H') ->
......
......@@ -21,21 +21,6 @@ Open Scope fmap_scope.
Arguments exist [A] [P].
(* -- TODO: move to TLC LibTactics *)
Ltac fequal_base ::=
let go := f_equal_fixed; [ fequal_base | ] in
match goal with
| |- exist _ _ = exist _ _ => apply exist_eq_exist
| |- (_,_,_) = (_,_,_) => go
| |- (_,_,_,_) = (_,_,_,_) => go
| |- (_,_,_,_,_) = (_,_,_,_,_) => go
| |- (_,_,_,_,_,_) = (_,_,_,_,_,_) => go
| |- _ => f_equal_fixed
end.
(* ********************************************************************** *)
(* * Construction of core of the logic *)
......@@ -154,6 +139,17 @@ Hint Extern 1 (\# _ _ _) => fmap_disjoint_pre.
Hint Resolve fmap_agree_sym.
(* LATER: move to TLC; (this cannot be put in TLCbuffer) *)
Ltac fequal_base ::=
let go := f_equal_fixed; [ fequal_base | ] in
match goal with
| |- exist _ _ = exist _ _ => apply exist_eq_exist
| |- (_,_,_) = (_,_,_) => go
| |- (_,_,_,_) = (_,_,_,_) => go
| |- (_,_,_,_,_) = (_,_,_,_,_) => go
| |- (_,_,_,_,_,_) = (_,_,_,_,_,_) => go
| |- _ => f_equal_fixed
end.
(* ---------------------------------------------------------------------- *)
(* ** Equalities on [heap] *)
......@@ -1122,6 +1118,7 @@ Ltac xpull_hprop tt ::= apply xpull_hprop; intro.
Ltac xpull_hexists tt ::= apply xpull_hexists; intro.
Ltac xpull_id tt ::= apply xpull_id; intro.
(* ---------------------------------------------------------------------- *)
(* ** Customizing xchange for RO triples, which are not local *)
......@@ -1158,6 +1155,16 @@ Proof using.
{ specializes M P1. applys~ on_rw_sub_base. }
Qed.
Lemma rule_fun : forall x t1 H Q,
H ==> Q (val_fun x t1) ->
Normal H ->
triple (trm_fun x t1) H Q.
Proof using.
introv M HS. intros h1 h2 D P1. exists___. splits*.
{ applys red_fun. }
{ specializes M P1. applys~ on_rw_sub_base. }
Qed.
Lemma rule_fix : forall f x t1 H Q,
H ==> Q (val_fix f x t1) ->
Normal H ->
......@@ -1551,8 +1558,9 @@ Proof using.
applys rule_consequence N. { hsimpl. } { intros x. hsimpl. apply normally_erase. }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Definition ofe the ROFrame connective *)
(* ** Definition of the ROFrame connective *)
Definition ROFrame (H1 H2 : hprop) :=
Hexists H3, normally H3 \* (RO(H3) \--* H1) \* (H3 \--* H2).
......@@ -1663,6 +1671,57 @@ Proof.
hchange (qwand_himpl_hwand X). hchange (hwand_cancel (Q1 X) (Q' X)). hsimpl.
Qed.
(* ********************************************************************** *)
(* * Derived rules for practical proofs *)
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) ->
var_funs (LibList.length Vs) xs ->
triple (substs xs Vs t1) H Q ->
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros h1 h2 D H1.
forwards~ (h1'&v&N1&N2&N3&N4): (rm M) h2 H1.
exists h1' v. splits~. { subst. applys~ red_app_funs_val. }
Qed.
Lemma var_funs_exec_elim : forall (n:nat) xs,
var_funs_exec n xs -> (var_funs n xs).
Proof using. introv M. rewrite var_funs_exec_eq in M. rew_istrue~ in M. Qed.
Hint Resolve var_funs_exec_elim.
Lemma rule_let' : forall x t1 t2 H2 H1 H Q Q1,