proofs/containers/hash_table/keys.bend
bend-collections-laws-containers@1.0.0.0 · 115 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/u32alg.bend as A
4import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
5import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/strings.bend as STR
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as UW
8
9# Key identity: structural String equality is an equivalence, and every key
10# has one check word (a one-character key below 2^31 its short word, any
11# other key its long hash word).
12
13
14def chr_refl(+c: Char) -> {S.chr_eq(c, c) == True{} : Bool}:
15 match c:
16 case Chr{+x}:
17 UW.u32_eq_refl(x)
18
19def str_refl(+s: String) -> {S.str_eq(s, s) == True{} : Bool}:
20 match s:
21 case SNil{}:
22 {==}
23 case SCon{+c, +t}:
24 L.and_intro(S.chr_eq(c, c), S.str_eq(t, t), chr_refl(c), str_refl(t))
25
26def chr_eq_of(+a: Char, +b: Char, +h: {S.chr_eq(a, b) == True{} : Bool}) -> {a == b : Char}:
27 match a b:
28 case Chr{+x} Chr{+y}:
29 Equal.cong(U32, Char, z => Chr{z}, x, y, A.eq_of(x, y, h))
30
31# equal by str_eq means equal
32def str_eq_of(+a: String, +b: String, +h: {S.str_eq(a, b) == True{} : Bool}) -> {a == b : String}:
33 match a b:
34 case SNil{} SNil{}:
35 {==}
36 case SNil{} SCon{c, t}:
37 Empty.absurd({SNil{} == SCon{c, t} : String}, L.false_true(h))
38 case SCon{c, t} SNil{}:
39 Empty.absurd({SCon{c, t} == SNil{} : String}, L.false_true(h))
40 case SCon{+x, +s} SCon{+y, +t}:
41 +ex = chr_eq_of(x, y, L.and_left(S.chr_eq(x, y), S.str_eq(s, t), h))
42 +es = str_eq_of(s, t, L.and_right(S.chr_eq(x, y), S.str_eq(s, t), h))
43 Equal.trans(String, SCon{x, s}, SCon{y, s}, SCon{y, t}, Equal.cong(Char, String, z => SCon{z, s}, x, y, ex), Equal.cong(String, String, z => SCon{y, z}, s, t, es))
44
45def str_eq_true(+a: String, +b: String, +e: {a == b : String}) -> {S.str_eq(a, b) == True{} : Bool}:
46 L.subst(String, z => {S.str_eq(a, z) == True{} : Bool}, a, b, e, str_refl(a))
47
48def sym_c(+a: String, +b: String, +c: Bool, +hc: {S.str_eq(a, b) == c : Bool}, +d: Bool, +hd: {S.str_eq(b, a) == d : Bool}) -> {c == d : Bool}:
49 match c d:
50 case True{} True{}:
51 {==}
52 case False{} False{}:
53 {==}
54 case True{} False{}:
55 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, S.str_eq(b, a), False{}, Equal.sym(Bool, S.str_eq(b, a), True{}, str_eq_true(b, a, Equal.sym(String, a, b, str_eq_of(a, b, hc)))), hd)))
56 case False{} True{}:
57 Empty.absurd({False{} == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, S.str_eq(a, b), False{}, Equal.sym(Bool, S.str_eq(a, b), True{}, str_eq_true(a, b, Equal.sym(String, b, a, str_eq_of(b, a, hd)))), hc)))
58
59def str_sym(+a: String, +b: String) -> {S.str_eq(a, b) == S.str_eq(b, a) : Bool}:
60 sym_c(a, b, S.str_eq(a, b), {==}, S.str_eq(b, a), {==})
61
62# ---- the check word of a key ----
63
64# a one-character key whose code is below 2^31 (stored by its word alone)
65def short_c(+c: U32, t: String) -> Bool:
66 match t:
67 case SNil{}:
68 U32.is_lt(c, H.tag())
69 case SCon{d, r}:
70 False{}
71
72def shortk(key: String) -> Bool:
73 match key:
74 case SNil{}:
75 False{}
76 case SCon{Chr{+c}, +t}:
77 short_c(c, t)
78
79def kw_c(+c: U32, +t: String, sh: Bool) -> U32:
80 match sh:
81 case True{}:
82 H.short_word(c)
83 case False{}:
84 STR.lword(SCon{Chr{c}, t})
85
86def kword(key: String) -> U32:
87 match key:
88 case SNil{}:
89 STR.lword(SNil{})
90 case SCon{Chr{+c}, +t}:
91 kw_c(c, t, short_c(c, t))
92
93def kword_long(+key: String, +hk: {shortk(key) == False{} : Bool}) -> {kword(key) == STR.lword(key) : U32}:
94 match key:
95 case SNil{}:
96 {==}
97 case SCon{Chr{+c}, +t}:
98 L.subst(Bool, b => {kw_c(c, t, b) == STR.lword(SCon{Chr{c}, t}) : U32}, False{}, short_c(c, t), Equal.sym(Bool, short_c(c, t), False{}, hk), {==})
99
100def kword_short(+c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}) -> {kword(SCon{Chr{c}, SNil{}}) == H.short_word(c) : U32}:
101 L.subst(Bool, b => {kw_c(c, SNil{}, b) == H.short_word(c) : U32}, True{}, U32.is_lt(c, H.tag()), Equal.sym(Bool, U32.is_lt(c, H.tag()), True{}, hc), {==})
102
103def not_true_eq(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
104 match b:
105 case True{}:
106 Empty.absurd({True{} == False{} : Bool}, L.false_true(h))
107 case False{}:
108 {==}
109
110def not_true_eq2(+b: Bool, +h: {Bool.not(b) == False{} : Bool}) -> {b == True{} : Bool}:
111 match b:
112 case True{}:
113 {==}
114 case False{}:
115 Empty.absurd({False{} == True{} : Bool}, L.true_false(h))