Commit 76c7149d authored by charguer's avatar charguer

fun2

parent a8dedefc
......@@ -261,7 +261,7 @@ Proof using.
introv N. intros x. simpls. do 2 case_if; auto.
Qed.
Lemma fmap_single_single_same_inv : forall (x:A) (v1 v2:B),
Lemma fmap_disjoint_single_single_same_inv : forall (x:A) (v1 v2:B),
\# (fmap_single x v1) (fmap_single x v2) ->
False.
Proof using.
......
......@@ -52,7 +52,7 @@ Fixpoint trm_size (t:trm) : nat :=
Lemma trm_size_subst : forall t x v,
trm_size (subst x v t) = trm_size t.
Proof using.
intros t. induction t; intros; simpl; repeat case_if; auto.
intros. induction t; (try destruct r); simpl; repeat case_if; auto.
Qed.
(** Hint for induction on size. Proves subgoals of the form
......
......@@ -14,6 +14,8 @@ Set Implicit Arguments.
Require Export LibFix LambdaSepCredits. (* MODIFIED FOR CREDITS *)
Open Scope heap_scope.
Implicit Types v w : val.
(* ********************************************************************** *)
(* * Type of a formula *)
......@@ -70,22 +72,22 @@ Hint Resolve is_local_local.
Inductive Trm : Type :=
| Trm_val : val -> Trm
| Trm_if : val -> Trm -> Trm -> Trm
| Trm_if_val : val -> Trm -> Trm -> Trm
| Trm_let : var -> Trm -> Trm -> Trm
| Trm_let_fix : var -> var -> Trm -> Trm -> Trm
| Trm_app : val -> val -> Trm.
(** Definition of capture-avoiding substitution on [Trm] *)
Fixpoint subst_Trm (y : var) (w : val) (t : Trm) : Trm :=
Fixpoint Subst (y : var) (w : val) (t : Trm) : Trm :=
match t with
| Trm_val v => Trm_val (subst_val y w v)
| Trm_if v t1 t2 => Trm_if (subst_val y w v) (subst_Trm y w t1) (subst_Trm y w t2)
| Trm_let x t1 t2 => Trm_let x (subst_Trm y w t1) (If x = y then t2 else subst_Trm y w t2)
| Trm_val v => Trm_val v
| Trm_if_val v t1 t2 => Trm_if_val v (Subst y w t1) (Subst y w t2)
| Trm_let x t1 t2 => Trm_let x (Subst y w t1) (If x = y then t2 else Subst y w t2)
| Trm_let_fix f x t1 t2 => Trm_let_fix f x
(If (x = y \/ f = y) then t1 else subst_Trm y w t1)
(If f = y then t2 else subst_Trm y w t2)
| Trm_app v1 v2 => Trm_app (subst_val y w v1) (subst_val y w v2)
(if eq_var_dec x y then t1 else if eq_var_dec f y then t1 else Subst y w t1)
(if eq_var_dec f y then t2 else Subst y w t2)
| Trm_app v1 v2 => Trm_app v1 v2
end.
(** Translation from [Trm] to [trm], by encoding [Trm_let_fix]
......@@ -95,9 +97,9 @@ Fixpoint trm_of_Trm (t : Trm) : trm :=
let aux := trm_of_Trm in
match t with
| Trm_val v => trm_val v
| Trm_if v t1 t2 => trm_if v (aux t1) (aux t2)
| Trm_if_val v t1 t2 => trm_if v (aux t1) (aux t2)
| Trm_let x t1 t2 => trm_let x (aux t1) (aux t2)
| Trm_let_fix f x t1 t2 => trm_let f (trm_val (val_fix f x (aux t1))) (aux t2)
| Trm_let_fix f x t1 t2 => trm_let f (trm_fix f x (aux t1)) (aux t2)
| Trm_app v1 v2 => trm_app v1 v2
end.
......@@ -112,14 +114,14 @@ Coercion trm_of_Trm : Trm >-> trm.
Fixpoint Trm_size (t:Trm) : nat :=
match t with
| Trm_val v => 1
| Trm_if v t1 t2 => 1 + Trm_size t1 + Trm_size t2
| Trm_if_val v t1 t2 => 1 + Trm_size t1 + Trm_size t2
| Trm_let x t1 t2 => 1 + Trm_size t1 + Trm_size t2
| Trm_let_fix f x t1 t2 => 1 + Trm_size t1 + Trm_size t2
| Trm_app f v => 1
end.
Lemma Trm_size_subst : forall x v t,
Trm_size (subst_Trm x v t) = Trm_size t.
Trm_size (Subst x v t) = Trm_size t.
Proof using.
intros. induction t; simpl; repeat case_if; auto.
Qed.
......@@ -128,11 +130,11 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* ** Definition of the [app] predicate *)
(** The proposition [app f v H Q] asserts that the application
(** The proposition [app (f v) H Q] asserts that the application
of [f] to [v] has [H] as pre-condition and [Q] as post-condition. *)
Definition app f v H Q :=
triple (trm_app f v) H Q.
Definition app t H Q :=
triple t H Q.
(* ---------------------------------------------------------------------- *)
......@@ -141,29 +143,29 @@ Definition app f v H Q :=
(** These auxiliary definitions give the characteristic formula
associated with each term construct. *)
Definition cf_val v : formula := fun H Q =>
Definition cf_val (v:val) : formula := fun H Q =>
H ==> Q v.
Definition cf_if v (F1 F2 : formula) : formula := fun H Q =>
Definition cf_if_val (v:val) (F1 F2:formula) : formula := fun H Q =>
If (v = val_int 0) then F2 H Q else F1 H Q.
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,
F1 H Q1
/\ (forall (X:val), (F2of X) (Q1 X) Q).
Definition cf_app f v : formula := fun H Q =>
app f v H Q.
Definition cf_app (f:val) (v:val) : formula := fun H Q =>
app (f v) H Q.
(* MODIFIED FOR CREDITS *)
Definition Tick (F:formula) := fun H Q =>
exists H', pay_one H H' /\ F H' Q.
(* MODIFIED FOR CREDITS *)
Definition cf_fix (F1of : val -> val -> formula)
(F2of : val -> formula) : formula := fun H Q =>
Definition cf_fix (F1of:val->val->formula)
(F2of:val->formula) : formula := fun H Q =>
forall (F:val),
(forall X, (Tick (F1of F X)) ===> app F X) ->
(forall X, (Tick (F1of F X)) ===> app (F X)) ->
(F2of F) H Q.
......@@ -171,15 +173,15 @@ Definition cf_fix (F1of : val -> val -> formula)
(* ** Instance of [app] for primitive operations *)
Lemma app_ref : forall v,
app prim_ref v \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
app (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using. applys rule_ref. Qed.
Lemma app_get : forall v l,
app prim_get (val_loc l) (l ~~> v) (fun x => \[x = v] \* (l ~~> v)).
app (prim_get (val_loc l)) (l ~~> v) (fun x => \[x = v] \* (l ~~> v)).
Proof using. applys rule_get. Qed.
Lemma app_set : forall w l v,
app prim_set (val_pair (val_loc l) w) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
app (prim_set (val_loc l) w) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
Proof using. applys rule_set. Qed.
......@@ -194,11 +196,11 @@ Proof using. applys rule_set. Qed.
Definition cf_def cf (t:Trm) :=
match t with
| Trm_val v => local (cf_val v)
| Trm_if v t1 t2 => local (cf_if v (cf t1) (cf t2))
| Trm_let x t1 t2 => local (cf_let (cf t1) (fun X => cf (subst_Trm x X t2)))
| Trm_if_val v t1 t2 => local (cf_if_val v (cf t1) (cf t2))
| Trm_let x t1 t2 => local (cf_let (cf t1) (fun X => cf (Subst x X t2)))
| Trm_let_fix f x t1 t2 => local (cf_fix
(fun F X => cf (subst_Trm f F (subst_Trm x X t1)))
(fun F => cf (subst_Trm f F t2)))
(fun F X => cf (Subst f F (Subst x X t1)))
(fun F => cf (Subst f F t2)))
| Trm_app f v => local (cf_app f v)
end.
......@@ -236,22 +238,21 @@ Hint Extern 1 (measure Trm_size _ _) => hnf; simpl; math.
(** Substitution commutes with the translation from [Trm] to [trm] *)
Lemma subst_trm_of_Trm : forall y w (t:Trm),
subst_trm y w (trm_of_Trm t) = trm_of_Trm (subst_Trm y w t).
subst y w (trm_of_Trm t) = trm_of_Trm (Subst y w t).
Proof using.
intros. induction t; simpl; auto.
{ rewrite IHt1, IHt2. auto. }
{ rewrite IHt1, IHt2. case_if~. }
{ rewrite IHt1, IHt2. do 2 case_if~. }
{ rewrite IHt1, IHt2. do 2 case_if~. }
Qed.
(** The size of a [Trm] is preserved by substitution of
a variable by a value. *)
Lemma Trm_size_subst_Trm_value : forall y (w:val) (t:Trm),
Trm_size (subst_Trm y w t) = Trm_size t.
Lemma Trm_size_subst_value : forall y (w:val) (t:Trm),
Trm_size (Subst y w t) = Trm_size t.
Proof using.
intros. induction t; simpl; auto.
case_if~. do 2 case_if~.
intros. induction t; simpl; auto; repeat case_if; auto.
Qed.
......@@ -273,6 +274,9 @@ Proof using.
rewrite is_local_triple. applys local_weaken_body M. applys SF.
Qed.
Notation "'trm_fix'' f x t1" := (trm_func (Rec f) x t1)
(at level 69, f ident, x ident, t1 at level 0).
Lemma sound_for_cf : forall (t:Trm),
sound_for t (cf t).
Proof using.
......@@ -280,24 +284,25 @@ Proof using.
rewrite cf_unfold. destruct t; simpl;
applys sound_for_local; intros H Q P.
{ applys~ rule_val. }
{ hnf in P. applys rule_if. case_if; applys~ IH. }
{ hnf in P. applys rule_if_val. case_if; applys~ IH. }
{ destruct P as (Q1&P1&P2). applys rule_let Q1.
{ applys~ IH. }
{ intros X. rewrite subst_trm_of_Trm.
applys~ IH. hnf. rewrite~ Trm_size_subst_Trm_value. } }
{ renames v to f, v0 to v. applys rule_let_fix. hnf in P.
applys~ IH. hnf. rewrite~ Trm_size_subst_value. } }
{ renames v to f, v0 to x. applys rule_let_fix. hnf in P.
intros F HF. rewrite subst_trm_of_Trm. applys IH.
{ hnf. rewrite~ Trm_size_subst_Trm_value. }
{ hnf. rewrite~ Trm_size_subst_value. }
{ applys P. intros X H' Q' (Q''&HP&HB). (* MODIFIED FOR CREDITS *)
applys HF HP.
do 2 rewrite subst_trm_of_Trm. applys~ IH.
{ hnf. rewrite Trm_size_subst_Trm_value.
rewrite~ Trm_size_subst_Trm_value. } } }
{ hnf. rewrite Trm_size_subst_value.
rewrite~ Trm_size_subst_value. } } }
{ applys P. }
Qed.
Theorem triple_of_cf : forall t H Q,
cf t H Q -> triple t H Q.
cf t H Q ->
triple t H Q.
Proof using. intros. applys* sound_for_cf. Qed.
......
......@@ -26,122 +26,81 @@ Implicit Type l p q : loc.
(* ********************************************************************** *)
(* * Functions of two arguments *)
(* ---------------------------------------------------------------------- *)
(** Derived terms *)
(** Definitions *)
Definition val_fun2 x1 x2 t :=
val_fun x1 (trm_fun x2 t).
Notation "'Fun' x1 x2 ':=' t" :=
(val_fun2 x1 x2 t)
(trm_fun x1 (trm_fun x2 t))
(at level 69, x1 ident, x2 ident) : trm_scope.
Notation "'VFun' x1 x2 ':=' t" :=
(val_fun x1 (trm_fun x2 t))
(at level 69, x1 ident, x2 ident) : trm_scope.
Definition val_fun2 x1 x2 t :=
val_fun x1 (val_fun x2 t).
(* TODO
Lemma rule_app2 : forall x1 x2 F V1 V2 t1 H Q,
F = (val_fun2 x1 x2 t1) ->
(* var_dummy not in fv(t1) *)
triple (subst x1 V1 (subst x2 V2 t1)) H Q ->
triple (F V1 V2) H Q.
Proof using.
Admitted.
*)
Definition spec_fun2 (x1 x2:var) (t1:trm) (F:val) :=
forall X1 X2, triple (subst x1 X1 (subst x2 X2 t1)) ===> triple (F X1 X2).
Definition val_fun2 x1 x2 t :=
val_fun x1 (trm_fun x2 t).
Lemma subst_cross : forall x1 x2 v1 v2 t,
x1 <> x2 ->
subst x2 v2 (subst x1 v1 t) = subst x1 v1 (subst x2 v2 t).
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.
(* ---------------------------------------------------------------------- *)
(** Reduction *)
Lemma red_app_fun2_val : forall m1 m2 vf v1 v2 x1 x2 t r,
vf = val_fun2 x1 x2 t ->
red m1 (subst x2 v2 (subst x1 v1 t)) m2 r ->
x1 <> x2 ->
red m1 (vf v1 v2) m2 r.
Proof using. Hint Resolve red_val.
introv E M N. subst. unfold val_fun2.
applys red_app_fun. applys red_app_fun. applys red_val. applys red_val.
reflexivity. simpl. case_if. applys red_fun. applys red_val.
reflexivity.
applys M.
Proof using.
Hint Resolve red_val. introv E M N. subst. unfold val_fun2.
applys~ red_app_func.
{ applys* red_app_func. simpl. applys* red_func. }
{ simpl. case_if~. }
Qed.
(* ---------------------------------------------------------------------- *)
(** Rules *)
Definition spec_fun2 (x1 x2:var) (t1:trm) (F:val) :=
forall X1 X2, triple (subst x2 X2 (subst x1 X1 t1)) ===> triple (F X1 X2).
Lemma spec_fun2_val_fun2 : forall x1 x2 t1,
x1 <> x2 ->
spec_fun2 x1 x2 t1 (val_fun2 x1 x2 t1).
Proof using.
intros x1 x2 t1 N X1 X2 H Q M. intros H' h Hf.
rewrite~ subst_cross in M.
forwards (h'&v&R&K): (rm M) Hf.
exists h' v. splits.
{ applys~ red_app_fun2_val. }
{ hhsimpl. }
exists h' v. splits~. { applys~ red_app_fun2_val. }
Qed.
Lemma rule_app_fun2 : forall x1 x2 f F V1 V2 t1 H Q,
F = (val_fun2 x1 x2 t1) ->
x1 <> x2 ->
triple (subst x2 V2 (subst x1 V1 t1)) H Q ->
triple (F V1 V2) H Q.
Proof using. intros. subst. applys* spec_fun2_val_fun2. Qed.
Lemma rule_let_fun2 : forall f x1 x2 t1 t2 H Q,
(forall (F:val), spec_fun2 x1 x2 t1 F -> triple (subst f F t2) H Q) ->
x1 <> x2 ->
triple (trm_let f (trm_fun x1 (trm_fun x2 t1)) t2) H Q.
Proof using.
introv M. applys rule_let (fun F => \[spec_fun2 x1 x2 t1 F] \* H).
{ applys rule_fun. introv HF. hsimpl~. }
introv M N. applys rule_let (fun F => \[spec_fun2 x1 x2 t1 F] \* H).
{ applys rule_func_val. hsimpl. applys~ spec_fun2_val_fun2. }
{ intros F. applys rule_extract_hprop. applys M. }
Qed.
(* ********************************************************************** *)
(* * Extension of the language with records *)
Lemma rule_app_fun : forall x F V t1 H Q,
F = (val_fun x t1) ->
triple (subst var_dummy F (subst x V t1)) H Q ->
triple (trm_app F V) H Q.
Proof using. intros. applys* rule_app. Qed.
Lemma rule_app_fun2 : forall x1 x2 F V1 V2 t1 H Q,
F = (val_fun2 x1 x2 t1) ->
triple (subst var_dummy F (subst x2 V2 (subst x1 V1 t1))) H Q ->
triple (F V1 V2) H Q.
Admitted. (* Proof using. intros. applys* rule_app_fun. Admitted.*)
(*
Definition nat_fold A (f:A->nat->A) (i:A) (n:nat) : A :=
match n with
| O => i
| S n' => f (nat_fold f i n') n'
end.
*)
(*
Definition fields := list field.
*)
(* ********************************************************************** *)
(* * Extension of the language with records *)
(*
Definition star_fields_values l fvs :=
fold_right (fun H fv => let (f,v) := fv in H \* l `.` f ~~> v) \[] fvs.
Definition star_fields l n :=
nat_fold (fun H f => H \* (Hexists v, l `.` f ~> v)) \[] n.
*)
(** Program variables *)
......
(*
EXO
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 H' h Hh.
forwards (h'&v&R&K): (rm M) Hh. exists h' v. splits~.
Qed.
Lemma rule_red : forall t1 t2 H Q,
(forall n m m' r, red n m t1 m' r -> red n m t2 m' r) ->
triple t1 H Q ->
triple t2 H Q.
Proof using.
introv T M. intros H' h Hh.
forwards (n&h'&v&R&K&C): (rm M) Hh. exists n h' v. splits~.
Qed.
*)
(*
Definition fields := list field.
Definition star_fields_values l fvs :=
fold_right (fun H fv => let (f,v) := fv in H \* l `.` f ~~> v) \[] fvs.
Definition star_fields l n :=
nat_fold (fun H f => H \* (Hexists v, l `.` f ~> v)) \[] n.
*)
(* (forall (F:val),
(forall X H' Q',
......@@ -29,6 +66,20 @@ Qed.
Lemma rule_if_val' : forall v t1 t2 H Q,
(v <> val_int 0 -> triple t1 H Q) ->
(v = val_int 0 -> triple t2 H Q) ->
triple (trm_if v t1 t2) H Q.
Proof using.
introv M1 M2. intros h1 h2 D HF. tests E: (v <> val_int 0).
{ forwards* (h'&v'&(N1&N2&N3&N4)): (rm M1) HF.
exists h' v'. splits~. { applys red_if_val; auto_false. } }
{ forwards* (h'&v'&(N1&N2&N3&N4)): (rm M2) h1 HF.
exists h' v'. splits~. { applys red_if_val; auto_false. } }
Qed.
| prim_fst : prim
......@@ -236,5 +287,44 @@ Fixpoint is_app_vals (t:trm) : bool :=
Opaque is_app_vals.
Lemma rule_app : forall f x F V t1 H Q,
F = (val_fix f x t1) ->
triple (subst f F (subst x V t1)) H Q ->
triple (trm_app F V) H Q.
Proof using.
introv EF M. subst F. intros h1 h2 D P1.
forwards~ (h1'&v&(N1&N2&N3&N4)): (rm M) h2 (rm P1).
exists h1' v. splits~.
{ applys~ red_app_fix_val. }
Qed.
Lemma rule_let_fix : forall f x t1 t2 H Q,
(forall (F:val),
(forall X H' Q',
triple (subst f F (subst x X t1)) H' Q' ->
triple (trm_app F X) H' Q') ->
triple (subst f F t2) H Q) ->
triple (trm_let f (trm_val (val_fix f x t1)) t2) H Q.
Proof using.
introv M. applys rule_let_val. intros F EF.
applys (rm M). clears H Q. intros X H Q.
applys rule_app. auto.
Qed.
Lemma subst_cross : forall x1 x2 v1 v2 t,
x1 <> x2 ->
subst x2 v2 (subst x1 v1 t) = subst x1 v1 (subst x2 v2 t).
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.
*)
......@@ -244,6 +244,11 @@ End Red.
Section Derived.
Hint Resolve red_val.
Lemma red_if_val : forall m1 m2 v r t1 t2,
red m1 (If v = val_int 0 then t2 else t1) m2 r ->
red m1 (trm_if v t1 t2) m2 r.
Proof using. introv M1. applys~ red_if. Qed.
Lemma red_app_fun_val : forall m1 m2 v1 v2 x t r,
v1 = val_fun x t ->
red m1 (subst x v2 t) m2 r ->
......
......@@ -328,15 +328,6 @@ Proof using.
introv M. applys rule_htop_post. applys~ rule_frame.
Qed.
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 H' h Hh.
forwards (h'&v&R&K): (rm M) Hh. exists h' v. splits~.
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Term rules *)
......@@ -414,7 +405,7 @@ Proof using.
{ intros X. applys rule_extract_hprop. intro_subst. applys M'. }
Qed.
Lemma rule_func : forall fopt x t1 H Q,
Lemma rule_func_val : forall fopt x t1 H Q,
H ==> Q (val_func fopt x t1) ->
triple (trm_func fopt x t1) H Q.
Proof using.
......@@ -433,25 +424,12 @@ Proof using.
exists h' v. splits~. { applys~ red_app_fun_val. }
Qed.
Lemma rule_app_fix : forall f x F V t1 H Q,
F = (val_fix f x t1) ->
triple (subst f F (subst x V t1)) H Q ->
triple (trm_app F V) H Q.
Proof using.
introv EF M. subst F. intros HF h N.
lets~ (h'&v&R&K): (rm M) HF h.
exists h' v. splits~. { applys~ red_app_fix_val. }
Qed.
Definition spec_fun (x:var) (t1:trm) (F:val) :=
forall X, triple (subst x X t1) ===> triple (trm_app F X).
Lemma spec_fun_val_fun : forall x t1,
spec_fun x t1 (val_fun x t1).
Proof using.
intros x t1 X H Q M. applys rule_red (rm M).
introv R. applys~ red_app_fun_val.
Qed.
Proof using. introv. intros X H Q M. applys* rule_app_fun. Qed.
Lemma rule_fun : forall x t1 H Q,
(forall (F:val), spec_fun x t1 F -> H ==> Q F) ->
......@@ -459,7 +437,7 @@ Lemma rule_fun : forall x t1 H Q,
Proof using.
introv M. forwards M': (rm M) (val_fun x t1).
{ applys spec_fun_val_fun. }
{ applys~ rule_func. }
{ applys~ rule_func_val. }
Qed.
Lemma rule_let_fun : forall f x t1 t2 H Q,
......@@ -471,15 +449,22 @@ Proof using.
{ intros F. applys rule_extract_hprop. applys M. }
Qed.
Lemma rule_app_fix : forall f x F V t1 H Q,
F = (val_fix f x t1) ->
triple (subst f F (subst x V t1)) H Q ->
triple (trm_app F V) H Q.
Proof using.
introv EF M. subst F. intros HF h N.
lets~ (h'&v&R&K): (rm M) HF h.
exists h' v. splits~. { applys~ red_app_fix_val. }
Qed.
Definition spec_fix (f:var) (x:var) (t1:trm) (F:val) :=
forall X, triple (subst f F (subst x X t1)) ===> triple (trm_app F X).
Lemma spec_fix_val_fix : forall f x t1,
spec_fix f x t1 (val_fix f x t1).
Proof using.
intros f x t1 X H Q M. applys rule_red (rm M).
introv R. applys~ red_app_fix_val.
Qed.
Proof using. introv. intros X H Q M. applys* rule_app_fix. Qed.
Lemma rule_fix : forall f x t1 H Q,
(forall (F:val), spec_fix f x t1 F -> H ==> Q F) ->
......@@ -487,7 +472,7 @@ Lemma rule_fix : forall f x t1 H Q,
Proof using.
introv M. forwards M': (rm M) (val_fix f x t1).
{ applys spec_fix_val_fix. }
{ applys~ rule_func. }
{ applys~ rule_func_val. }
Qed.
Lemma rule_let_fix : forall f x t1 t2 H Q,
......@@ -619,8 +604,6 @@ Proof using.
Qed.
(* ********************************************************************** *)
(* * Bonus *)
......
......@@ -46,6 +46,8 @@ Implicit Types v : val.
Inductive red : nat -> state -> trm -> state -> val -> Prop :=
| red_val : forall m v,
red 0 m (trm_val v) m v
| red_fix : forall m f x t1,
red 0 m (trm_fix f x t1) m (val_fix f x t1)
| red_if_val : forall n m1 m2 v r t1 t2,
red n m1 (If v = val_int 0 then t2 else t1) m2 r ->
red n m1 (trm_if v t1 t2) m2 r
......@@ -53,9 +55,6 @@ Inductive red : nat -> state -> trm -> state -> val -> Prop :=
red n1 m1 t1 m2 v1 ->
red n2 m2 (subst x v1 t2) m3 r ->
red (n1+n2) m1 (trm_let x t1 t2) m3 r
| red_fix : forall n m1 m2 f x t1 t2 r,
red n m1 (subst f (val_fix f x t1) t2) m2 r ->
red n m1 (trm_fix f x t1 t2) m2 r
| red_app : forall n1 n2 n3 m1 m2 m3 m4 t1 t2 v1 v2 f x t r,
red n1 m1 t1 m2 v1 ->
red n2 m2 t2 m3 v2 ->
......@@ -75,7 +74,7 @@ Inductive red : nat -> state -> trm -> state -> val -> Prop :=
Hint Resolve red_val.
Lemma red_app_val : forall n m1 m2 v1 v2 f x t r,
Lemma red_app_fix_val : forall n m1 m2 v1 v2 f x t r,
v1 = val_fix f x t ->
red n m1 (subst f v1 (subst x v2 t)) m2 r ->
red (n+1) m1 (trm_app v1 v2) m2 r.
......@@ -670,14 +669,26 @@ Proof using.
{ intros X. applys rule_extract_hprop. intro_subst. applys M'. }
Qed.
Lemma rule_app : forall f x F V t1 H H' Q,
F = (val_fix f x t1) ->
pay_one H H' ->
triple (subst f F (subst x V t1)) H' Q ->
triple (trm_app F V) H Q.
Lemma rule_fix_val : forall f x t1 H Q,
H ==> Q (val_fix f x t1) ->
triple (trm_fix f x t1) H Q.
Proof using.
introv M. intros HF h N. exists___. splits.
{ applys red_fix. }
{ hhsimpl. hchanges M. }
{ math. }
Qed.
Definition spec_fix (f:var) (x:var) (t1:trm) (F:val) :=
forall X H H' Q,
pay_one H H' ->
triple (subst f F (subst x X t1)) H' Q ->
triple (trm_app F X) H Q.
Lemma spec_fix_val_fix : forall f x t1,
spec_fix f x t1 (val_fix f x t1).
Proof using.
introv EF HP M. subst F. intros HF h N.
unfolds pay_one.
intros f x t1 X H H' Q HP M. intros HF h N. unfolds pay_one.
lets HP': himpl_frame_l HF (rm HP).
lets N': (rm HP') (rm N). rew_heap in N'.
destruct N' as (h1&h2&N1&N2&N3&N4).
......@@ -685,21 +696,34 @@ Proof using.
lets (Na&Nb): heap_eq_forward (rm N4). simpls. subst.
lets~ (n&h'&v&R&K&C): (rm M) HF h2.
exists (n+1)%nat h' v. splits~.
{ applys* red_app_val. fmap_red~. }