proofs/containers/balanced_search_tree/plug.bend
bend-collections-laws-containers@1.0.0.0 · 62 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/path.bend as P
8
9# A path plugged with a subtree: the tree it leads through. Its ids are the
10# ids before, the subtree's, and after; it links as the ghost says when the
11# subtree does below the path's parent and the path's frames do.
12# (source: tools/generators/tm_hand/plug.src)
13
14
15def plug(c: List<&2, P.Fr>, t: ST.Tr) -> ST.Tr:
16 match c:
17 case Nil{}:
18 t
19 case Con{f, u}:
20 match f:
21 case P.FR{+p, +lft, s}:
22 match lft:
23 case True{}:
24 plug(u, ST.TN{p, t, s})
25 case False{}:
26 plug(u, ST.TN{p, s, t})
27
28def ids_plug(+c: List<&2, P.Fr>, +t: ST.Tr) -> {ST.ids(plug(c, t)) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}:
29 match c:
30 case Nil{}:
31 Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(t), Nil{}), ST.ids(t), LL.append_nil(Nat, ST.ids(t)))
32 case Con{P.FR{+p, +lft, +s}, +u}:
33 match lft:
34 case True{}:
35 Equal.trans(List<&2, Nat>, ST.ids(plug(u, ST.TN{p, t, s})), SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(ST.TN{p, t, s}), P.after(u))), SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, u}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, u}))), ids_plug(u, ST.TN{p, t, s}), P.ids_l(u, p, t, s))
36 case False{}:
37 Equal.trans(List<&2, Nat>, ST.ids(plug(u, ST.TN{p, s, t})), SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(ST.TN{p, s, t}), P.after(u))), SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, u}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, u}))), ids_plug(u, ST.TN{p, s, t}), P.ids_r(u, p, s, t))
38
39
40# the plugged tree links when the subtree and the path do
41def rep_plug(~K: Data, +nl: List<&2, M.Node<K>>, +c: List<&2, P.Fr>, +t: ST.Tr, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}) -> {ST.rep(~K, plug(c, t), 0n, nl) == True{} : Bool}:
42 match c:
43 case Nil{}:
44 hr
45 case Con{P.FR{+p, +lft, +s}, +u}:
46 match lft:
47 case True{}:
48 +hk = L.and_left(P.cok1(~K, P.FR{p, True{}, s}, ST.rid(t), P.top(u), nl), P.ctxok(~K, u, p, nl), hc)
49 +hu = L.and_right(P.cok1(~K, P.FR{p, True{}, s}, ST.rid(t), P.top(u), nl), P.ctxok(~K, u, p, nl), hc)
50 +h0 = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), ST.rep(~K, s, p, nl)), hk)
51 +h12 = L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), ST.rep(~K, s, p, nl)), hk)
52 +hn = L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), ST.rep(~K, s, p, nl), h12)
53 +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), ST.rep(~K, s, p, nl), h12)
54 rep_plug(~K, nl, u, ST.TN{p, t, s}, L.and_intro(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), Bool.and(ST.rep(~K, t, p, nl), ST.rep(~K, s, p, nl))), h0, L.and_intro(ST.is_node(K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(u)), Bool.and(ST.rep(~K, t, p, nl), ST.rep(~K, s, p, nl)), hn, L.and_intro(ST.rep(~K, t, p, nl), ST.rep(~K, s, p, nl), hr, hs))), hu)
55 case False{}:
56 +hk = L.and_left(P.cok1(~K, P.FR{p, False{}, s}, ST.rid(t), P.top(u), nl), P.ctxok(~K, u, p, nl), hc)
57 +hu = L.and_right(P.cok1(~K, P.FR{p, False{}, s}, ST.rid(t), P.top(u), nl), P.ctxok(~K, u, p, nl), hc)
58 +h0 = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), ST.rep(~K, s, p, nl)), hk)
59 +h12 = L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), ST.rep(~K, s, p, nl)), hk)
60 +hn = L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), ST.rep(~K, s, p, nl), h12)
61 +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), ST.rep(~K, s, p, nl), h12)
62 rep_plug(~K, nl, u, ST.TN{p, s, t}, L.and_intro(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), Bool.and(ST.rep(~K, s, p, nl), ST.rep(~K, t, p, nl))), h0, L.and_intro(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(u)), Bool.and(ST.rep(~K, s, p, nl), ST.rep(~K, t, p, nl)), hn, L.and_intro(ST.rep(~K, s, p, nl), ST.rep(~K, t, p, nl), hs, hr))), hu)