proofs/containers/balanced_search_tree/mk.bend
bend-collections-laws-containers@1.0.0.0 · 175 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/u32.bend as U
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/array_ext.bend as AX
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
8import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/layout.bend as LY
10
11# The canonical block of a list: a perfect tree of depth d whose slots are
12# the list's items (Some) followed by empty slots (None).
13
14
15# the first k slots of the items xs
16def fill(-T: Data, +k: Nat, xs: List<&2, T>) -> List<&2, Maybe<&2, T>>:
17 match k xs:
18 case 0n _:
19 Nil{}
20 case 1n+j Nil{}:
21 Con{None{}, fill(T, j, Nil{})}
22 case 1n+j Con{x, r}:
23 Con{Some{x}, fill(T, j, r)}
24
25def headm(-T: Data, xs: List<&2, T>) -> Maybe<&2, T>:
26 match xs:
27 case Nil{}:
28 None{}
29 case Con{x, r}:
30 Some{x}
31
32def mk(-T: Data, +d: Nat, +xs: List<&2, T>) -> AR.Tree<Maybe<&2, T>>:
33 match d:
34 case 0n:
35 AR.TLeaf{headm(T, xs)}
36 case 1n+p:
37 AR.TNode{mk(T, p, xs), mk(T, p, SC.drop(T, xs, SC.pow2(p)))}
38
39def mk_perfect(-T: Data, +d: Nat, +xs: List<&2, T>) -> {AR.perfect(Maybe<&2, T>, d, mk(T, d, xs)) == True{} : Bool}:
40 match d:
41 case 0n:
42 {==}
43 case 1n+p:
44 L.and_intro(AR.perfect(Maybe<&2, T>, p, mk(T, p, xs)), AR.perfect(Maybe<&2, T>, p, mk(T, p, SC.drop(T, xs, SC.pow2(p)))), mk_perfect(T, p, xs), mk_perfect(T, p, SC.drop(T, xs, SC.pow2(p))))
45
46def fill_add(-T: Data, +a: Nat, +b: Nat, +xs: List<&2, T>) -> {fill(T, Nat.add(a, b), xs) == SC.append(Maybe<&2, T>, fill(T, a, xs), fill(T, b, SC.drop(T, xs, a))) : List<&2, Maybe<&2, T>>}:
47 match a xs:
48 case 0n _:
49 Equal.cong(List<&2, T>, List<&2, Maybe<&2, T>>, z => fill(T, b, z), xs, SC.drop(T, xs, 0n), Equal.sym(List<&2, T>, SC.drop(T, xs, 0n), xs, AX.drop_zero(T, xs)))
50 case 1n+j Nil{}:
51 LL.cons_cong(Maybe<&2, T>, None{}, fill(T, Nat.add(j, b), Nil{}), SC.append(Maybe<&2, T>, fill(T, j, Nil{}), fill(T, b, Nil{})), fill_add(T, j, b, Nil{}))
52 case 1n+j Con{x, +r}:
53 LL.cons_cong(Maybe<&2, T>, Some{x}, fill(T, Nat.add(j, b), r), SC.append(Maybe<&2, T>, fill(T, j, r), fill(T, b, SC.drop(T, r, j))), fill_add(T, j, b, r))
54
55def dbl(+p: Nat) -> {SC.pow2(1n+p) == Nat.add(SC.pow2(p), SC.pow2(p)) : Nat}:
56 Equal.trans(Nat, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), Nat.add(SC.pow2(p), 0n)), Nat.add(SC.pow2(p), SC.pow2(p)), U.double_pow(SC.pow2(p)), Equal.cong(Nat, Nat, z => Nat.add(SC.pow2(p), z), Nat.add(SC.pow2(p), 0n), SC.pow2(p), N.add_zero(SC.pow2(p))))
57
58def fill_one(-T: Data, +xs: List<&2, T>) -> {fill(T, 1n, xs) == Con{headm(T, xs), Nil{}} : List<&2, Maybe<&2, T>>}:
59 match xs:
60 case Nil{}:
61 {==}
62 case Con{x, r}:
63 {==}
64
65# the slots of the canonical block
66def mk_slots(-T: Data, +d: Nat, +xs: List<&2, T>) -> {AR.slots(Maybe<&2, T>, mk(T, d, xs)) == fill(T, SC.pow2(d), xs) : List<&2, Maybe<&2, T>>}:
67 match d:
68 case 0n:
69 Equal.sym(List<&2, Maybe<&2, T>>, fill(T, 1n, xs), Con{headm(T, xs), Nil{}}, fill_one(T, xs))
70 case 1n+p:
71 +P = SC.pow2(p)
72 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, mk(T, p, xs)), fill(T, P, xs), mk_slots(T, p, xs)) : {SC.append(Maybe<&2, T>, _, AR.slots(Maybe<&2, T>, mk(T, p, SC.drop(T, xs, P)))) == fill(T, SC.pow2(1n+p), xs) : List<&2, Maybe<&2, T>>}
73 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, mk(T, p, SC.drop(T, xs, P))), fill(T, P, SC.drop(T, xs, P)), mk_slots(T, p, SC.drop(T, xs, P))) : {SC.append(Maybe<&2, T>, fill(T, P, xs), _) == fill(T, SC.pow2(1n+p), xs) : List<&2, Maybe<&2, T>>}
74 %Equal.sym(Nat, SC.pow2(1n+p), Nat.add(P, P), dbl(p)) : {SC.append(Maybe<&2, T>, fill(T, P, xs), fill(T, P, SC.drop(T, xs, P))) == fill(T, _, xs) : List<&2, Maybe<&2, T>>}
75 Equal.sym(List<&2, Maybe<&2, T>>, fill(T, Nat.add(P, P), xs), SC.append(Maybe<&2, T>, fill(T, P, xs), fill(T, P, SC.drop(T, xs, P))), fill_add(T, P, P, xs))
76
77# ---- the layout facts ----
78
79def fill_somes(-T: Data, +k: Nat, +xs: List<&2, T>, +h: {Nat.is_le(SC.length(T, xs), k) == True{} : Bool}) -> {LY.somes(T, fill(T, k, xs)) == xs : List<&2, T>}:
80 match k xs:
81 case 0n Nil{}:
82 {==}
83 case 0n Con{x, r}:
84 Empty.absurd({Nil{} == Con{x, r} : List<&2, T>}, L.false_true(h))
85 case 1n+j Nil{}:
86 fill_somes(T, j, Nil{}, N.zero_le(j))
87 case 1n+j Con{x, +r}:
88 LL.cons_cong(T, x, LY.somes(T, fill(T, j, r)), r, fill_somes(T, j, r, h))
89
90def fill_nones(-T: Data, +k: Nat) -> {LY.nones(T, fill(T, k, Nil{})) == True{} : Bool}:
91 match k:
92 case 0n:
93 {==}
94 case 1n+j:
95 fill_nones(T, j)
96
97def fill_lay(-T: Data, +k: Nat, +xs: List<&2, T>, +h: {Nat.is_le(SC.length(T, xs), k) == True{} : Bool}) -> {LY.lay(T, fill(T, k, xs), SC.length(T, xs)) == True{} : Bool}:
98 match k xs:
99 case 0n Nil{}:
100 {==}
101 case 0n Con{x, r}:
102 Empty.absurd({LY.lay(T, Nil{}, 1n+SC.length(T, r)) == True{} : Bool}, L.false_true(h))
103 case 1n+j Nil{}:
104 fill_nones(T, j)
105 case 1n+j Con{x, +r}:
106 fill_lay(T, j, r, h)
107
108def fill_len(-T: Data, +k: Nat, +xs: List<&2, T>) -> {SC.length(Maybe<&2, T>, fill(T, k, xs)) == k : Nat}:
109 match k xs:
110 case 0n _:
111 {==}
112 case 1n+j Nil{}:
113 N.succ_cong(SC.length(Maybe<&2, T>, fill(T, j, Nil{})), j, fill_len(T, j, Nil{}))
114 case 1n+j Con{x, +r}:
115 N.succ_cong(SC.length(Maybe<&2, T>, fill(T, j, r)), j, fill_len(T, j, r))
116
117def fill_upd(-T: Data, +k: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> {SC.update(Maybe<&2, T>, fill(T, k, xs), i, Some{v}) == fill(T, k, SC.update(T, xs, i, v)) : List<&2, Maybe<&2, T>>}:
118 match k xs i:
119 case 0n _ _:
120 {==}
121 case 1n+j Nil{} _:
122 Empty.absurd({SC.update(Maybe<&2, T>, fill(T, 1n+j, Nil{}), i, Some{v}) == fill(T, 1n+j, Nil{}) : List<&2, Maybe<&2, T>>}, N.lt_zero_absurd(i, h))
123 case 1n+j Con{x, r} 0n:
124 {==}
125 case 1n+j Con{x, +r} 1n+q:
126 LL.cons_cong(Maybe<&2, T>, Some{x}, SC.update(Maybe<&2, T>, fill(T, j, r), q, Some{v}), fill(T, j, SC.update(T, r, q, v)), fill_upd(T, j, r, q, v, h))
127
128def fill_snoc(-T: Data, +k: Nat, +xs: List<&2, T>, +v: T, +h: {Nat.is_lt(SC.length(T, xs), k) == True{} : Bool}) -> {SC.update(Maybe<&2, T>, fill(T, k, xs), SC.length(T, xs), Some{v}) == fill(T, k, SC.snoc(T, xs, v)) : List<&2, Maybe<&2, T>>}:
129 match k xs:
130 case 0n _:
131 Empty.absurd({SC.update(Maybe<&2, T>, Nil{}, SC.length(T, xs), Some{v}) == Nil{} : List<&2, Maybe<&2, T>>}, N.lt_zero_absurd(SC.length(T, xs), h))
132 case 1n+j Nil{}:
133 {==}
134 case 1n+j Con{x, +r}:
135 LL.cons_cong(Maybe<&2, T>, Some{x}, SC.update(Maybe<&2, T>, fill(T, j, r), SC.length(T, r), Some{v}), fill(T, j, SC.snoc(T, r, v)), fill_snoc(T, j, r, v, h))
136
137# ---- trees equal to canonical blocks ----
138
139def mk_eq(-T: Data, +d: Nat, +u: AR.Tree<Maybe<&2, T>>, +xs: List<&2, T>, +pu: {AR.perfect(Maybe<&2, T>, d, u) == True{} : Bool}, +e: {AR.slots(Maybe<&2, T>, u) == fill(T, SC.pow2(d), xs) : List<&2, Maybe<&2, T>>}) -> {u == mk(T, d, xs) : AR.Tree<Maybe<&2, T>>}:
140 AX.tree_ext(Maybe<&2, T>, d, u, mk(T, d, xs), pu, mk_perfect(T, d, xs), Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, u), fill(T, SC.pow2(d), xs), AR.slots(Maybe<&2, T>, mk(T, d, xs)), e, Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), fill(T, SC.pow2(d), xs), mk_slots(T, d, xs))))
141
142# a slot written below the length
143def mk_set(-T: Data, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.upd(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v}) == mk(T, d, SC.update(T, xs, i, v)) : AR.Tree<Maybe<&2, T>>}:
144 +hi = N.lt_le_trans(i, SC.length(T, xs), SC.pow2(d), h, hc)
145 +es = Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), i, Some{v}), fill(T, SC.pow2(d), SC.update(T, xs, i, v)), AR.upd_slots(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v}, hi, mk_perfect(T, d, xs)), Equal.trans(List<&2, Maybe<&2, T>>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), i, Some{v}), SC.update(Maybe<&2, T>, fill(T, SC.pow2(d), xs), i, Some{v}), fill(T, SC.pow2(d), SC.update(T, xs, i, v)), Equal.cong(List<&2, Maybe<&2, T>>, List<&2, Maybe<&2, T>>, z => SC.update(Maybe<&2, T>, z, i, Some{v}), AR.slots(Maybe<&2, T>, mk(T, d, xs)), fill(T, SC.pow2(d), xs), mk_slots(T, d, xs)), fill_upd(T, SC.pow2(d), xs, i, v, h)))
146 mk_eq(T, d, AR.upd(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v}), SC.update(T, xs, i, v), AR.upd_perfect(Maybe<&2, T>, d, mk(T, d, xs), i, Some{v}, mk_perfect(T, d, xs)), es)
147
148# the slot at the length written (a push with room)
149def mk_push(-T: Data, +d: Nat, +xs: List<&2, T>, +v: T, +h: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.upd(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v}) == mk(T, d, SC.snoc(T, xs, v)) : AR.Tree<Maybe<&2, T>>}:
150 +es = Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), SC.length(T, xs), Some{v}), fill(T, SC.pow2(d), SC.snoc(T, xs, v)), AR.upd_slots(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v}, h, mk_perfect(T, d, xs)), Equal.trans(List<&2, Maybe<&2, T>>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, mk(T, d, xs)), SC.length(T, xs), Some{v}), SC.update(Maybe<&2, T>, fill(T, SC.pow2(d), xs), SC.length(T, xs), Some{v}), fill(T, SC.pow2(d), SC.snoc(T, xs, v)), Equal.cong(List<&2, Maybe<&2, T>>, List<&2, Maybe<&2, T>>, z => SC.update(Maybe<&2, T>, z, SC.length(T, xs), Some{v}), AR.slots(Maybe<&2, T>, mk(T, d, xs)), fill(T, SC.pow2(d), xs), mk_slots(T, d, xs)), fill_snoc(T, SC.pow2(d), xs, v, h)))
151 mk_eq(T, d, AR.upd(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v}), SC.snoc(T, xs, v), AR.upd_perfect(Maybe<&2, T>, d, mk(T, d, xs), SC.length(T, xs), Some{v}, mk_perfect(T, d, xs)), es)
152
153def fill_rep(-T: Data, +k: Nat) -> {fill(T, k, Nil{}) == SC.replicate(Maybe<&2, T>, k, None{}) : List<&2, Maybe<&2, T>>}:
154 match k:
155 case 0n:
156 {==}
157 case 1n+j:
158 LL.cons_cong(Maybe<&2, T>, None{}, fill(T, j, Nil{}), SC.replicate(Maybe<&2, T>, j, None{}), fill_rep(T, j))
159
160def drop_all(-T: Data, +xs: List<&2, T>, +k: Nat, +h: {Nat.is_le(SC.length(T, xs), k) == True{} : Bool}) -> {SC.drop(T, xs, k) == Nil{} : List<&2, T>}:
161 match xs k:
162 case Nil{} _:
163 {==}
164 case Con{x, r} 0n:
165 Empty.absurd({Con{x, r} == Nil{} : List<&2, T>}, L.false_true(h))
166 case Con{x, +r} 1n+j:
167 drop_all(T, r, j, h)
168
169# the doubled block of a full list (old block and an empty half)
170def mk_grow(-T: Data, +d: Nat, +xs: List<&2, T>, +hc: {Nat.is_le(SC.length(T, xs), SC.pow2(d)) == True{} : Bool}) -> {AR.TNode{mk(T, d, xs), AR.trep(Maybe<&2, T>, d, None{})} == mk(T, 1n+d, xs) : AR.Tree<Maybe<&2, T>>}:
171 +e1 = Equal.trans(AR.Tree<Maybe<&2, T>>, AR.trep(Maybe<&2, T>, d, None{}), mk(T, d, Nil{}), mk(T, d, SC.drop(T, xs, SC.pow2(d))), mk_eq(T, d, AR.trep(Maybe<&2, T>, d, None{}), Nil{}, AR.trep_perfect(Maybe<&2, T>, d, None{}), Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), fill(T, SC.pow2(d), Nil{}), AR.trep_slots(Maybe<&2, T>, d, None{}), Equal.sym(List<&2, Maybe<&2, T>>, fill(T, SC.pow2(d), Nil{}), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), fill_rep(T, SC.pow2(d))))), Equal.cong(List<&2, T>, AR.Tree<Maybe<&2, T>>, z => mk(T, d, z), Nil{}, SC.drop(T, xs, SC.pow2(d)), Equal.sym(List<&2, T>, SC.drop(T, xs, SC.pow2(d)), Nil{}, drop_all(T, xs, SC.pow2(d), hc))))
172 Equal.cong(AR.Tree<Maybe<&2, T>>, AR.Tree<Maybe<&2, T>>, z => AR.TNode{mk(T, d, xs), z}, AR.trep(Maybe<&2, T>, d, None{}), mk(T, d, SC.drop(T, xs, SC.pow2(d))), e1)
173
174def mk_empty(-T: Data, +d: Nat) -> {AR.trep(Maybe<&2, T>, d, None{}) == mk(T, d, Nil{}) : AR.Tree<Maybe<&2, T>>}:
175 mk_eq(T, d, AR.trep(Maybe<&2, T>, d, None{}), Nil{}, AR.trep_perfect(Maybe<&2, T>, d, None{}), Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), fill(T, SC.pow2(d), Nil{}), AR.trep_slots(Maybe<&2, T>, d, None{}), Equal.sym(List<&2, Maybe<&2, T>>, fill(T, SC.pow2(d), Nil{}), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), fill_rep(T, SC.pow2(d)))))