Commit dc6a15e2 authored by charguer's avatar charguer

modelsepok

parent 111fd3e9
......@@ -206,7 +206,7 @@ Inductive red : state -> trm -> state -> val -> Prop :=
| red_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
red ma (trm_new v) (ma \+ mb) (val_loc l)
red ma (trm_new v) (mb \+ ma) (val_loc l)
| red_get : forall ma mb l v,
ma = (state_single l v) ->
\# ma mb ->
......
......@@ -111,64 +111,10 @@ Notation "\GC" := (heap_is_gc) : heap_scope.
Notation "'Hexists' x1 , H" := (heap_is_exists (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 , H" := (Hexists x1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 , H" := (Hexists x1, Hexists x2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 x4 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 x4 x5 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 : T1 , H" := (heap_is_exists (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) , H" := (Hexists x1:T1,H)
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) ( x5 : T5 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, Hexists x5:T5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) x2 , H" :=
(Hexists x1:T1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) x2 x3 , H" :=
(Hexists x1:T1, Hexists x2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) x2 x3 x4 , H" :=
(Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) x2 x3 x4 x5 , H" :=
(Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) x3 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 x5 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 x5 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "r '~~>' v" := (heap_is_single r v)
(at level 32, no associativity) : heap_scope.
......@@ -177,32 +123,15 @@ Notation "Q \*+ H" :=
(fun x => heap_is_star (Q x) H)
(at level 40) : heap_scope.
(*
Notation "# H" := (fun (_:unit) => (H:hprop))
(at level 39, H at level 99) : heap_scope.
*)
(* BONUS
Notation "\[= v ]" := (fun x => \[x = v])
(at level 0) : heap_scope.
Notation "P ==+> Q" := (pred_le P%h (heap_is_star P Q))
(at level 55, only parsing) : heap_scope.
*)
(********************************************************************)
(* ** Triple *)
Definition triple t H Q :=
forall h1 h2, \# h1 h2 -> H h1 ->
exists h1' h3 r,
\# h1' h2 h3
/\ red (h1 \+ h2) t (h1' \+ h2 \+ h3) r
/\ Q r h1'.
Definition app f v H Q :=
triple (trm_app f v) H Q.
(********************************************************************)
(* ** Lemmas on states and heaps *)
......@@ -469,7 +398,6 @@ Tactic Notation "rew_heap" "*" "in" hyp(H) :=
(********************************************************************)
(* ** Rules *)
......@@ -477,8 +405,20 @@ Implicit Types H : hprop.
Implicit Types Q : val -> hprop.
(** Triples *)
(** Structural *)
Definition triple t H Q :=
forall h1 h2, \# h1 h2 -> H h1 ->
exists h1' h3 r,
\# h1' h2 h3
/\ 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) ->
......@@ -515,9 +455,7 @@ Proof using.
{ exists h1'a h1b. splits~. rew_disjoint. jauto. } }
Qed.
(* TODO: add to hint extern "rew_disjoint" the jauto_set. *)
(** Terms *)
(** Term rules *)
Lemma rule_val : forall v H Q,
H ==> Q v ->
......@@ -590,28 +528,59 @@ Proof using.
Qed.
Lemma rule_new : forall v,
triple (trm_new v) \[] (fun r => Hexists l, [r = val_loc l] \* l ~~> v).
triple (trm_new v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
skip.
Transparent heap_is_single.
introv D H1. unfolds heap_is_single.
hnf in H1. subst h1. rewrite state_union_neutral_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.
{ rew_disjoint. splits; jauto. }
{ applys~ red_new. }
{ exists l heap_empty (state_single l v). splits~. }
Qed.
Lemma rule_get : forall l,
Lemma rule_get : forall v l,
triple (trm_get (val_loc l)) (l ~~> v) (fun x => \[x = v] \* l ~~> v).
Proof using.
skip.
Transparent heap_is_single.
introv D H1. unfolds heap_is_single.
exists h1 heap_empty v. rewrite state_union_neutral_r.
splits.
{ rew_disjoint. jauto. }
{ applys~ red_get. }
{ exists heap_empty h1. splits~. }
Qed.
Lemma rule_set : forall l v w,
triple (trm_set (val_loc l) w) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
Proof using.
skip.
Transparent heap_is_single.
introv D H1. unfolds heap_is_single.
exists (state_single l w) heap_empty val_unit.
rewrite state_union_neutral_r.
splits.
{ rew_disjoint. splits; jauto. subst h1.
unfolds heap_disjoint, state_disjoint, pfun_disjoint, state_single. simpls.
intros x. specializes D x. case_if; intuition auto_false. }
{ applys~ red_set v. }
{ exists heap_empty (state_single l w). splits~. }
Qed.
End Red.
(* TODO: add to hint extern "rew_disjoint" the jauto_set. *)
(********************************************************************)
(* ** More *)
......
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