Commit 1950967d authored by charguer's avatar charguer
Browse files

proof_ro

parent bfa89ad9
......@@ -99,6 +99,13 @@ Definition pfun_union (A B : Type) (f1 f2 : pfun A B) :=
| None => f2 x
end.
Definition pfun_compatible (A B : Type) (f1 f2 : pfun A B) :=
forall x v1 v2,
f1 x = Some v1 ->
f2 x = Some v2 ->
v1 = v2.
(*------------------------------------------------------------------*)
(** Representation of state *)
......@@ -120,6 +127,11 @@ Definition state_disjoint (h1 h2 : state) : Prop :=
Definition state_disjoint_3 h1 h2 h3 :=
state_disjoint h1 h2 /\ state_disjoint h2 h3 /\ state_disjoint h1 h3.
(** Compatible states *)
Definition state_compatible (g1 g2 : state) :=
pfun_compatible g1 g2.
(** Finiteness of union *)
Lemma pfun_union_finite : forall (A B : Type) (f1 f2 : pfun A B),
......@@ -296,8 +308,21 @@ Lemma state_disjoint_3_unfold : forall h1 h2 h3,
\# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
Proof using. auto. Qed.
(** Compatibility *)
Lemma state_compatible_refl : refl state_compatible.
Proof using.
intros h. introv M1 M2. congruence.
Qed.
(** Union *)
Lemma state_union_idempotent : idempotent2 state_union.
Proof using.
intros [f F]. apply~ state_eq. simpl. intros x.
unfold pfun_union. cases~ (f x).
Qed.
Lemma state_union_neutral_l : forall h,
state_union state_empty h = h.
Proof using.
......
......@@ -57,17 +57,6 @@ Definition heap_empty : heap :=
(* (state_empty, 0%nat). *)
*)
Definition pfun_compatible (A B : Type) (f1 f2 : pfun A B) :=
forall x v1 v2,
f1 x = Some v1 ->
f2 x = Some v2 ->
v1 = v2.
Definition state_compatible (g1 g2 : state) :=
pfun_compatible g1 g2.
(* forall k \in (dom g1 \n dom g2), g1[k] = g2[k]. *)
(*------------------------------------------------------------------*)
(* ** Definition of heap predicates *)
......@@ -86,18 +75,15 @@ Definition heap_is_empty : hprop :=
Definition heap_is_single (l:loc) (v:val) : hprop :=
fun '(h,g) => h = state_single l v /\ g = state_empty.
(** Read-only singleton heap
(** Read-only singleton heap *)
Definition heap_is_single_ro (l:loc) (v:val) : hprop :=
fun '(h,g) => h = state_empty /\ g = state_single l v.
*)
(** Heap union *)
Definition heap_is_star (H1 H2 : hprop) : hprop :=
fun '(h,g) => exists h1 h2 g1 g2,
fun '(h,g) => exists h1 g1 h2 g2,
H1 (h1,g1)
/\ H2 (h2,g2)
/\ state_disjoint h1 h2
......@@ -271,9 +257,9 @@ Proof using. introv M (x&N). rewrites~ (>> M N). Qed.
(********************************************************************)
(* ** Read-only *)
Definition RO H :=
Definition RO (H:hprop) : hprop :=
fun '(h,g) =>
h = empty
h = state_empty
/\ exists h1 g1, H(h1,g1)
/\ state_disjoint h1 g1
/\ g = state_union h1 g1.
......@@ -282,92 +268,93 @@ Definition RO H :=
Remarque: "RO (r ~~> v \* r ~~:> v)" iff \[False]
*)
Lemma RO_elim : forall H h g,
(RO H) (h,g) -> h = state_empty.
Proof using. introv (M1&M2). auto. Qed.
Lemma RO_ref : (RO (r ~~> v)) = (r ~~:> v).
Proof.
Equivalence de:
{ exists h1 g1 disjoint,
h =empty
g = h1+g1
h1 = singleton_map r v
g1 = empty }
et
{ h = empty
g = singleton_map r v. }
Qed.
Lemma RO_invert : (RO H) (h,g) -> h = empty.
Proof. trivial from definition. Qed.
Definition duplicatable (H:hprop) : Prop :=
H ==> H \* H.
Lemma RO_duplicatable : RO H ==> RO H \* RO H.
Proof.
"RO H" décrit une paire (empty,g), par le lemme précédent.
On donne (empty, empty, g, g) en témoins à ltoile.
Lemma RO_duplicatable : forall H,
duplicatable (RO H).
Proof using.
intros H (h&g) M.
lets E: RO_elim M. subst.
exists state_empty g state_empty g. splits~.
{ apply state_compatible_refl. }
{ rewrite~ state_union_idempotent. }
Qed.
Lemma RO_star : RO (H1 \* H2) = (RO H1 \* RO H2)
Proof.
Equivalence de
{ h = empty
/\ exists h3 g3 disjoints,
g = h3+g3
/\ exists h1 h2 g1 g2,
/\ disjoint (dom h1) (dom h2)
/\ h3 = h1+h2
/\ compatible g1 g2
/\ g3 = g1+g2
/\ H1 (h1,g1)
/\ H2 (h2,g2)
}
et
{
exists h1 h2 g1 g2,
/\ disjoint (dom h1) (dom h2)
/\ h = h1+h2
/\ compatible g1 g2
/\ g = g1+g2
/\ h1 = empty /\ exists h11 g11 disjoints, g1 = h11+g11 /\ H1(h11,g11).
/\ h2 = empty /\ exists h21 g21 disjoints, g2 = h21+g21 /\ H2(h21,g21).
}
Pour h, on a:
- h = empty
- h = h1+h2= empty+empty.
Pour g, on a
- g = h3+g3 = h1+h2+g1+g2 avec H1 (h1,g1) et H2 (h2,g2)
- g = g1+g2 = h11+g11+h21+g21 avec H1(h11,g11) et H2(h21,g21)
Il suffit de faire les instantiations correspondantes.
Lemma RO_singe : forall l v,
(RO (heap_is_single l v))
= heap_is_single_ro l v.
Proof using.
intros. unfold heap_is_single, heap_is_single_ro.
apply prop_ext_1. intros (h,g).
iff (M1&h1&g1&(M2a&M2b)&M3&M4) (M1&M2).
{ subst. split~. }
{ split. auto. exists g h. subst. splits~. }
Qed.
Lemma RO_exists :
RO (Hexists x, H) = Hexists x, RO H.
// formellement :
RO (heap_exists J) = heap_exists (fun x => RO (J x))
Proof.
Equivalence de
{
h = empty
/\ exists h1 g1 disjoints,
g = h1+g1
/\ exists x,
J x (h1,g1).
}
et
{
exists x,
h = empty
/\ exists h1 g1 disjoints,
g = h1+g1
/\ J x(h1,g1).
}
Trivial.
Lemma RO_exists : forall A (J:A->hprop),
RO (heap_is_pack J)
= Hexists x, RO (J x).
Proof using.
intros. apply prop_ext_1. intros (h,g).
iff (M1&(h1&g1&(x&N1)&N2&N3)) (x&(E&h1&g1&N1&N2&N3)).
{ exists x. split*. }
{ split*. exists h1 g1. splits*. exists* x. }
Qed.
Lemma RO_star : forall H1 H2,
RO (H1 \* H2) ==> (RO H1 \* RO H2).
Proof using.
intros. intros (h,g).
intros (M1&(h3&g3&(h1&g1&h2&g2&U1&U2&U3&U4&U5&U6)&N1&N2)).
exists state_empty (h1 \+ g1) state_empty (h2 \+ g2).
subst h3 g3.
rewrite state_disjoint_union_eq_r in N1.
do 2 rewrite state_disjoint_union_eq_l in N1.
destruct N1 as ((N1a&N1b)&N1c&N1d).
splits.
{ split~. exists___. splits*. }
{ split~. exists___. splits*. }
{ apply state_disjoint_empty_l. }
{ subst h. auto. }
{ intros l v1 v2 E1 E2.
unfold state_union, pfun_union in E1,E2. simpls.
unfold state_disjoint, pfun_disjoint in *.
destruct (U3 l) as [C|C].
{ rewrite C in E1. cases (state_data h2 l).
{ destruct (N1b l). congruence. congruence. }
{ applys* U5. } }
{ rewrite C in E2. cases (state_data h1 l).
{ destruct (N1c l). congruence. congruence. }
{ applys* U5. } } }
{ subst g.
do 2 rewrite <- state_union_assoc. fequal.
do 2 rewrite state_union_assoc. fequal.
apply~ state_union_comm. }
Qed.
(* NOT TRUE
Lemma RO_star : forall H1 H2,
RO (H1 \* H2) = (RO H1 \* RO H2).
Proof using.
intros. apply prop_ext_1. intros (h,g). split.
{ intros (M1&(h3&g3&(h1&g1&h2&g2&U1&U2&U3&U4&U5&U6)&N1&N2)).
skip. }
{ intros (h1&g1&h2&g2&(M1a&h11&g11&M1b&M1c&M1d)
&(M2a&h12&g12&M2b&M2c&M2d)&M3&M4&M5&M6).
split.
{ subst~. }
{ exists (h11 \+ h12) (g11 \+ g12). splits~.
{ exists h11 g11 h12 g12. splits~. subst. skip. skip. }
{ subst. skip. }
{ subst. skip. } }
Qed.
*)
(********************************************************************)
......
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