Commit e4b5e585 authored by charguer's avatar charguer
Browse files

UFarray_map complete

parent 341fd592
......@@ -7,6 +7,19 @@ Require Import TLC.LibListZ.
Generalizable Variables B.
Lemma index_update_inv : forall A `{Inhab B} (L:map A B) (a x:A) (b:B),
index L a ->
index (L[a:=b]) x ->
index L x.
Proof using.
introv IB Ia Ix. rewrite index_eq_indom in *.
rewrite* dom_update_at_index in Ix.
Qed.
Module Import MArray.
......@@ -14,6 +27,7 @@ Parameter MArray : forall A, map int A -> loc -> hprop.
Require Import TLC.LibSet.
Open Scope set_scope.
Definition conseq_dom A (n:int) (M:map int A) : Prop :=
dom M = \set{ i | 0 <= i < n }.
......@@ -21,6 +35,37 @@ Parameter MArray_conseq_dom : forall A (M:map int A) p,
p ~> MArray M ==+> Hexists n, \[conseq_dom n M].
(*******************************************************************)
(** Properties of conseq *)
Lemma conseq_dom_index_eq : forall A n (L:map int A),
conseq_dom n L ->
index n = index L. (* i.e. [index L x <> index n x] *)
Proof using.
introv HD. extens. intros x. rewrite int_index_eq.
rewrite index_eq_indom. unfolds in HD. rewrite HD.
rewrite* in_set_st_eq.
Qed.
Lemma conseq_dom_index_L : forall A n (L:map int A) x,
conseq_dom n L ->
index n x ->
index L x.
Proof. introv Hd Hx. rewrites* <- (>> conseq_dom_index_eq Hd). Qed.
Hint Resolve conseq_dom_index_L.
Lemma conseq_dom_update : forall A n (L:map int A) x y,
conseq_dom n L ->
index n x ->
conseq_dom n (L[x:=y]).
Proof using.
introv HD Hx. unfolds conseq_dom.
rewrite* dom_update_at_index. typeclass.
Qed.
(* TODO: MArray domain *)
(* -------------------------------------------------------------------------- *)
......@@ -258,7 +303,7 @@ Qed.
Hint Resolve index_L.
(** Roots of valid nodes are valid nodes. *)
(* not needed, used onthefly by automation *)
Lemma index_R : forall L R x,
roots L R ->
index L x ->
......@@ -316,7 +361,7 @@ Qed.
(** Lemmas for specifying and justifying the operations *)
Ltac auto_tilde ::=
try solve [ jauto_set; solve [ eauto | congruence | math ] ].
try solve [ jauto_set; solve [ eauto | congruence | math | typeclass ] ].
Hint Resolve index_of_index_length'.
......@@ -359,35 +404,31 @@ Qed.
Lemma udpate_inv : forall L' L a b,
L' = L[a:=b] ->
index L a ->
(forall i, index L i -> index L' i)
/\ (forall i, index L' i -> index L i)
/\ (forall i, index L i -> i <> a -> L'[i] = L[i])
/\ (index L a -> L'[a] = b).
Proof using.
intros. subst. splits; intros.
{ rewrite index_eq_indom in *. rew_map*. typeclass. }
skip. (* TODO { rewrite index_eq_indom in *. rew_map* in H. typeclass. }*)
(*
Print LibMap.
{ rewrite~ @LibMap.update_eq. }
{ rewrite~ @index_update_eq in H. }
{ rewrite~ @read_update_neq. }
{ rewrite~ @read_update_same. }
introv E Da. subst L'. splits.
{ intros. rewrite index_eq_indom in *. rew_map~. }
{ introv H. applys~ index_update_inv Da. }
{ introv H N. rewrite* LibMap.read_update_neq. }
{ introv H. rewrite* LibMap.read_update_same. }
Qed.
*)
Admitted.
(** Lemma for link operations: case of nodes that do not
belong to the two components involved. *)
Lemma repr_update_neq : forall L a b L' x z,
repr L x z ->
index L a ->
L' = L[a:=b] ->
L[a] = a ->
z <> a ->
repr L' x z.
Proof using.
introv M E R N. lets (I1&_&K1&_): udpate_inv (rm E).
introv M Ia E R N. forwards~ (I1&_&K1&_): udpate_inv (rm E).
induction M.
{ applys~ repr_root. rewrite~ K1. }
{ applys~ repr_next y. rewrite~ K1. }
......@@ -404,7 +445,7 @@ Lemma repr_update_eq : forall L a b L' x,
a <> b ->
repr L' x b.
Proof using.
introv M E Ib Rb N. lets (I1&_&K1&K2): udpate_inv (rm E).
introv M E Ib Rb N. forwards~ (I1&_&K1&K2): udpate_inv (rm E).
lets Ra: repr_inv_L M.
gen_eq a': a. induction M; intros E.
{ subst x. applys~ repr_next b. rewrite~ K2.
......@@ -426,7 +467,7 @@ Proof using. (* Note: this proof uses hint [repr_inv_L] *)
introv M HR E N Dx Dy. intros u Du.
forwards~ Hx: roots_inv_L_root x HR.
forwards~ Hy: roots_inv_L_root y HR.
lets (I1&I2&_&_): udpate_inv E.
forwards~ (I1&I2&_&_): udpate_inv E.
rewrites (rm M). unfold link. case_if as C.
{ destruct C as [C|C].
{ rewrite <- C in E. applys~ repr_update_eq E. }
......@@ -444,7 +485,8 @@ Lemma roots_compress : forall L R a L',
Proof using.
introv HR E Da. intros x Dx.
forwards~ Ha: HR a. lets Ra: repr_inv_L Ha.
lets (I1&I2&K1&K2): udpate_inv E. forwards~ M: HR x.
forwards~ (I1&I2&K1&K2): udpate_inv E.
forwards~ M: HR x.
gen_eq z: (R x). induction M; introv Ez.
{ applys~ repr_root. tests C: (x = a).
{ rewrite~ K2. }
......@@ -473,36 +515,6 @@ Definition UF (n:int) (R:int->int) (t:loc) : hprop :=
(*******************************************************************)
(** Hints *)
Lemma conseq_dom_index_eq : forall A n (L:map int A),
conseq_dom n L ->
index n = index L. (* i.e. [index L x <> index n x] *)
Proof using.
introv HD. extens. intros x. rewrite int_index_eq.
rewrite index_eq_indom. unfolds in HD. rewrite HD.
rewrite* in_set_st_eq.
Qed.
Lemma conseq_dom_index_L : forall A n (L:map int A) x,
conseq_dom n L ->
index n x ->
index L x.
Proof. introv Hd Hx. rewrites* <- (>> conseq_dom_index_eq Hd). Qed.
Hint Resolve conseq_dom_index_L.
Lemma conseq_dom_update : forall n L x y,
conseq_dom n L ->
index n x ->
conseq_dom n (L[x:=y]).
Proof using.
introv HD Hx. unfolds conseq_dom.
rewrite* dom_update_at_index. typeclass.
Qed.
(*******************************************************************)
(** Create *)
......@@ -582,7 +594,7 @@ Proof using.
{ unfold UF. xpull. intros L (Hn&HR).
xapp*. xsimpl*. splits.
{ applys* conseq_dom_update.
rewrites (>> conseq_dom_index_eq Hn) in *; applys* index_R. }
rewrites~ (>> conseq_dom_index_eq Hn) in *. }
{ applys* roots_link L R x y. } }
{ xrets. rewrite* link_related. }
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