Commit 9b988654 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

fm 2012 pbm 3: simplification

parent 16bb03b1
......@@ -52,7 +52,7 @@ module Treedel
tree m m[p].right r ->
tree m p (Node l p r)
(* degenerated zipper for a left descent *)
(* degenerated zipper for a left descent (= list of pairs) *)
type zipper 'a =
| Top
| Left (zipper 'a) 'a (tree 'a)
......@@ -78,10 +78,10 @@ module Treedel
lemma main_lemma:
forall m: memory, t pp p: pointer, ppr pr: tree pointer, z: zipper pointer.
let it = zip (Node Empty p pr) (Left z pp ppr) in
let it = zip (Node (Node Empty p pr) pp ppr) z in
tree m t it -> distinct (inorder it) ->
let m' = m[pp <- { m[pp] with left = m[p].right }] in
tree m' t (zip pr (Left z pp ppr))
tree m' t (zip (Node pr pp ppr) z)
(* specification is as follows: if t is a tree and its list of pointers
is x::l then, at the end of execution, its list is l and m = *)
......@@ -125,13 +125,8 @@ module Treedel
let m = get_data !p in
tt := get_right !p;
mem := set !mem !pp { !mem[!pp] with left = !tt };
let ghost pl = left !subtree in assert { pl = Empty };
ghost ot := zip (right !subtree) (Left !zipper !pp !ppr);
ghost match !subtree with Empty -> absurd
| Node pl _ pr ->
assert { pl = Empty }; ot := zip pr (Left !zipper !pp !ppr) end;
(t, m)
......@@ -237,10 +237,12 @@ Theorem WP_parameter_search_tree_delete_min : forall (t:pointer) (it:(tree
intros t it mem1 ((h1,h2),h3) h4 h5 h6 h7 o h8 h9 o1 h10 subtree ppr zipper1
tt pp p (h11,(h12,(h13,(h14,h15)))) h16 h17 h18 h19 h20 tt1 h21 mem2 h22.
destruct subtree; auto.
subst subtree1; simpl in h15.
rewrite <- H1.
rewrite <- H5.
subst pl; simpl.
rewrite inorder_zip.
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