proofs/containers/balanced_search_tree/tree.bend
bend-collections-laws-containers@1.0.0.0 · 145 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/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
9
10# The ghost tree: its height is at most its size, and the search loop over
11# the node list walks it: from a subtree's root, with fuel above the height,
12# the loop returns the ghost search of the subtree.
13# (source: tools/generators/tm_hand/tree.src)
14
15
16# ---- height ----
17
18def nmax(+a: Nat, +b: Nat) -> Nat:
19 ST.pk(Nat, Nat.is_lt(a, b), b, a)
20
21def ht(t: ST.Tr) -> Nat:
22 match t:
23 case ST.TE{}:
24 0n
25 case ST.TN{i, tl, tr}:
26 1n+nmax(ht(tl), ht(tr))
27
28def max_c(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_le(a, c) == True{} : Bool}, +hb: {Nat.is_le(b, c) == True{} : Bool}, +x: Bool) -> {Nat.is_le(ST.pk(Nat, x, b, a), c) == True{} : Bool}:
29 match x:
30 case True{}:
31 hb
32 case False{}:
33 ha
34
35# max(a, b) <= c when both are
36def max_le(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_le(a, c) == True{} : Bool}, +hb: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(nmax(a, b), c) == True{} : Bool}:
37 max_c(a, b, c, ha, hb, Nat.is_lt(a, b))
38
39def le_max_c(+a: Nat, +b: Nat, +x: Bool, +hx: {Nat.is_lt(a, b) == x : Bool}) -> {Nat.is_le(a, ST.pk(Nat, x, b, a)) == True{} : Bool} & {Nat.is_le(b, ST.pk(Nat, x, b, a)) == True{} : Bool}:
40 match x:
41 case True{}:
42 (N.lt_le(a, b, hx), N.le_refl(b))
43 case False{}:
44 (N.le_refl(a), N.not_lt_le(a, b, hx))
45
46def le_max_l(+a: Nat, +b: Nat) -> {Nat.is_le(a, nmax(a, b)) == True{} : Bool}:
47 Pair.fst({Nat.is_le(a, nmax(a, b)) == True{} : Bool}, {Nat.is_le(b, nmax(a, b)) == True{} : Bool}, le_max_c(a, b, Nat.is_lt(a, b), {==}))
48
49def le_max_r(+a: Nat, +b: Nat) -> {Nat.is_le(b, nmax(a, b)) == True{} : Bool}:
50 Pair.snd({Nat.is_le(a, nmax(a, b)) == True{} : Bool}, {Nat.is_le(b, nmax(a, b)) == True{} : Bool}, le_max_c(a, b, Nat.is_lt(a, b), {==}))
51
52
53def le_add_l(+a: Nat, +b: Nat) -> {Nat.is_le(b, Nat.add(a, b)) == True{} : Bool}:
54 %Equal.sym(Nat, Nat.add(a, b), Nat.add(b, a), N.add_comm(a, b)) : {Nat.is_le(b, _) == True{} : Bool}
55 N.le_add_right(b, a)
56
57# the height is at most the number of ids
58def ht_le(+t: ST.Tr) -> {Nat.is_le(ht(t), SC.length(Nat, ST.ids(t))) == True{} : Bool}:
59 match t:
60 case ST.TE{}:
61 {==}
62 case ST.TN{+i, +tl, +tr}:
63 %Equal.sym(Nat, SC.length(Nat, ST.ids(ST.TN{i, tl, tr})), Nat.add(SC.length(Nat, ST.ids(tl)), 1n+SC.length(Nat, ST.ids(tr))), LL.length_append(Nat, ST.ids(tl), Con{i, ST.ids(tr)})) : {Nat.is_le(1n+nmax(ht(tl), ht(tr)), _) == True{} : Bool}
64 %Equal.sym(Nat, Nat.add(SC.length(Nat, ST.ids(tl)), 1n+SC.length(Nat, ST.ids(tr))), 1n+Nat.add(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr))), N.add_succ(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr)))) : {Nat.is_le(1n+nmax(ht(tl), ht(tr)), _) == True{} : Bool}
65 max_le(ht(tl), ht(tr), Nat.add(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr))), N.le_trans(ht(tl), SC.length(Nat, ST.ids(tl)), Nat.add(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr))), ht_le(tl), N.le_add_right(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr)))), N.le_trans(ht(tr), SC.length(Nat, ST.ids(tr)), Nat.add(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr))), ht_le(tr), le_add_l(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr)))))
66
67def ht_l(+i: Nat, +tl: ST.Tr, +tr: ST.Tr, +f: Nat, +h: {Nat.is_lt(ht(ST.TN{i, tl, tr}), 1n+f) == True{} : Bool}) -> {Nat.is_lt(ht(tl), f) == True{} : Bool}:
68 N.le_lt_trans(ht(tl), nmax(ht(tl), ht(tr)), f, le_max_l(ht(tl), ht(tr)), h)
69
70def ht_r(+i: Nat, +tl: ST.Tr, +tr: ST.Tr, +f: Nat, +h: {Nat.is_lt(ht(ST.TN{i, tl, tr}), 1n+f) == True{} : Bool}) -> {Nat.is_lt(ht(tr), f) == True{} : Bool}:
71 N.le_lt_trans(ht(tr), nmax(ht(tl), ht(tr)), f, le_max_r(ht(tl), ht(tr)), h)
72
73# ---- the ghost search ----
74
75# the comparison of k with a node's key (a free node: equal, as probe does)
76def kc(~K: Data, ~cmp: K -> K -> Cmp, +k: K, x: M.Node<K>) -> Cmp:
77 match x:
78 case M.Free{f}:
79 EQ{}
80 case M.N{c, a, b, q, key}:
81 cmp(k, key)
82
83def pk3(-T: Data, +c: Cmp, x: T, y: T, z: T) -> T:
84 match c:
85 case LT{}:
86 x
87 case GT{}:
88 y
89 case EQ{}:
90 z
91
92def tsearch(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, t: ST.Tr, +nl: List<&2, M.Node<K>>, +k: K, +p: Nat, +left: Bool) -> M.Search:
93 match t:
94 case ST.TE{}:
95 M.Search{0n, p, left}
96 case ST.TN{+i, tl, tr}:
97 pk3(M.Search, kc(~K, ~cmp, k, ST.nd(K, nl, i)), tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left})
98
99
100def sl_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +left: Bool, +k: K, +f: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +key: K, +ea: {a == ST.rid(tl) : Nat}, +eb: {b == ST.rid(tr) : Nat}, +ihl: {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(tl), i, True{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(tl), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{})) : ST.Sh<K, V> & M.Search}, +ihr: {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(tr), i, False{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(tr), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{})) : ST.Sh<K, V> & M.Search}, +cc: Cmp) -> {MI.search_loop(~K, ~V, ~cmp, 1n+f, k, i, p, left, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (M.N{c, a, b, q, key}, cc))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, pk3(M.Search, cc, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left})) : ST.Sh<K, V> & M.Search}:
101 match cc:
102 case LT{}:
103 %Equal.sym(Nat, a, ST.rid(tl), ea) : {MI.search_loop(~K, ~V, ~cmp, f, k, _, i, True{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _, k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{})) : ST.Sh<K, V> & M.Search}
104 ihl
105 case GT{}:
106 %Equal.sym(Nat, b, ST.rid(tr), eb) : {MI.search_loop(~K, ~V, ~cmp, f, k, _, i, False{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _, k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{})) : ST.Sh<K, V> & M.Search}
107 ihr
108 case EQ{}:
109 {==}
110
111def sl_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +left: Bool, +k: K, +f: Nat, +x: M.Node<K>, +hx: {ST.is_node(K, x, ST.rid(tl), ST.rid(tr), p) == True{} : Bool}, +ihl: {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(tl), i, True{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(tl), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{})) : ST.Sh<K, V> & M.Search}, +ihr: {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(tr), i, False{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(tr), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{})) : ST.Sh<K, V> & M.Search}) -> {MI.search_loop(~K, ~V, ~cmp, 1n+f, k, i, p, left, MI.probe_node(~K, ~V, ~cmp, i, k, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, x))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, pk3(M.Search, kc(~K, ~cmp, k, x), tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left})) : ST.Sh<K, V> & M.Search}:
112 match x:
113 case M.Free{fx}:
114 Empty.absurd({MI.search_loop(~K, ~V, ~cmp, 1n+f, k, i, p, left, MI.probe_node(~K, ~V, ~cmp, i, k, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Free{fx}))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, pk3(M.Search, EQ{}, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left})) : ST.Sh<K, V> & M.Search}, L.false_true(hx))
115 case M.N{+c, +a, +b, +q, +key}:
116 +ha = L.and_left(Nat.is_eq(a, ST.rid(tl)), Bool.and(Nat.is_eq(b, ST.rid(tr)), Nat.is_eq(q, p)), hx)
117 +hb = L.and_left(Nat.is_eq(b, ST.rid(tr)), Nat.is_eq(q, p), L.and_right(Nat.is_eq(a, ST.rid(tl)), Bool.and(Nat.is_eq(b, ST.rid(tr)), Nat.is_eq(q, p)), hx))
118 sl_c(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, i, tl, tr, p, left, k, f, c, a, b, q, key, N.eq_from_is_eq(a, ST.rid(tl), ha), N.eq_from_is_eq(b, ST.rid(tr), hb), ihl, ihr, cmp(k, key))
119
120
121def rep_parts(~K: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +nl: List<&2, M.Node<K>>, +h: {ST.rep(~K, ST.TN{i, tl, tr}, p, nl) == True{} : Bool}) -> {ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p) == True{} : Bool} & ({ST.rep(~K, tl, i, nl) == True{} : Bool} & {ST.rep(~K, tr, i, nl) == True{} : Bool}):
122 +h2 = L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl))), h)
123 +h3 = L.and_right(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), h2)
124 (L.and_left(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), h2), (L.and_left(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl), h3), L.and_right(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl), h3)))
125
126def rep_node(~K: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +nl: List<&2, M.Node<K>>, +h: {ST.rep(~K, ST.TN{i, tl, tr}, p, nl) == True{} : Bool}) -> {ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p) == True{} : Bool}:
127 L.and_left(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl))), h))
128
129def rep_l(~K: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +nl: List<&2, M.Node<K>>, +h: {ST.rep(~K, ST.TN{i, tl, tr}, p, nl) == True{} : Bool}) -> {ST.rep(~K, tl, i, nl) == True{} : Bool}:
130 L.and_left(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl), L.and_right(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl))), h)))
131
132def rep_r(~K: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +nl: List<&2, M.Node<K>>, +h: {ST.rep(~K, ST.TN{i, tl, tr}, p, nl) == True{} : Bool}) -> {ST.rep(~K, tr, i, nl) == True{} : Bool}:
133 L.and_right(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl), L.and_right(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl))), h)))
134
135# the search loop from a subtree's root is the ghost search of the subtree
136def sl(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +f: Nat, +t: ST.Tr, +p: Nat, +left: Bool, +k: K, +hr: {ST.rep(~K, t, p, nl) == True{} : Bool}, +hf: {Nat.is_lt(ht(t), f) == True{} : Bool}) -> {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(t), p, left, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(t), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, t, nl, k, p, left)) : ST.Sh<K, V> & M.Search}:
137 match f t:
138 case 0n _:
139 Empty.absurd({MI.search_loop(~K, ~V, ~cmp, 0n, k, ST.rid(t), p, left, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(t), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, t, nl, k, p, left)) : ST.Sh<K, V> & M.Search}, L.true_not_false(Nat.is_lt(ht(t), 0n), hf, N.not_lt_zero(ht(t))))
140 case 1n+g ST.TE{}:
141 {==}
142 case 1n+g ST.TN{+i, +tl, +tr}:
143 +ihl = sl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, g, tl, i, True{}, k, rep_l(~K, i, tl, tr, p, nl, hr), ht_l(i, tl, tr, g, hf))
144 +ihr = sl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, g, tr, i, False{}, k, rep_r(~K, i, tl, tr, p, nl, hr), ht_r(i, tl, tr, g, hf))
145 sl_node(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, i, tl, tr, p, left, k, g, ST.nd(K, nl, i), rep_node(~K, i, tl, tr, p, nl, hr), ihl, ihr)