Commit a03f2ca2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'iris-proofmode' of gitlab.inria.fr:charguer/cfml into iris-proofmode

parents 6e11695f 0fc463db
...@@ -19,11 +19,6 @@ Implicit Types v : val. ...@@ -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 *) (* todo move *)
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q, Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
......
...@@ -16,43 +16,53 @@ Ltac auto_star ::= jauto. ...@@ -16,43 +16,53 @@ Ltac auto_star ::= jauto.
Implicit Types p q : loc. Implicit Types p q : loc.
Implicit Types n : int. Implicit Types n : int.
Implicit Types v : val. Implicit Types r : val.
(* ********************************************************************** *)
(* * Tactics to help in the proofs *)
(* To move and factorize *) (** Tactic to reason about [let y = f x in t],
Notation "F 'PRE' H 'POST' Q" := where [M] is the specification lemma for [f]. *)
(F H Q)
(at level 69, only parsing) : heap_scope.
(* todo move *)
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q, Tactic Notation "xletapp" constr(M) :=
F = (val_funs xs t1) -> ram_apply_let M;
var_funs (LibList.length Vs) xs -> [ solve [ auto 20 with iFrame ]
triple (substs xs Vs t1) H Q -> | unlock; xpull; simpl ].
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, (** Tactic to reason about [let f x = t1 in t2] *)
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. Tactic Notation "xletfun" :=
applys rule_letfun; simpl; xpull.
(* ********************************************************************** *) (** Tactic to reason about [triple (f x) H Q], by unfolding
(* * Formalisation of higher-order iterator on a reference *) the definition of [f]. *)
Tactic Notation "xdef" := Tactic Notation "xdef" :=
rew_nary; rew_vals_to_trms; rew_nary; rew_vals_to_trms;
match goal with |- triple (trm_apps (trm_val ?f) _) _ _ => match goal with |- triple (trm_apps (trm_val ?f) _) _ _ =>
applys rule_apps_funs; match goal with
[unfold f; rew_nary; reflexivity | auto | simpl] | H: f =_ |- _ =>
end. 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 *) (** 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), ...@@ -72,9 +82,10 @@ Lemma rule_ref_apply : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
POST Q). POST Q).
Proof using. Proof using.
introv M. xdef. ram_apply_let rule_get_ro. { auto with iFrame. } introv M. xdef. ram_apply_let rule_get_ro. { auto with iFrame. }
move=>X /=. unlock. xpull=>->. done. move=>X /=. xpull=>->. done.
Qed. Qed.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** In-place update of a reference by applying a function *) (** In-place update of a reference by applying a function *)
...@@ -99,8 +110,12 @@ Proof using. ...@@ -99,8 +110,12 @@ Proof using.
unlock. move=>y /=. ram_apply rule_set. { auto 10 with iFrame. } unlock. move=>y /=. ram_apply rule_set. { auto 10 with iFrame. }
Qed. 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) := Definition Box (n:int) (p:loc) :=
Hexists (q:loc), (p ~~~> q) \* (q ~~~> n). Hexists (q:loc), (p ~~~> q) \* (q ~~~> n).
...@@ -132,18 +147,20 @@ Arguments Box_unfold : clear implicits. ...@@ -132,18 +147,20 @@ Arguments Box_unfold : clear implicits.
Arguments RO_Box_unfold : clear implicits. Arguments RO_Box_unfold : clear implicits.
Arguments RO_Box_fold : clear implicits. Arguments RO_Box_fold : clear implicits.
(*---*)
(* ---------------------------------------------------------------------- *)
(** Get operation *)
(*
let get p =
! (!p)
*)
Definition val_box_get := Definition val_box_get :=
ValFun 'p := ValFun 'p :=
Let 'q := val_get 'p in Let 'q := val_get 'p in
val_get 'q. 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, Lemma rule_box_get : forall p n,
triple (val_box_get p) triple (val_box_get p)
PRE (RO (p ~> Box n)) PRE (RO (p ~> Box n))
...@@ -154,22 +171,17 @@ Proof using. ...@@ -154,22 +171,17 @@ Proof using.
ram_apply rule_get_ro. auto with iFrame. ram_apply rule_get_ro. auto with iFrame.
Qed. 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 let up2 f p =
q := f !q + f !q let q = !p in
q := f !q + f !q
*) *)
Definition val_box_twice := Definition val_box_up2 :=
ValFun 'f 'p := ValFun 'f 'p :=
Let 'q := val_get 'p in Let 'q := val_get 'p in
Let 'n1 := val_get 'q in Let 'n1 := val_get 'q in
...@@ -179,54 +191,11 @@ Definition val_box_twice := ...@@ -179,54 +191,11 @@ Definition val_box_twice :=
Let 'm := 'a1 '+ 'a2 in Let 'm := 'a1 '+ 'a2 in
val_set 'q 'm. val_set 'q 'm.
(* to move to LamdaSepRo, next to rule_fix *) Lemma rule_box_up2 : forall (F:int->int) n (f:val) p,
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,
(forall (x:int), triple (f x) (forall (x:int), triple (f x)
PRE (RO(p ~> Box n)) PRE (RO(p ~> Box n))
POST (fun r => \[r = val_int (F x)])) -> POST (fun r => \[r = val_int (F x)])) ->
triple (val_box_twice f p) triple (val_box_up2 f p)
PRE (p ~> Box n) PRE (p ~> Box n)
POST (fun r => \[r = val_unit] \* p ~> Box (2 * F n)). POST (fun r => \[r = val_unit] \* p ~> Box (2 * F n)).
Proof using. Proof using.
...@@ -244,11 +213,15 @@ Proof using. ...@@ -244,11 +213,15 @@ Proof using.
unlock. xpull => /= a2 ->. unlock. xpull => /= a2 ->.
xletapp rule_add => ? ->. xletapp rule_add => ? ->.
ram_apply rule_set. ram_apply rule_set.
iIntros "Hp $ !> % -> Hq". iSplitR; [done|]. iApply Box_fold. iFrame. iIntros "Hp $ !>!> % -> Hq". iSplitR; [done|]. iApply Box_fold. iFrame.
by math_rewrite (2 * F n = F n + F n)%Z. by math_rewrite (2 * F n = F n + F n)%Z.
Qed. Qed.
Arguments rule_box_twice : clear implicits. Arguments rule_box_up2 : clear implicits.
(* ---------------------------------------------------------------------- *)
(** Box demo program *)
Definition val_box_demo := Definition val_box_demo :=
ValFun 'n := ValFun 'n :=
...@@ -257,32 +230,9 @@ Definition val_box_demo := ...@@ -257,32 +230,9 @@ Definition val_box_demo :=
LetFun 'f 'x := LetFun 'f 'x :=
Let 'a := val_box_get 'p in Let 'a := val_box_get 'p in
'x '+ 'a in 'x '+ 'a in
Let 'u := val_box_twice 'f 'p in Let 'u := val_box_up2 'f 'p in
val_box_get 'p. 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), Lemma rule_box_demo : forall (n:int),
triple (val_box_demo n) triple (val_box_demo n)
PRE \[] PRE \[]
...@@ -292,8 +242,8 @@ Proof using. ...@@ -292,8 +242,8 @@ Proof using.
xletapp rule_ref => ? q ->. xletapp rule_ref => ? q ->.
xletapp rule_ref => ? p ->. xletapp rule_ref => ? p ->.
xletfun => F HF. 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 ->. { intros. xdef. xletapp rule_box_get => m ->.
ram_apply rule_add. { iIntros "?". ram_apply rule_add. { iIntros "?".
iSplitR. iModIntro. auto. auto with iFrame. } } (* TODO : improve. *) iSplitR. iModIntro. auto. auto with iFrame. } } (* TODO : improve. *)
...@@ -301,6 +251,6 @@ iSplitR. iModIntro. auto. auto with iFrame. } } (* TODO : improve. *) ...@@ -301,6 +251,6 @@ iSplitR. iModIntro. auto. auto with iFrame. } } (* TODO : improve. *)
auto with iFrame. } auto with iFrame. }
unlock. xpull=> u /= _. apply rule_htop_post. ram_apply rule_box_get. unlock. xpull=> u /= _. apply rule_htop_post. ram_apply rule_box_get.
math_rewrite (2 * (n + n) = 4 * n)%Z. math_rewrite (2 * (n + n) = 4 * n)%Z.
iIntros "$". auto 10 with iFrame. (* TODO: improve. *) iIntros "$ !>". auto 10 with iFrame. (* TODO: improve. *)
Qed. Qed.
...@@ -14,12 +14,6 @@ Set Implicit Arguments. ...@@ -14,12 +14,6 @@ Set Implicit Arguments.
From TLC Require Import LibCore. 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) *) (** * Maps (partial functions) *)
...@@ -494,7 +488,7 @@ Lemma fmap_agree_union_l_inv : forall f1 f2 f3, ...@@ -494,7 +488,7 @@ Lemma fmap_agree_union_l_inv : forall f1 f2 f3,
fmap_agree f1 f3 fmap_agree f1 f3
/\ fmap_agree f2 f3. /\ fmap_agree f2 f3.
Proof using. Proof using.
(* TODO: proofs redundant with others above *) (* LATER: proofs redundant with others above *)
introv M2 M1. split. introv M2 M1. split.
{ intros l v1 v2 E1 E2. { intros l v1 v2 E1 E2.
specializes M1 l v1 v2 E1. applys~ M2 l v1 v2. specializes M1 l v1 v2 E1. applys~ M2 l v1 v2.
...@@ -829,7 +823,7 @@ Proof using. ...@@ -829,7 +823,7 @@ Proof using.
unfold fmap_disjoint, map_disjoint. simpl. unfold fmap_disjoint, map_disjoint. simpl.
lets (l&F): (loc_fresh_nat (null::L)). lets (l&F): (loc_fresh_nat (null::L)).
exists l. split. 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. { subst. right. applys not_not_inv. intros H. applys F.
constructor. applys~ M. } } constructor. applys~ M. } }
{ intro_subst. applys~ F. } { intro_subst. applys~ F. }
...@@ -847,7 +841,7 @@ Proof using. ...@@ -847,7 +841,7 @@ Proof using.
{ rewrite fmap_conseq_succ. { rewrite fmap_conseq_succ.
destruct (IHk (S l)%nat) as [E|?]. destruct (IHk (S l)%nat) as [E|?].
{ intros i N. applys F (S i). applys_eq N 2. math. } { 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. { subst. right. applys not_not_inv. intros H. applys F 0%nat.
constructor. math_rewrite (l'+0 = l')%nat. applys~ M. } } constructor. math_rewrite (l'+0 = l')%nat. applys~ M. } }
{ auto. } } } { auto. } } }
......
...@@ -50,14 +50,6 @@ Definition cf_seq (F1 F2:formula) : formula := fun H Q => ...@@ -50,14 +50,6 @@ Definition cf_seq (F1 F2:formula) : formula := fun H Q =>
F1 H (fun r => \[r = val_unit] \* H1) F1 H (fun r => \[r = val_unit] \* H1)
/\ F2 H1 Q. /\ 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 => Definition cf_let (F1:formula) (F2of:val->formula) : formula := fun H Q =>
exists Q1, exists Q1,
F1 H Q1 F1 H Q1
...@@ -85,6 +77,14 @@ Definition cf_for (v1 v2:val) (F3:int->formula) : formula := fun H Q => ...@@ -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') -> (forall i H' Q', F i H' Q' -> S i H' Q') ->
S n1 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 *) (* ** Definition of the CF generator *)
...@@ -384,12 +384,12 @@ Ltac xcf_trm n ::= ...@@ -384,12 +384,12 @@ Ltac xcf_trm n ::=
Ltac xcf_basic_fun n f' ::= Ltac xcf_basic_fun n f' ::=
let f := xcf_get_fun tt in let f := xcf_get_fun tt in
match f with 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; applys triple_apps_funs_of_cf_iter n;
[ reflexivity | reflexivity | xcf_post tt ] [ reflexivity | reflexivity | xcf_post tt ]
| val_fixs _ _ _ => | val_fixs _ _ _ =>
applys triple_apps_fixs_of_cf_iter n f'; 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 *)
| reflexivity | reflexivity
| xcf_post tt ] | xcf_post tt ]
...@@ -474,7 +474,7 @@ Ltac xapp_xapply E cont_post := ...@@ -474,7 +474,7 @@ Ltac xapp_xapply E cont_post :=
match goal with match goal with
| |- ?F ?H ?Q => is_evar Q; xapplys E | |- ?F ?H ?Q => is_evar Q; xapplys E
| |- ?F ?H (fun r => \[r = val_unit] \* ?H') => is_evar H'; 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) | _ => xapply_core E ltac:(fun tt => hcancel) ltac:(cont_post)
end. end.
...@@ -508,7 +508,7 @@ Ltac xapp_basic E cont_post tt ::= ...@@ -508,7 +508,7 @@ Ltac xapp_basic E cont_post tt ::=
xapp_with_args E ltac:(fun H => xapp_with_args E ltac:(fun H =>
xapp_xapply H cont_post). 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. ...@@ -280,22 +280,6 @@ Proof using. intros. applys* Sound_for_Cf. Qed.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(* ** Notation for characteristic Formulae *) (* ** 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'" := Notation "'`Fail'" :=
(Local (Cf_fail)) (Local (Cf_fail))
(at level 69) : charac. (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 := Definition is_extractible F :=
forall A (J:A->hprop) Q, forall A (J:A->hprop) Q,
......
...@@ -145,7 +145,7 @@ Inductive red : state -> trm -> state -> val -> Prop := ...@@ -145,7 +145,7 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m2 (subst x v1 t2) m3 r -> red m2 (subst x v1 t2) m3 r ->
red m1 (trm_let x t1 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, | 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 m1 t1 m2 v1 ->
red m2 t2 m3 v2 -> red m2 t2 m3 v2 ->
red m3 (trm_app v1 v2) m4 r -> red m3 (trm_app v1 v2) m4 r ->
...@@ -190,7 +190,7 @@ Inductive red : state -> trm -> state -> val -> Prop := ...@@ -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_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit) m2 r ->
red m1 (trm_while t1 t2) 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, | 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 m1 t1 m2 v1 ->
red m2 t2 m3 v2 -> red m2 t2 m3 v2 ->
red m3 (trm_for x v1 v2 t3) m4 r -> red m3 (trm_for x v1 v2 t3) m4 r ->
...@@ -593,8 +593,7 @@ Tactic Notation "rew_vals_to_trms" := ...@@ -593,8 +593,7 @@ Tactic Notation "rew_vals_to_trms" :=
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** Distinct variables *) (** Distinct variables *)
(* TODO: use LibListExec *) (* LATER: use LibListExec and generalize to lists *)
(* TODO: generalize to lists *)
Fixpoint var_fresh (y:var) (xs:vars) : bool := Fixpoint var_fresh (y:var) (xs:vars) : bool :=
match xs with match xs with
...@@ -625,7 +624,7 @@ Proof using. ...@@ -625,7 +624,7 @@ Proof using.
introv N. induction t; simpl; try solve [ fequals; introv N. induction t; simpl; try solve [ fequals;
repeat case_if; simpl; repeat case_if; auto ]. repeat case_if; simpl; repeat case_if; auto ].
repeat case_if; simpl; repeat case_if~. repeat case_if; simpl; repeat case_if~.
Qed. (* TODO: simplify *) Qed. (* LATER: simplify *)
Lemma subst_substs : forall x v ys ws t, Lemma subst_substs : forall x v ys ws t,
var_fresh x ys -> var_fresh x ys ->
...@@ -681,11 +680,12 @@ Definition var_funs (n:nat) (xs:vars) : Prop := ...@@ -681,11 +680,12 @@ Definition var_funs (n:nat) (xs:vars) : Prop :=
/\ length xs = n /\ length xs = n
/\ xs <> nil. /\ 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) nat_compare n (List.length xs)
&& is_not_nil xs (* --todo: rename to exec *) && is_not_nil xs
&& var_distinct xs. && var_distinct xs.
Lemma var_funs_exec_eq : forall n xs, Lemma var_funs_exec_eq : forall n xs,
...@@ -703,9 +703,9 @@ Definition var_fixs (f:var) (n:nat) (xs:vars) : Prop := ...@@ -703,9 +703,9 @@ Definition var_fixs (f:var) (n:nat) (xs:vars) : Prop :=
/\ length xs = n /\ length xs = n
/\ xs <> nil. /\ 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) nat_compare n (List.length xs)
&& is_not_nil xs (* todo: rename to exec *) && is_not_nil xs
&& var_distinct (f::xs). && var_distinct (f::xs).
Lemma var_fixs_exec_eq : forall f n xs, Lemma var_fixs_exec_eq : forall f n xs,
......
...@@ -126,8 +126,6 @@ Open Scope heap_scope. ...@@ -126,8 +126,6 @@ Open Scope heap_scope.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(* ** Tactic for automation *) (* ** Tactic for automation *)
(* TODO: check how much is really useful *)
Hint Extern 1 (_ = _ :> heap) => fmap_eq. Hint Extern 1 (_ = _ :> heap) => fmap_eq.
Tactic Notation "fmap_disjoint_pre" := Tactic Notation "fmap_disjoint_pre" :=
...@@ -419,7 +417,7 @@ Qed. ...@@ -419,7 +417,7 @@ Qed.
(** Tactic for helping reasoning about concrete calls to [alloc] *) (** 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 match goal with
| |- context [ abs 0 ] => change (abs 0) with 0%nat | |- context [ abs 0 ] => change (abs 0) with 0%nat
| |- context [ abs 1 ] => change (abs 1) with 1%nat | |- context [ abs 1 ] => change (abs 1) with 1%nat
...@@ -589,7 +587,7 @@ Proof using. ...@@ -589,7 +587,7 @@ Proof using.
asserts Z: ((\[False] \* \Top \* HF) h1'). asserts Z: ((\[False] \* \Top \* HF) h1').
{ applys himpl_trans K1. hchange M3. hsimpl. hsimpl. } { applys himpl_trans K1. hchange M3. hsimpl. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.