Commit ca4e14d8 authored by charguer's avatar charguer

inprogerss

parent 795354c0
......@@ -11,9 +11,12 @@ include $(CFML)/Makefile.common
SRC :=\
ModelLambda \
ModelSep \
ModelCredits \
ModelRO \
ModelSepFunctor \
ModelSepBasic \
ModelSepCredits
OTHER :=\
ModelSepRO \
ModelCF \
ModelCFCredits \
ModelTactics
......
......@@ -68,7 +68,7 @@ with subst_trm (y : var) (w : val) (t : trm) : trm :=
(********************************************************************)
(* ** States *)
(* * States *)
Tactic Notation "cases" constr(E) := (* For TLC *)
let H := fresh "Eq" in cases E as H.
......@@ -258,6 +258,45 @@ End Red.
Local Open Scope state_scope.
(*------------------------------------------------------------------*)
(** Big-step evaluation with counting of the number of beta reductions
(used by the formalization of Separation Logic with time credits) *)
Section Redn.
Local Open Scope nat_scope.
Local Open Scope state_scope.
Inductive redn : nat -> state -> trm -> state -> val -> Prop :=
| redn_val : forall m v,
redn 0 m (trm_val v) m v
| redn_if : forall n m1 m2 v r t1 t2,
redn n m1 (If v = val_int 0 then t2 else t1) m2 r ->
redn n m1 (trm_if v t1 t2) m2 r
| redn_let : forall n1 n2 m1 m2 m3 x t1 t2 v1 r,
redn n1 m1 t1 m2 v1 ->
redn n2 m2 (subst_trm x v1 t2) m3 r ->
redn (n1+n2) m1 (trm_let x t1 t2) m3 r
| redn_app : forall n m1 m2 v1 v2 f x t r,
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_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
redn 0 ma (prim_new v) (mb \+ ma) (val_loc l)
| redn_get : forall m l v,
state_data m l = Some v ->
redn 0 m (prim_get (val_loc l)) m v
| redn_set : forall m m' l v,
m' = state_update m l v ->
redn 0 m (prim_set (val_pair (val_loc l) v)) m' val_unit.
End Redn.
(************************************************************)
(* * Lemmas *)
(*------------------------------------------------------------------*)
(* ** Equality of states *)
......@@ -580,7 +619,7 @@ Qed.
(************************************************************)
(** * Tactics *)
(* * Tactics *)
(*------------------------------------------------------------------*)
(* ** Proving disjointness results *)
......@@ -622,7 +661,7 @@ Qed.
(*------------------------------------------------------------------*)
(* ** Proving equality of states *)
(* ** Tactic [state_eq] for proving equality of states *)
(** [state_eq] proves equalities between unions of states.
It attempts to discharge the disjointness side-conditions.
......@@ -744,7 +783,9 @@ Proof using.
{ state_eq. }
Qed.
(*------------------------------------------------------------------*)
(* ** Tactic [state_red] for proving [red] goals modulo
equalities between states *)
(** [state_red] proves a goal of the form [red h1 t h2 v]
using an hypothesis of the shape [red h1' t h2' v],
......
This diff is collapsed.
This diff is collapsed.
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