Commit 3516e6d9 authored by charguer's avatar charguer

simplify

parent cd52b5bc
Definition app f v H Q :=
triple (trm_app f v) H Q.
Lemma rule_app : forall f v H Q,
app f v H Q ->
triple (trm_app f v) H Q.
Proof using.
auto.
Qed.
(*
| red_fix : forall m1 m2 f x t1 t2 r,
red m1 (subst_trm f (val_fix f x t1) t2) m2 r ->
red m1 (trm_fix f x t1 t2) m2 r
*)
(********************************************************************)
(* ** More *)
......
......@@ -27,7 +27,6 @@ with trm : Type :=
| trm_if : val -> trm -> trm -> trm
| trm_let : var -> trm -> trm -> trm
| trm_app : val -> val -> trm
| trm_fix : var -> var -> trm -> trm -> trm
| trm_new : val -> trm
| trm_get : val -> trm
| trm_set : val -> val -> trm.
......@@ -38,7 +37,8 @@ with trm : Type :=
Fixpoint subst_val (y : var) (w : val) (v : val) : val :=
match v with
| val_var x => If x = y then w else v
| _ => v (* note that closures have no free variables *)
| val_fix f x t => If (x = y \/ f = y) then v else val_fix f x (subst_trm y w t)
| _ => v
end
with subst_trm (y : var) (w : val) (t : trm) : trm :=
......@@ -47,10 +47,6 @@ with subst_trm (y : var) (w : val) (t : trm) : trm :=
| 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_app v1 v2 => trm_app (subst_val y w v1) (subst_val y w v2)
| trm_fix f x t1 t2 =>
trm_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_new v => trm_new (subst_val y w v)
| trm_get v => trm_get (subst_val y w v)
| trm_set v1 v2 => trm_set (subst_val y w v1) (subst_val y w v2)
......@@ -191,9 +187,6 @@ Inductive red : state -> trm -> state -> val -> Prop :=
v1 = val_fix f x t ->
red m1 (subst_trm f v1 (subst_trm x v2 t)) m2 r ->
red m1 (trm_app v1 v2) m2 r
| red_fix : forall m1 m2 f x t1 t2 r,
red m1 (subst_trm f (val_fix f x t1) t2) m2 r ->
red m1 (trm_fix f x t1 t2) m2 r
| red_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
......@@ -211,6 +204,7 @@ Inductive red : state -> trm -> state -> val -> Prop :=
End Red.
(*------------------------------------------------------------------*)
(** Big-step evaluation with counting of the number of beta reductions
(used by the formalization of Separation Logic with time credits) *)
......@@ -233,9 +227,6 @@ Inductive redn : nat -> state -> trm -> state -> val -> Prop :=
v1 = val_fix f x t ->
redn n m1 (subst_trm f v1 (subst_trm x v2 t)) m2 r ->
redn (S n) m1 (trm_app v1 v2) m2 r
| redn_fix : forall n m1 m2 f x t1 t2 r,
redn n m1 (subst_trm f (val_fix f x t1) t2) m2 r ->
redn n m1 (trm_fix f x t1 t2) m2 r
| redn_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
......@@ -253,6 +244,7 @@ Inductive redn : nat -> state -> trm -> state -> val -> Prop :=
End Redn.
Local Open Scope state_scope.
......
......@@ -321,7 +321,18 @@ Lemma himpl_extract_prop : forall (P:Prop) H H',
(P -> H ==> H') -> (\[P] \* H) ==> H'.
Proof using. introv W Hh. lets (?&?): hprop_star_prop_elim Hh. applys* W. Qed.
Lemma himpl_extract_exists : forall A (x:A) H J,
Lemma himpl_extract_exists : forall A H (J:A->hprop),
(forall x, J x ==> H) -> (hprop_exists J) ==> H.
Proof using. introv W. intros h (x&Hh). applys* W. Qed.
Lemma himpl_inst_prop : forall (P:Prop) H H',
P -> H ==> H' -> H ==> (\[P] \* H').
Proof using.
introv HP W. intros h Hh. exists heap_empty h.
splits*. applys* hprop_empty_st_prove.
Qed.
Lemma himpl_inst_exists : forall A (x:A) H J,
(H ==> J x) -> H ==> (hprop_exists J).
Proof using. introv W h. exists x. apply~ W. Qed.
......@@ -355,19 +366,15 @@ Definition triple t H Q :=
/\ red (h1 \+ h2) t (h1' \+ h2 \+ h3) r
/\ Q r h1'.
Definition app f v H Q :=
triple (trm_app f v) H Q.
(** Structural rules *)
Lemma rule_extract_prop : forall t (P:Prop) H Q,
(P -> triple t H Q) ->
triple t (H \* \[P]) Q.
triple t (\[P] \* H) Q.
Proof using.
introv M D (h21&h22&N1&(HE&HP)&N3&N4).
subst h22 h1. rewrite heap_union_empty_r.
forwards (h1'&h3&r&R1&R2&R3): M HP h2 N1.
introv M D (h21&h22&(HE&HP)&N2&N3&N4).
subst h21 h1. rewrite heap_union_empty_l.
forwards (h1'&h3&r&R1&R2&R3): M HP h2 N2.
{ substs. rew_disjoint*. }
exists~ h1' h3 r.
Qed.
......@@ -477,14 +484,16 @@ Proof using.
{ auto. } }
Qed.
Lemma rule_app : forall f v H Q,
app f v H Q ->
triple (trm_app f v) H Q.
Proof using.
auto.
Lemma rule_let_val : forall x v1 t2 H Q,
(forall (X:val), X = v1 -> triple (subst_trm x X t2) H Q) ->
triple (trm_let x (trm_val v1) t2) H Q.
Proof using.
introv M. applys rule_let (fun x => \[x = v1] \* H).
{ applys rule_val. applys~ himpl_inst_prop. }
{ intros X. applys rule_extract_prop. applys M. }
Qed.
Lemma rule_val_fix : forall f x F V t1 H Q,
Lemma rule_app : forall f x F V t1 H Q,
F = (val_fix f x t1) ->
triple (subst_trm f F (subst_trm x V t1)) H Q ->
triple (trm_app F V) H Q.
......@@ -497,22 +506,17 @@ Proof using.
{ auto. }
Qed.
Lemma rule_fix : forall f x t1 t2 H Q,
Lemma rule_let_fix : forall f x t1 t2 H Q,
(forall (F:val),
(forall X H' Q',
triple (subst_trm f F (subst_trm x X t1)) H' Q' ->
app F X H' Q') ->
triple (trm_app F X) H' Q') ->
triple (subst_trm f F t2) H Q) ->
triple (trm_fix f x t1 t2) H Q.
triple (trm_let f (trm_val (val_fix f x t1)) t2) H Q.
Proof using.
introv M D H1.
forwards (h1'&h3&r&R1&R2&R3): M (val_fix f x t1) D H1.
{ clears h1 h2 H Q. intros X H Q M. unfolds.
applys~ rule_val_fix M. }
exists h1' h3 r. splits.
{ rew_disjoint*. }
{ applys~ red_fix. }
{ auto. }
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 rule_new : forall v,
......
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