Commit 9d0fb880 authored by charguer's avatar charguer
Browse files

proof rank

parent 3241299c
......@@ -196,6 +196,11 @@ Proof using.
destruct (M x); auto_false.
Qed.
Axiom LibMap_extens : forall A `{Inhab B} (M1 M2:map A B),
dom M1 = dom M2 ->
(forall (x:A), x \indom M1 -> M1[x] = M2[x]) ->
M1 = M2.
End Map.
......
......@@ -240,24 +240,17 @@ Qed.
represented as [Root n] for some [n]. *)
Lemma roots_inv_L_Root : forall x D L R,
roots (LibMap_map parent L) R ->
D = dom L ->
no_self_link D L ->
inv D R L ->
x \in D ->
(R x) \in D ->
exists n, L[R x] = Root n.
Proof using.
introv HR HD HN Hx HRx. forwards~ EQ: roots_inv_L_root x HR.
introv (HD&HR&HN&HL) Hx HRx. forwards~ EQ: roots_inv_L_root x HR.
rewrite~ LibMap_map_read in EQ. cases (L[R x]) as ERx.
{ eauto. } { simpls. false~ HN (R x). }
{ eauto. } { simpls. false~ HL (R x). }
Qed.
Generalizable Variables A B.
Axiom LibMap_extens : forall A `{Inhab B} (M1 M2:map A B),
dom M1 = dom M2 ->
(forall (x:A), M1[x] = M2[x]) ->
M1 = M2.
(** [inv] is preserved by updating the rank information. *)
Lemma inv_rerank : forall x D L L' R n,
inv D R L ->
......@@ -266,10 +259,18 @@ Lemma inv_rerank : forall x D L L' R n,
inv D R L'.
Proof using.
introv HI Hd EL'. lets (HD&HR&HN&HL): HI.
asserts ED: (dom L = dom L').
{ subst L'. rewrite~ dom_update_at_index.
rewrite~ index_eq_indom. rewrite~ <- HD. }
forwards~ HRx: indom_root x HI. splits.
{ subst L'. rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ asserts_rewrite~ (LibMap_map parent L' = LibMap_map parent L).
{ skip. (* TODO applys LibMap_extens. by extensionality ... *) } }
{ applys LibMap_extens. { repeat rewrite LibMap_dom_map. auto. }
{ intros a Ha. rewrite LibMap_dom_map in Ha.
rewrite~ LibMap_map_read. rewrite~ LibMap_map_read; [| rewrite~ ED].
subst L'. rewrite read_update. case_if.
{ forwards~ (m&Hm): roots_inv_L_Root x HI. subst a. rewrite Hm. simple~. }
{ auto. } } } }
{ auto. }
{ subst L'. unfolds no_self_link. intros a b Ha HLa.
rewrite read_update in HLa. case_if. applys~ HL. }
......
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