string.bend
bend-mathlib@0.6.0.0 · 382 lines · 0 definitions
1# bend-mathlib/string.bend: String append, reverse and length, and comparison.
2# Comparison descends String.eq -> String.cmp -> Char.cmp -> U32.cmp -> Word.cmp.
3import Base
4import bend-mathlib@0.6.0.0/bool.bend as MBool
5
6def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
7 %e : Bool.pick(Type, _, Empty, Unit)
8 Unit{}
9
10def internal_append_nil(a: String) -> {a == String.append(a, SNil{}) : String}:
11 match a:
12 case SNil{}:
13 {==}
14 case SCon{+h, +t}:
15 %internal_append_nil(t) : {SCon{h, t} == SCon{h, _} : String}
16 {==}
17
18# The empty string is a right identity for append: a ++ "" = a.
19law append_nil:
20 for a: String
21 {String.append(a, SNil{}) == a : String}
22
23def append_nil(a):
24 Equal.sym(String, a, String.append(a, SNil{}), internal_append_nil(a))
25
26# The empty string is a left identity for append: "" ++ a = a.
27law nil_append:
28 for -a: String
29 {String.append(SNil{}, a) == a : String}
30
31def nil_append(a):
32 {==}
33
34def internal_append_assoc(a: String, -b: String, -c: String) -> {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}:
35 match a:
36 case SNil{}:
37 {==}
38 case SCon{+h, +t}:
39 %internal_append_assoc(t, b, c) : {SCon{h, String.append(t, String.append(b, c))} == SCon{h, _} : String}
40 {==}
41
42# Append is associative: (a ++ b) ++ c = a ++ (b ++ c).
43law append_assoc:
44 for a: String
45 for -b: String
46 for -c: String
47 {String.append(String.append(a, b), c) == String.append(a, String.append(b, c)) : String}
48
49def append_assoc(a, b, c):
50 Equal.sym(String, String.append(a, String.append(b, c)), String.append(String.append(a, b), c), internal_append_assoc(a, b, c))
51
52def internal_length_append(a: String, -b: String) -> {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}:
53 match a:
54 case SNil{}:
55 {==}
56 case SCon{+h, +t}:
57 %internal_length_append(t, b) : {1n+Nat.add(String.length(t), String.length(b)) == 1n+_ : Nat}
58 {==}
59
60# The length of an append is the sum of the lengths.
61law length_append:
62 for a: String
63 for -b: String
64 {String.length(String.append(a, b)) == Nat.add(String.length(a), String.length(b)) : Nat}
65
66def length_append(a, b):
67 Equal.sym(Nat, Nat.add(String.length(a), String.length(b)), String.length(String.append(a, b)), internal_length_append(a, b))
68
69def internal_reverse_go_spec(s: String, +acc: String) -> {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}:
70 match s:
71 case SNil{}:
72 {==}
73 case SCon{+h, +t}:
74 %internal_reverse_go_spec(t, SCon{h, SNil{}}) : {String.append(_, acc) == String.reverse.go(t, SCon{h, acc}) : String}
75 %internal_append_assoc(String.reverse(t), SCon{h, SNil{}}, acc) : {_ == String.reverse.go(t, SCon{h, acc}) : String}
76 %internal_reverse_go_spec(t, SCon{h, acc}) : {String.append(String.reverse(t), SCon{h, acc}) == _ : String}
77 {==}
78
79# The reverse accumulator loop appends the reversed string to the accumulator.
80law reverse_go_spec:
81 for s: String
82 for acc: String
83 {String.reverse.go(s, acc) == String.append(String.reverse(s), acc) : String}
84
85def reverse_go_spec(s, acc):
86 Equal.sym(String, String.append(String.reverse(s), acc), String.reverse.go(s, acc), internal_reverse_go_spec(s, acc))
87
88def internal_reverse_append(a: String, +b: String) -> {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}:
89 match a:
90 case SNil{}:
91 %internal_append_nil(String.reverse(b)) : {_ == String.reverse(b) : String}
92 {==}
93 case SCon{+h, +t}:
94 %internal_reverse_go_spec(t, SCon{h, SNil{}}) : {String.append(String.reverse(b), _) == String.reverse.go(String.append(t, b), SCon{h, SNil{}}) : String}
95 %internal_reverse_go_spec(String.append(t, b), SCon{h, SNil{}}) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == _ : String}
96 %internal_reverse_append(t, b) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == String.append(_, SCon{h, SNil{}}) : String}
97 %internal_append_assoc(String.reverse(b), String.reverse(t), SCon{h, SNil{}}) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == _ : String}
98 {==}
99
100# Reversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a.
101law reverse_append:
102 for a: String
103 for b: String
104 {String.reverse(String.append(a, b)) == String.append(String.reverse(b), String.reverse(a)) : String}
105
106def reverse_append(a, b):
107 Equal.sym(String, String.append(String.reverse(b), String.reverse(a)), String.reverse(String.append(a, b)), internal_reverse_append(a, b))
108
109def internal_reverse_reverse(a: String) -> {a == String.reverse(String.reverse(a)) : String}:
110 match a:
111 case SNil{}:
112 {==}
113 case SCon{+h, +t}:
114 %internal_reverse_go_spec(t, SCon{h, SNil{}}) : {SCon{h, t} == String.reverse.go(_, SNil{}) : String}
115 %internal_reverse_append(String.reverse(t), SCon{h, SNil{}}) : {SCon{h, t} == _ : String}
116 %internal_reverse_reverse(t) : {SCon{h, t} == String.append(String.reverse(SCon{h, SNil{}}), _) : String}
117 {==}
118
119# Reversing twice gives the string back.
120law reverse_reverse:
121 for a: String
122 {String.reverse(String.reverse(a)) == a : String}
123
124def reverse_reverse(a):
125 Equal.sym(String, a, String.reverse(String.reverse(a)), internal_reverse_reverse(a))
126
127def internal_word_cmp_refl(n: Nat, w: Word(n)) -> {EQ{} == Word.cmp(n, w, w) : Cmp}:
128 match n:
129 case 0n:
130 {==}
131 case 1n+p:
132 match w:
133 case WCon{ab, at}:
134 %internal_word_cmp_refl(p, at) : {EQ{} == Word.cmp.fin(ab, ab, _) : Cmp}
135 %Equal.sym(Cmp, Bool.cmp(ab, ab), EQ{}, MBool.cmp_refl(ab)) : {EQ{} == _ : Cmp}
136 {==}
137
138def internal_u32_cmp_refl(x: U32) -> {EQ{} == U32.cmp(x, x) : Cmp}:
139 match x:
140 case U32{w}:
141 %internal_word_cmp_refl(32n, w) : {EQ{} == _ : Cmp}
142 {==}
143
144# Comparing a U32 with itself gives EQ.
145law u32_cmp_refl:
146 for x: U32
147 {U32.cmp(x, x) == EQ{} : Cmp}
148
149def u32_cmp_refl(x):
150 Equal.sym(Cmp, EQ{}, U32.cmp(x, x), internal_u32_cmp_refl(x))
151
152def internal_char_cmp_refl(c: Char) -> {((c, c), EQ{}) == Char.cmp(c, c) : (Char & Char) & Cmp}:
153 match c:
154 case Chr{x}:
155 %internal_u32_cmp_refl(x) : {((Chr{x}, Chr{x}), EQ{}) == ((Chr{x}, Chr{x}), _) : (Char & Char) & Cmp}
156 {==}
157
158# Comparing a character with itself gives EQ and hands both back.
159law char_cmp_refl:
160 for c: Char
161 {Char.cmp(c, c) == ((c, c), EQ{}) : (Char & Char) & Cmp}
162
163def char_cmp_refl(c):
164 Equal.sym((Char & Char) & Cmp, ((c, c), EQ{}), Char.cmp(c, c), internal_char_cmp_refl(c))
165
166def internal_cmp_refl(s: String) -> {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}:
167 match s:
168 case SNil{}:
169 {==}
170 case SCon{h, t}:
171 match h:
172 case Chr{x}:
173 %internal_u32_cmp_refl(x) : {((SCon{Chr{x}, t}, SCon{Chr{x}, t}), EQ{}) == String.cmp.fin(t, t, ((Chr{x}, Chr{x}), _)) : (String & String) & Cmp}
174 %internal_cmp_refl(t) : {((SCon{Chr{x}, t}, SCon{Chr{x}, t}), EQ{}) == String.cmp.rec(Chr{x}, Chr{x}, _) : (String & String) & Cmp}
175 {==}
176
177# Comparing a string with itself gives EQ and hands both back.
178law cmp_refl:
179 for s: String
180 {String.cmp(s, s) == ((s, s), EQ{}) : (String & String) & Cmp}
181
182def cmp_refl(s):
183 Equal.sym((String & String) & Cmp, ((s, s), EQ{}), String.cmp(s, s), internal_cmp_refl(s))
184
185# Every string is equal to itself under String.eq.
186law eq_refl:
187 for s: String
188 {String.eq(s, s) == True{} : Bool}
189
190def eq_refl(s):
191 %internal_cmp_refl(s) : {Cmp.is_eq(Pair.snd(String & String, Cmp, _)) == True{} : Bool}
192 {==}
193
194def internal_fin_head(ab: Bool, bb: Bool, c: Cmp, h: {Cmp.is_eq(Word.cmp.fin(ab, bb, c)) == True{} : Bool}) -> {ab == bb : Bool}:
195 match c:
196 case LT{}:
197 Empty.absurd({ab == bb : Bool}, internal_false_ne_true(h))
198 case EQ{}:
199 MBool.eq_of_cmp_eq(ab, bb, h)
200 case GT{}:
201 Empty.absurd({ab == bb : Bool}, internal_false_ne_true(h))
202
203def internal_fin_tail(ab: Bool, bb: Bool, c: Cmp, h: {Cmp.is_eq(Word.cmp.fin(ab, bb, c)) == True{} : Bool}) -> {Cmp.is_eq(c) == True{} : Bool}:
204 match c:
205 case LT{}:
206 Empty.absurd({Cmp.is_eq(LT{}) == True{} : Bool}, internal_false_ne_true(h))
207 case EQ{}:
208 {==}
209 case GT{}:
210 Empty.absurd({Cmp.is_eq(GT{}) == True{} : Bool}, internal_false_ne_true(h))
211
212def internal_word_eq(n: Nat, a: Word(n), b: Word(n), +h: {Cmp.is_eq(Word.cmp(n, a, b)) == True{} : Bool}) -> {a == b : Word(n)}:
213 match n:
214 case 0n:
215 match a b:
216 case WNil{} WNil{}:
217 {==}
218 case 1n+ +p:
219 match a b:
220 case WCon{+ab, +at} WCon{+bb, +bt}:
221 %internal_fin_head(ab, bb, Word.cmp(p, at, bt), h) : {WCon{ab, at} == WCon{_, bt} : Word(1n+p)}
222 %internal_word_eq(p, at, bt, internal_fin_tail(ab, bb, Word.cmp(p, at, bt), h)) : {WCon{ab, at} == WCon{ab, _} : Word(1n+p)}
223 {==}
224
225# Two U32s that U32.is_eq calls equal are equal.
226law u32_eq_of_is_eq:
227 for a: U32
228 for b: U32
229 for h: {U32.is_eq(a, b) == True{} : Bool}
230 {a == b : U32}
231
232def u32_eq_of_is_eq(a, b, h):
233 match a b:
234 case U32{x} U32{y}:
235 %internal_word_eq(32n, x, y, h) : {U32{x} == U32{_} : U32}
236 {==}
237
238# Two characters that Char.is_eq calls equal are equal.
239law char_eq_of_is_eq:
240 for a: Char
241 for b: Char
242 for h: {Char.is_eq(a, b) == True{} : Bool}
243 {a == b : Char}
244
245def char_eq_of_is_eq(a, b, h):
246 match a b:
247 case Chr{x} Chr{y}:
248 %u32_eq_of_is_eq(x, y, h) : {Chr{x} == Chr{_} : Char}
249 {==}
250
251def internal_rec_is_eq(h1: Char, h2: Char, rr: (String & String) & Cmp) -> {Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp.rec(h1, h2, rr))) == Cmp.is_eq(Pair.snd(String & String, Cmp, rr)) : Bool}:
252 match rr:
253 case ((a, b), c):
254 {==}
255
256def internal_is_eq_of(c: Cmp, +d: Cmp, e: {c == d : Cmp}, h: {Cmp.is_eq(c) == True{} : Bool}) -> {Cmp.is_eq(d) == True{} : Bool}:
257 %e : {Cmp.is_eq(_) == True{} : Bool}
258 h
259
260def internal_step(+x: U32, +y: U32, +t1: String, +t2: String, c: Cmp, ec: {c == U32.cmp(x, y) : Cmp}, h: {Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp.fin(t1, t2, ((Chr{x}, Chr{y}), c)))) == True{} : Bool}, ih: {String.eq(t1, t2) == True{} : Bool} -> {t1 == t2 : String}) -> {SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}:
261 match c:
262 case LT{}:
263 Empty.absurd({SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}, internal_false_ne_true(h))
264 case GT{}:
265 Empty.absurd({SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}, internal_false_ne_true(h))
266 case EQ{}:
267 %u32_eq_of_is_eq(x, y, internal_is_eq_of(EQ{}, U32.cmp(x, y), ec, {==})) : {SCon{Chr{x}, t1} == SCon{Chr{_}, t2} : String}
268 %ih(Equal.trans(Bool, String.eq(t1, t2), Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp.rec(Chr{x}, Chr{y}, String.cmp(t1, t2)))), True{}, Equal.sym(Bool, Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp.rec(Chr{x}, Chr{y}, String.cmp(t1, t2)))), String.eq(t1, t2), internal_rec_is_eq(Chr{x}, Chr{y}, String.cmp(t1, t2))), h)) : {SCon{Chr{x}, t1} == SCon{Chr{x}, _} : String}
269 {==}
270
271# Two strings that String.eq calls equal are equal.
272law eq_of_eq_true:
273 for a: String
274 for b: String
275 for h: {String.eq(a, b) == True{} : Bool}
276 {a == b : String}
277
278def eq_of_eq_true(a, b, h):
279 match a b:
280 case SNil{} SNil{}:
281 {==}
282 case SNil{} SCon{x, t}:
283 Empty.absurd({SNil{} == SCon{x, t} : String}, internal_false_ne_true(h))
284 case SCon{x, t} SNil{}:
285 Empty.absurd({SCon{x, t} == SNil{} : String}, internal_false_ne_true(h))
286 case SCon{Chr{+x}, +t1} SCon{Chr{+y}, +t2}:
287 internal_step(x, y, t1, t2, U32.cmp(x, y), {==}, h, hh => eq_of_eq_true(t1, t2, hh))
288
289# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
290
291# The empty string is a right identity for append: a ++ "" = a, reversed to rewrite toward the simple side.
292law append_nil_sym:
293 for a: String
294 {a == String.append(a, SNil{}) : String}
295
296def append_nil_sym(a):
297 Equal.sym(String, String.append(a, SNil{}), a, append_nil(a))
298
299# The empty string is a left identity for append: "" ++ a = a, reversed to rewrite toward the simple side.
300law nil_append_sym:
301 for -a: String
302 {a == String.append(SNil{}, a) : String}
303
304def nil_append_sym(a):
305 Equal.sym(String, String.append(SNil{}, a), a, nil_append(a))
306
307# Append is associative: (a ++ b) ++ c = a ++ (b ++ c), reversed to rewrite toward the simple side.
308law append_assoc_sym:
309 for a: String
310 for -b: String
311 for -c: String
312 {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}
313
314def append_assoc_sym(a, b, c):
315 Equal.sym(String, String.append(String.append(a, b), c), String.append(a, String.append(b, c)), append_assoc(a, b, c))
316
317# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
318law length_append_sym:
319 for a: String
320 for -b: String
321 {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}
322
323def length_append_sym(a, b):
324 Equal.sym(Nat, String.length(String.append(a, b)), Nat.add(String.length(a), String.length(b)), length_append(a, b))
325
326# The reverse accumulator loop appends the reversed string to the accumulator, reversed to rewrite toward the simple side.
327law reverse_go_spec_sym:
328 for s: String
329 for acc: String
330 {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}
331
332def reverse_go_spec_sym(s, acc):
333 Equal.sym(String, String.reverse.go(s, acc), String.append(String.reverse(s), acc), reverse_go_spec(s, acc))
334
335# Reversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a, reversed to rewrite toward the simple side.
336law reverse_append_sym:
337 for a: String
338 for b: String
339 {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}
340
341def reverse_append_sym(a, b):
342 Equal.sym(String, String.reverse(String.append(a, b)), String.append(String.reverse(b), String.reverse(a)), reverse_append(a, b))
343
344# Reversing twice gives the string back, reversed to rewrite toward the simple side.
345law reverse_reverse_sym:
346 for a: String
347 {a == String.reverse(String.reverse(a)) : String}
348
349def reverse_reverse_sym(a):
350 Equal.sym(String, String.reverse(String.reverse(a)), a, reverse_reverse(a))
351
352# Comparing a U32 with itself gives EQ, reversed to rewrite toward the simple side.
353law u32_cmp_refl_sym:
354 for x: U32
355 {EQ{} == U32.cmp(x, x) : Cmp}
356
357def u32_cmp_refl_sym(x):
358 Equal.sym(Cmp, U32.cmp(x, x), EQ{}, u32_cmp_refl(x))
359
360# Comparing a character with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
361law char_cmp_refl_sym:
362 for c: Char
363 {((c, c), EQ{}) == Char.cmp(c, c) : (Char & Char) & Cmp}
364
365def char_cmp_refl_sym(c):
366 Equal.sym((Char & Char) & Cmp, Char.cmp(c, c), ((c, c), EQ{}), char_cmp_refl(c))
367
368# Comparing a string with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
369law cmp_refl_sym:
370 for s: String
371 {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}
372
373def cmp_refl_sym(s):
374 Equal.sym((String & String) & Cmp, String.cmp(s, s), ((s, s), EQ{}), cmp_refl(s))
375
376# Every string is equal to itself under String.eq, reversed to rewrite toward the simple side.
377law eq_refl_sym:
378 for s: String
379 {True{} == String.eq(s, s) : Bool}
380
381def eq_refl_sym(s):
382 Equal.sym(Bool, String.eq(s, s), True{}, eq_refl(s))