proofs/containers/hash_table/strings.bend
bend-collections-laws-containers@1.0.0.0 · 88 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
3import bend-collections-laws-containers@1.0.0.0/src/math/hash.bend as HS
4import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
5
6# The hash map's String walks: hashing hands the key back and folds the
7# multiply-xor mix over its characters; equality is the spec's structural
8# equality and hands both strings back; copying makes two equal strings.
9
10def rr(+s: String, +acc: String) -> {H.rev_onto(H.rev_onto(s, acc), SNil{}) == H.rev_onto(acc, s) : String}:
11 match s:
12 case SNil{}:
13 {==}
14 case SCon{h, t}:
15 rr(t, SCon{h, acc})
16
17def rev2(+s: String) -> {H.rev_onto(H.rev_onto(s, SNil{}), SNil{}) == s : String}:
18 rr(s, SNil{})
19
20# the hash of a key: the mix folded over its character codes
21def fold(s: String, +h: U32) -> U32:
22 match s:
23 case SNil{}:
24 h
25 case SCon{Chr{+c}, t}:
26 fold(t, HS.mix(h, c))
27
28def hash_acc(+s: String, +h: U32, +acc: String) -> {H.hash_acc(s, h, acc) == (H.rev_onto(acc, s), fold(s, h)) : String & U32}:
29 match s:
30 case SNil{}:
31 {==}
32 case SCon{Chr{+c}, t}:
33 hash_acc(t, HS.mix(h, c), SCon{Chr{c}, acc})
34
35# a key's long check word
36def lword(+s: String) -> U32:
37 H.long_word(fold(s, 0))
38
39def key_long(+s: String) -> {H.key_long(s) == (s, lword(s)) : String & U32}:
40 Equal.cong(String & U32, String & U32, r => H.lw_fin(r), H.hash_acc(s, 0, SNil{}), (s, fold(s, 0)), hash_acc(s, 0, SNil{}))
41
42def and_true(+e: Bool) -> {Bool.and(e, True{}) == e : Bool}:
43 match e:
44 case True{}:
45 {==}
46 case False{}:
47 {==}
48
49def and_false(+e: Bool) -> {Bool.and(e, False{}) == False{} : Bool}:
50 match e:
51 case True{}:
52 {==}
53 case False{}:
54 {==}
55
56def and_assoc(+e: Bool, +p: Bool, +q: Bool) -> {Bool.and(Bool.and(e, p), q) == Bool.and(e, Bool.and(p, q)) : Bool}:
57 match e:
58 case True{}:
59 {==}
60 case False{}:
61 {==}
62
63def eq_acc(+a: String, +b: String, +ra: String, +rb: String, +e: Bool) -> {H.eq_acc(a, b, ra, rb, e) == ((H.rev_onto(ra, a), H.rev_onto(rb, b)), Bool.and(e, S.str_eq(a, b))) : (String & String) & Bool}:
64 match a b:
65 case SNil{} SNil{}:
66 Equal.cong(Bool, (String & String) & Bool, z => ((H.rev_onto(ra, SNil{}), H.rev_onto(rb, SNil{})), z), e, Bool.and(e, True{}), Equal.sym(Bool, Bool.and(e, True{}), e, and_true(e)))
67 case SNil{} SCon{h, t}:
68 Equal.cong(Bool, (String & String) & Bool, z => ((H.rev_onto(ra, SNil{}), H.rev_onto(rb, SCon{h, t})), z), False{}, Bool.and(e, False{}), Equal.sym(Bool, Bool.and(e, False{}), False{}, and_false(e)))
69 case SCon{Chr{c}, t} SNil{}:
70 Equal.cong(Bool, (String & String) & Bool, z => ((H.rev_onto(ra, SCon{Chr{c}, t}), H.rev_onto(rb, SNil{})), z), False{}, Bool.and(e, False{}), Equal.sym(Bool, Bool.and(e, False{}), False{}, and_false(e)))
71 case SCon{Chr{+x}, +ta} SCon{Chr{+y}, +tb}:
72 Equal.trans((String & String) & Bool, H.eq_acc(ta, tb, SCon{Chr{x}, ra}, SCon{Chr{y}, rb}, Bool.and(e, U32.is_eq(x, y))), ((H.rev_onto(ra, SCon{Chr{x}, ta}), H.rev_onto(rb, SCon{Chr{y}, tb})), Bool.and(Bool.and(e, U32.is_eq(x, y)), S.str_eq(ta, tb))), ((H.rev_onto(ra, SCon{Chr{x}, ta}), H.rev_onto(rb, SCon{Chr{y}, tb})), Bool.and(e, S.str_eq(SCon{Chr{x}, ta}, SCon{Chr{y}, tb}))),
73 eq_acc(ta, tb, SCon{Chr{x}, ra}, SCon{Chr{y}, rb}, Bool.and(e, U32.is_eq(x, y))),
74 Equal.cong(Bool, (String & String) & Bool, z => ((H.rev_onto(ra, SCon{Chr{x}, ta}), H.rev_onto(rb, SCon{Chr{y}, tb})), z), Bool.and(Bool.and(e, U32.is_eq(x, y)), S.str_eq(ta, tb)), Bool.and(e, Bool.and(U32.is_eq(x, y), S.str_eq(ta, tb))), and_assoc(e, U32.is_eq(x, y), S.str_eq(ta, tb))))
75
76# THEOREM: eq is String equality, handing both strings back.
77def eq(+a: String, +b: String) -> {H.eq(a, b) == ((a, b), S.str_eq(a, b)) : (String & String) & Bool}:
78 eq_acc(a, b, SNil{}, SNil{}, True{})
79
80def copy_acc(+s: String, +ra: String, +rb: String) -> {H.copy_acc(s, ra, rb) == (H.rev_onto(ra, s), H.rev_onto(rb, s)) : String & String}:
81 match s:
82 case SNil{}:
83 {==}
84 case SCon{Chr{+c}, t}:
85 copy_acc(t, SCon{Chr{c}, ra}, SCon{Chr{c}, rb})
86
87def str_copy(+s: String) -> {H.str_copy(s) == (s, s) : String & String}:
88 copy_acc(s, SNil{}, SNil{})