Commit 1617a008 authored by charguer's avatar charguer

proof_credits

parent 1c04997b
......@@ -12,7 +12,9 @@ include $(CFML)/Makefile.common
SRC :=\
ModelLambda \
ModelSep \
ModelRO
ModelCredits
# ModelRO
PWD := $(shell pwd)
V_AUX := $(wildcard $(TLC)/*.v) $(CFML)/lib/coq/Shared.v
......
This diff is collapsed.
......@@ -182,6 +182,9 @@ Notation "h1 \+ h2" := (state_union h1 h2)
(************************************************************)
(* * Source language semantics *)
(*------------------------------------------------------------------*)
(** Big-step evaluation *)
Section Red.
Local Open Scope state_scope.
......@@ -220,10 +223,50 @@ Inductive red : state -> trm -> state -> val -> Prop :=
End Red.
(*------------------------------------------------------------------*)
(** Big-step evaluation with counting of the number of beta reductions *)
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_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_letfix f x t1 t2) m2 r
| redn_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
redn 0 ma (trm_new v) (mb \+ ma) (val_loc l)
| redn_get : forall ma mb l v,
ma = (state_single l v) ->
\# ma mb ->
redn 0 (ma \+ mb) (trm_get (val_loc l)) (ma \+ mb) v
| redn_set : forall ma1 ma2 mb l v1 v2,
ma1 = (state_single l v1) ->
ma2 = (state_single l v2) ->
\# ma1 mb ->
redn 0 (ma1 \+ mb) (trm_set (val_loc l) v2) (ma2 \+ mb) val_unit.
End Redn.
Local Open Scope state_scope.
(*------------------------------------------------------------------*)
(* ** Properties on states *)
......@@ -329,14 +372,14 @@ Proof using.
unfold pfun_union. cases~ (f x).
Qed.
Lemma state_union_neutral_l : forall h,
Lemma state_union_empty_l : forall h,
state_union state_empty h = h.
Proof using.
intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
apply~ state_eq.
Qed.
Lemma state_union_neutral_r : forall h,
Lemma state_union_empty_r : forall h,
state_union h state_empty = h.
Proof using.
intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
......@@ -360,7 +403,7 @@ Qed.
(** Hints and tactics *)
Hint Resolve state_union_neutral_l state_union_neutral_r.
Hint Resolve state_union_empty_l state_union_empty_r.
Hint Rewrite
state_disjoint_union_eq_l
......
......@@ -152,13 +152,13 @@ Proof using. intros. applys~ state_disjoint_union_eq_r. Qed.
(** Union *)
Lemma heap_union_neutral_l : forall h,
Lemma heap_union_empty_l : forall h,
heap_empty \+ h = h.
Proof using. intros. applys~ state_union_neutral_l. Qed.
Proof using. intros. applys~ state_union_empty_l. Qed.
Lemma heap_union_neutral_r : forall h,
Lemma heap_union_empty_r : forall h,
h \+ heap_empty = h.
Proof using. intros. applys~ state_union_neutral_r. Qed.
Proof using. intros. applys~ state_union_empty_r. Qed.
Lemma heap_union_comm : forall h1 h2,
\# h1 h2 ->
......@@ -186,7 +186,7 @@ Proof using. auto. Qed.
Hint Resolve
heap_disjoint_sym
heap_disjoint_empty_l heap_disjoint_empty_r
heap_union_neutral_l heap_union_neutral_r.
heap_union_empty_l heap_union_empty_r.
Hint Rewrite
heap_disjoint_union_eq_l
......@@ -241,7 +241,7 @@ Lemma hprop_star_empty_l : forall H,
Proof using.
intro. unfold hprop, hprop_star. extens. intros h.
iff (h1&h2&M1&M2&D&U) M.
hnf in M1. subst h1 h. rewrite~ heap_union_neutral_l.
hnf in M1. subst h1 h. rewrite~ heap_union_empty_l.
exists heap_empty h. hint hprop_empty_prove. splits~.
Qed.
......@@ -288,7 +288,7 @@ Qed.
Lemma hprop_star_prop_elim : forall (P:Prop) H h,
(\[P] \* H) h -> P /\ H h.
Proof using.
introv (?&?&N&?&?&?). destruct N. subst. rewrite~ heap_union_neutral_l.
introv (?&?&N&?&?&?). destruct N. subst. rewrite~ heap_union_empty_l.
Qed.
Lemma hprop_star_prop_extract_prop : forall (P:Prop) H H',
......@@ -331,7 +331,7 @@ Lemma rule_extract_prop : forall t (P:Prop) H Q,
triple t (H \* \[P]) Q.
Proof using.
introv M D (h21&h22&N1&(HE&HP)&N3&N4).
subst h22 h1. rewrite heap_union_neutral_r.
subst h22 h1. rewrite heap_union_empty_r.
forwards (h1'&h3&r&R1&R2&R3): M HP h2 N1.
{ substs. rew_disjoint*. }
exists~ h1' h3 r.
......@@ -368,7 +368,7 @@ Lemma rule_val : forall v H Q,
triple (trm_val v) H Q.
Proof using.
introv M D H1.
exists h1 heap_empty v. rewrite heap_union_neutral_r.
exists h1 heap_empty v. rewrite heap_union_empty_r.
splits.
{ rew_disjoint*. }
{ applys red_val. }
......@@ -440,14 +440,14 @@ Lemma rule_new : forall v,
Proof using.
Transparent hprop_single.
introv D H1. unfolds hprop_single.
lets: hprop_empty_inv H1. subst h1. rewrite heap_union_neutral_l.
lets: hprop_empty_inv H1. subst h1. rewrite heap_union_empty_l.
asserts (l&Hl): (exists l, (state_data h2) l = None).
{ skip. } (* infinitely many locations -- TODO *)
asserts Fr: (state_disjoint h2 (state_single l v)).
{ unfolds state_disjoint, pfun_disjoint, state_single. simpls.
intros x. case_if~. }
exists (state_single l v) heap_empty (val_loc l).
rewrite state_union_neutral_r. splits.
rewrite heap_union_empty_r. splits.
{ rew_disjoint. splits*. }
{ applys~ red_new. }
{ exists l heap_empty (state_single l v). splits~. }
......@@ -458,7 +458,7 @@ Lemma rule_get : forall v l,
Proof using.
Transparent hprop_single.
introv D H1. unfolds hprop_single.
exists h1 heap_empty v. rewrite heap_union_neutral_r.
exists h1 heap_empty v. rewrite heap_union_empty_r.
splits.
{ rew_disjoint*. }
{ applys~ red_get. }
......@@ -471,7 +471,7 @@ Proof using.
Transparent hprop_single.
introv D H1. unfolds hprop_single.
exists (state_single l w) heap_empty val_unit.
rewrite state_union_neutral_r.
rewrite heap_union_empty_r.
splits.
{ rew_disjoint. splits*. subst h1.
unfolds heap_disjoint, state_disjoint, pfun_disjoint, state_single. simpls.
......
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