proofs/containers/balanced_search_tree/navl.bend
bend-collections-laws-containers@1.0.0.0 · 93 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/order.bend as O
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
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/ord.bend as OR
8
9# The specification's first_where and last_where over sorted entries split
10# by a key k: entries below k never qualify upward and always downward,
11# entries above k the other way round. (source: tools/generators/tm_hand/navl.src)
12
13
14def fw_app_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +b: Bool, +hb: {S.ordering_ok(cmp(k, S.key(K, V, e)), incl) == b : Bool}, +ih: {S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, t, ys)) == OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, k, incl, t), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}) -> {S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, Con{e, t}, ys)) == OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t}), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}:
15 match b:
16 case True{}:
17 %Equal.sym(Bool, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), True{}, hb) : {S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, t, ys))) == OR.orm(M.Entry<K, V>, S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t)), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}
18 {==}
19 case False{}:
20 %Equal.sym(Bool, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), False{}, hb) : {S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, t, ys))) == OR.orm(M.Entry<K, V>, S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t)), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}
21 ih
22
23def fw_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>) -> {S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, xs, ys)) == OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, k, incl, xs), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}:
24 match xs:
25 case Nil{}:
26 {==}
27 case Con{+e, +t}:
28 fw_app_c(~K, ~V, ~cmp, k, incl, e, t, ys, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), {==}, fw_app(~K, ~V, ~cmp, k, incl, t, ys))
29
30# nothing below k is at or above it
31def fw_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +h: {OR.ltall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.first_where(~K, ~V, ~cmp, k, incl, es) == None{} : Maybe<&2, M.Entry<K, V>>}:
32 match es:
33 case Nil{}:
34 {==}
35 case Con{+e, +t}:
36 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, OR.lt_gt(~K, ~cmp, ~o, S.key(K, V, e), k, L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), h))) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t)) == None{} : Maybe<&2, M.Entry<K, V>>}
37 fw_none(~K, ~V, ~cmp, ~o, k, incl, t, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), h))
38
39# everything above k qualifies: the first
40def fw_head(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +h: {OR.gtall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.first_where(~K, ~V, ~cmp, k, incl, es) == S.head(M.Entry<K, V>, es) : Maybe<&2, M.Entry<K, V>>}:
41 match es:
42 case Nil{}:
43 {==}
44 case Con{+e, +t}:
45 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, O.lt_is(cmp(k, S.key(K, V, e)), L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, t), h))) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t)) == Some{e} : Maybe<&2, M.Entry<K, V>>}
46 {==}
47
48def lw_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>) -> {S.last_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, xs, ys), b) == S.last_where(~K, ~V, ~cmp, k, incl, ys, S.last_where(~K, ~V, ~cmp, k, incl, xs, b)) : Maybe<&2, M.Entry<K, V>>}:
49 match xs:
50 case Nil{}:
51 {==}
52 case Con{+e, +t}:
53 lw_app(~K, ~V, ~cmp, k, incl, t, ys, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, b))
54
55# nothing above k is at or below it: the candidate stays
56def lw_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>, +h: {OR.gtall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.last_where(~K, ~V, ~cmp, k, incl, es, b) == b : Maybe<&2, M.Entry<K, V>>}:
57 match es:
58 case Nil{}:
59 {==}
60 case Con{+e, +t}:
61 %Equal.sym(Cmp, cmp(S.key(K, V, e), k), GT{}, OR.lt_gt(~K, ~cmp, ~o, k, S.key(K, V, e), L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, t), h))) : {S.last_where(~K, ~V, ~cmp, k, incl, t, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, incl), Some{e}, b)) == b : Maybe<&2, M.Entry<K, V>>}
62 lw_none(~K, ~V, ~cmp, ~o, k, incl, t, b, L.and_right(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, t), h))
63
64def last_orm(-K: Data, -V: Data, +u: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +a: Maybe<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>) -> {OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, u}), a) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, u}), b) : Maybe<&2, M.Entry<K, V>>}:
65 match u:
66 case Nil{}:
67 {==}
68 case Con{+e2, +u2}:
69 last_orm(K, V, u2, e2, a, b)
70
71def lw_all_c(-K: Data, -V: Data, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>) -> {OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, t), Some{e}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, t}), b) : Maybe<&2, M.Entry<K, V>>}:
72 match t:
73 case Nil{}:
74 {==}
75 case Con{+e2, +u}:
76 last_orm(K, V, u, e2, Some{e}, b)
77
78# everything below k qualifies: the last, or the candidate when none
79def lw_all(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>, +h: {OR.ltall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.last_where(~K, ~V, ~cmp, k, incl, es, b) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, es), b) : Maybe<&2, M.Entry<K, V>>}:
80 match es:
81 case Nil{}:
82 {==}
83 case Con{+e, +t}:
84 %Equal.sym(Cmp, cmp(S.key(K, V, e), k), LT{}, O.lt_is(cmp(S.key(K, V, e), k), L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), h))) : {S.last_where(~K, ~V, ~cmp, k, incl, t, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, incl), Some{e}, b)) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, t}), b) : Maybe<&2, M.Entry<K, V>>}
85 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, t, Some{e}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, t), Some{e}), lw_all(~K, ~V, ~cmp, k, incl, t, Some{e}, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), h))) : {_ == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, t}), b) : Maybe<&2, M.Entry<K, V>>}
86 lw_all_c(K, V, e, t, b)
87
88def ltall_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +hx: {OR.ltall(~K, ~V, ~cmp, k, xs) == True{} : Bool}, +hy: {OR.ltall(~K, ~V, ~cmp, k, ys) == True{} : Bool}) -> {OR.ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, ys)) == True{} : Bool}:
89 match xs:
90 case Nil{}:
91 hy
92 case Con{+e, +t}:
93 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys)), L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), hx), ltall_app(~K, ~V, ~cmp, k, t, ys, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), hx), hy))