string.bend
bend-mathlib@0.7.0.0 · 667 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.7.0.0/nat.bend as MNat
5import bend-mathlib@0.7.0.0/bool.bend as MBool
6
7def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
8 %e : Bool.pick(Type, _, Empty, Unit)
9 Unit{}
10
11def internal_append_nil(a: String) -> {a == String.append(a, SNil{}) : String}:
12 match a:
13 case SNil{}:
14 {==}
15 case SCon{+h, +t}:
16 %internal_append_nil(t) : {SCon{h, t} == SCon{h, _} : String}
17 {==}
18
19# The empty string is a right identity for append: a ++ "" = a.
20law append_nil:
21 for a: String
22 {String.append(a, SNil{}) == a : String}
23
24def append_nil(a):
25 Equal.sym(String, a, String.append(a, SNil{}), internal_append_nil(a))
26
27# The empty string is a left identity for append: "" ++ a = a.
28law nil_append:
29 for -a: String
30 {String.append(SNil{}, a) == a : String}
31
32def nil_append(a):
33 {==}
34
35def internal_append_assoc(a: String, -b: String, -c: String) -> {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}:
36 match a:
37 case SNil{}:
38 {==}
39 case SCon{+h, +t}:
40 %internal_append_assoc(t, b, c) : {SCon{h, String.append(t, String.append(b, c))} == SCon{h, _} : String}
41 {==}
42
43# Append is associative: (a ++ b) ++ c = a ++ (b ++ c).
44law append_assoc:
45 for a: String
46 for -b: String
47 for -c: String
48 {String.append(String.append(a, b), c) == String.append(a, String.append(b, c)) : String}
49
50def append_assoc(a, b, c):
51 Equal.sym(String, String.append(a, String.append(b, c)), String.append(String.append(a, b), c), internal_append_assoc(a, b, c))
52
53def internal_length_append(a: String, -b: String) -> {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}:
54 match a:
55 case SNil{}:
56 {==}
57 case SCon{+h, +t}:
58 %internal_length_append(t, b) : {1n+Nat.add(String.length(t), String.length(b)) == 1n+_ : Nat}
59 {==}
60
61# The length of an append is the sum of the lengths.
62law length_append:
63 for a: String
64 for -b: String
65 {String.length(String.append(a, b)) == Nat.add(String.length(a), String.length(b)) : Nat}
66
67def length_append(a, b):
68 Equal.sym(Nat, Nat.add(String.length(a), String.length(b)), String.length(String.append(a, b)), internal_length_append(a, b))
69
70def internal_reverse_go_spec(s: String, +acc: String) -> {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}:
71 match s:
72 case SNil{}:
73 {==}
74 case SCon{+h, +t}:
75 %internal_reverse_go_spec(t, SCon{h, SNil{}}) : {String.append(_, acc) == String.reverse.go(t, SCon{h, acc}) : String}
76 %internal_append_assoc(String.reverse(t), SCon{h, SNil{}}, acc) : {_ == String.reverse.go(t, SCon{h, acc}) : String}
77 %internal_reverse_go_spec(t, SCon{h, acc}) : {String.append(String.reverse(t), SCon{h, acc}) == _ : String}
78 {==}
79
80# The reverse accumulator loop appends the reversed string to the accumulator.
81law reverse_go_spec:
82 for s: String
83 for acc: String
84 {String.reverse.go(s, acc) == String.append(String.reverse(s), acc) : String}
85
86def reverse_go_spec(s, acc):
87 Equal.sym(String, String.append(String.reverse(s), acc), String.reverse.go(s, acc), internal_reverse_go_spec(s, acc))
88
89def internal_reverse_append(a: String, +b: String) -> {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}:
90 match a:
91 case SNil{}:
92 %internal_append_nil(String.reverse(b)) : {_ == String.reverse(b) : String}
93 {==}
94 case SCon{+h, +t}:
95 %internal_reverse_go_spec(t, SCon{h, SNil{}}) : {String.append(String.reverse(b), _) == String.reverse.go(String.append(t, b), SCon{h, SNil{}}) : String}
96 %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}
97 %internal_reverse_append(t, b) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == String.append(_, SCon{h, SNil{}}) : String}
98 %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}
99 {==}
100
101# Reversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a.
102law reverse_append:
103 for a: String
104 for b: String
105 {String.reverse(String.append(a, b)) == String.append(String.reverse(b), String.reverse(a)) : String}
106
107def reverse_append(a, b):
108 Equal.sym(String, String.append(String.reverse(b), String.reverse(a)), String.reverse(String.append(a, b)), internal_reverse_append(a, b))
109
110def internal_reverse_reverse(a: String) -> {a == String.reverse(String.reverse(a)) : String}:
111 match a:
112 case SNil{}:
113 {==}
114 case SCon{+h, +t}:
115 %internal_reverse_go_spec(t, SCon{h, SNil{}}) : {SCon{h, t} == String.reverse.go(_, SNil{}) : String}
116 %internal_reverse_append(String.reverse(t), SCon{h, SNil{}}) : {SCon{h, t} == _ : String}
117 %internal_reverse_reverse(t) : {SCon{h, t} == String.append(String.reverse(SCon{h, SNil{}}), _) : String}
118 {==}
119
120# Reversing twice gives the string back.
121law reverse_reverse:
122 for a: String
123 {String.reverse(String.reverse(a)) == a : String}
124
125def reverse_reverse(a):
126 Equal.sym(String, a, String.reverse(String.reverse(a)), internal_reverse_reverse(a))
127
128def internal_word_cmp_refl(n: Nat, w: Word(n)) -> {EQ{} == Word.cmp(n, w, w) : Cmp}:
129 match n:
130 case 0n:
131 {==}
132 case 1n+p:
133 match w:
134 case WCon{ab, at}:
135 %internal_word_cmp_refl(p, at) : {EQ{} == Word.cmp.fin(ab, ab, _) : Cmp}
136 %Equal.sym(Cmp, Bool.cmp(ab, ab), EQ{}, MBool.cmp_refl(ab)) : {EQ{} == _ : Cmp}
137 {==}
138
139def internal_u32_cmp_refl(x: U32) -> {EQ{} == U32.cmp(x, x) : Cmp}:
140 match x:
141 case U32{w}:
142 %internal_word_cmp_refl(32n, w) : {EQ{} == _ : Cmp}
143 {==}
144
145# Comparing a U32 with itself gives EQ.
146law u32_cmp_refl:
147 for x: U32
148 {U32.cmp(x, x) == EQ{} : Cmp}
149
150def u32_cmp_refl(x):
151 Equal.sym(Cmp, EQ{}, U32.cmp(x, x), internal_u32_cmp_refl(x))
152
153def internal_char_cmp_refl(c: Char) -> {((c, c), EQ{}) == Char.cmp(c, c) : (Char & Char) & Cmp}:
154 match c:
155 case Chr{x}:
156 %internal_u32_cmp_refl(x) : {((Chr{x}, Chr{x}), EQ{}) == ((Chr{x}, Chr{x}), _) : (Char & Char) & Cmp}
157 {==}
158
159# Comparing a character with itself gives EQ and hands both back.
160law char_cmp_refl:
161 for c: Char
162 {Char.cmp(c, c) == ((c, c), EQ{}) : (Char & Char) & Cmp}
163
164def char_cmp_refl(c):
165 Equal.sym((Char & Char) & Cmp, ((c, c), EQ{}), Char.cmp(c, c), internal_char_cmp_refl(c))
166
167def internal_cmp_refl(s: String) -> {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}:
168 match s:
169 case SNil{}:
170 {==}
171 case SCon{h, t}:
172 match h:
173 case Chr{x}:
174 %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}
175 %internal_cmp_refl(t) : {((SCon{Chr{x}, t}, SCon{Chr{x}, t}), EQ{}) == String.cmp.rec(Chr{x}, Chr{x}, _) : (String & String) & Cmp}
176 {==}
177
178# Comparing a string with itself gives EQ and hands both back.
179law cmp_refl:
180 for s: String
181 {String.cmp(s, s) == ((s, s), EQ{}) : (String & String) & Cmp}
182
183def cmp_refl(s):
184 Equal.sym((String & String) & Cmp, ((s, s), EQ{}), String.cmp(s, s), internal_cmp_refl(s))
185
186# Every string is equal to itself under String.eq.
187law eq_refl:
188 for s: String
189 {String.eq(s, s) == True{} : Bool}
190
191def eq_refl(s):
192 %internal_cmp_refl(s) : {Cmp.is_eq(Pair.snd(String & String, Cmp, _)) == True{} : Bool}
193 {==}
194
195def internal_fin_head(ab: Bool, bb: Bool, c: Cmp, h: {Cmp.is_eq(Word.cmp.fin(ab, bb, c)) == True{} : Bool}) -> {ab == bb : Bool}:
196 match c:
197 case LT{}:
198 Empty.absurd({ab == bb : Bool}, internal_false_ne_true(h))
199 case EQ{}:
200 MBool.eq_of_cmp_eq(ab, bb, h)
201 case GT{}:
202 Empty.absurd({ab == bb : Bool}, internal_false_ne_true(h))
203
204def 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}:
205 match c:
206 case LT{}:
207 Empty.absurd({Cmp.is_eq(LT{}) == True{} : Bool}, internal_false_ne_true(h))
208 case EQ{}:
209 {==}
210 case GT{}:
211 Empty.absurd({Cmp.is_eq(GT{}) == True{} : Bool}, internal_false_ne_true(h))
212
213def 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)}:
214 match n:
215 case 0n:
216 match a b:
217 case WNil{} WNil{}:
218 {==}
219 case 1n+ +p:
220 match a b:
221 case WCon{+ab, +at} WCon{+bb, +bt}:
222 %internal_fin_head(ab, bb, Word.cmp(p, at, bt), h) : {WCon{ab, at} == WCon{_, bt} : Word(1n+p)}
223 %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)}
224 {==}
225
226# Two U32s that U32.is_eq calls equal are equal.
227law u32_eq_of_is_eq:
228 for a: U32
229 for b: U32
230 for h: {U32.is_eq(a, b) == True{} : Bool}
231 {a == b : U32}
232
233def u32_eq_of_is_eq(a, b, h):
234 match a b:
235 case U32{x} U32{y}:
236 %internal_word_eq(32n, x, y, h) : {U32{x} == U32{_} : U32}
237 {==}
238
239# Two characters that Char.is_eq calls equal are equal.
240law char_eq_of_is_eq:
241 for a: Char
242 for b: Char
243 for h: {Char.is_eq(a, b) == True{} : Bool}
244 {a == b : Char}
245
246def char_eq_of_is_eq(a, b, h):
247 match a b:
248 case Chr{x} Chr{y}:
249 %u32_eq_of_is_eq(x, y, h) : {Chr{x} == Chr{_} : Char}
250 {==}
251
252def 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}:
253 match rr:
254 case ((a, b), c):
255 {==}
256
257def 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}:
258 %e : {Cmp.is_eq(_) == True{} : Bool}
259 h
260
261def 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}:
262 match c:
263 case LT{}:
264 Empty.absurd({SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}, internal_false_ne_true(h))
265 case GT{}:
266 Empty.absurd({SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}, internal_false_ne_true(h))
267 case EQ{}:
268 %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}
269 %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}
270 {==}
271
272# Two strings that String.eq calls equal are equal.
273law eq_of_eq_true:
274 for a: String
275 for b: String
276 for h: {String.eq(a, b) == True{} : Bool}
277 {a == b : String}
278
279def eq_of_eq_true(a, b, h):
280 match a b:
281 case SNil{} SNil{}:
282 {==}
283 case SNil{} SCon{x, t}:
284 Empty.absurd({SNil{} == SCon{x, t} : String}, internal_false_ne_true(h))
285 case SCon{x, t} SNil{}:
286 Empty.absurd({SCon{x, t} == SNil{} : String}, internal_false_ne_true(h))
287 case SCon{Chr{+x}, +t1} SCon{Chr{+y}, +t2}:
288 internal_step(x, y, t1, t2, U32.cmp(x, y), {==}, h, hh => eq_of_eq_true(t1, t2, hh))
289
290def internal_length_reverse_go(s: String, -acc: String) -> {Nat.add(String.length(s), String.length(acc)) == String.length(String.reverse.go(s, acc)) : Nat}:
291 match s:
292 case SNil{}:
293 {==}
294 case SCon{h, +t}:
295 %MNat.add_succ(String.length(t), String.length(acc)) : {_ == String.length(String.reverse.go(t, SCon{h, acc})) : Nat}
296 internal_length_reverse_go(t, SCon{h, acc})
297
298# Reversing preserves the length.
299law length_reverse:
300 for s: String
301 {String.length(String.reverse(s)) == String.length(s) : Nat}
302
303def length_reverse(s):
304 +s = s
305 Equal.trans(Nat, String.length(String.reverse(s)), Nat.add(String.length(s), 0n), String.length(s), Equal.sym(Nat, Nat.add(String.length(s), 0n), String.length(String.reverse(s)), internal_length_reverse_go(s, SNil{})), MNat.add_zero(String.length(s)))
306
307# Reversing the empty string gives the empty string.
308law reverse_nil:
309 {String.reverse(SNil{}) == SNil{} : String}
310
311def reverse_nil():
312 {==}
313
314# Reversing a one-character string gives it back.
315law reverse_singleton:
316 for -c: Char
317 {String.reverse(SCon{c, SNil{}}) == SCon{c, SNil{}} : String}
318
319def reverse_singleton(c):
320 {==}
321
322# A string is empty exactly when its length is zero.
323law is_empty_iff_length_eq_zero:
324 for s: String
325 {String.is_empty(s) == Nat.is_eq(String.length(s), 0n) : Bool}
326
327def is_empty_iff_length_eq_zero(s):
328 match s:
329 case SNil{}:
330 {==}
331 case SCon{h, t}:
332 {==}
333
334# An append is empty exactly when both parts are.
335law is_empty_append:
336 for a: String
337 for -b: String
338 {String.is_empty(String.append(a, b)) == Bool.and(String.is_empty(a), String.is_empty(b)) : Bool}
339
340def is_empty_append(a, b):
341 match a:
342 case SNil{}:
343 {==}
344 case SCon{h, t}:
345 {==}
346
347def internal_is_empty_reverse_go(s: String, -c: Char, -acc: String) -> {String.is_empty(String.reverse.go(s, SCon{c, acc})) == False{} : Bool}:
348 match s:
349 case SNil{}:
350 {==}
351 case SCon{h, t}:
352 internal_is_empty_reverse_go(t, h, SCon{c, acc})
353
354# The reverse is empty exactly when the string is.
355law is_empty_reverse:
356 for s: String
357 {String.is_empty(String.reverse(s)) == String.is_empty(s) : Bool}
358
359def is_empty_reverse(s):
360 match s:
361 case SNil{}:
362 {==}
363 case SCon{h, t}:
364 internal_is_empty_reverse_go(t, h, SNil{})
365
366# Taking n characters and appending the rest after dropping n gives the string back.
367law take_append_drop:
368 for s: String
369 for n: Nat
370 {String.append(String.take(s, n), String.drop(s, n)) == s : String}
371
372def take_append_drop(s, n):
373 match s n:
374 case SNil{} _:
375 {==}
376 case SCon{h, t} 0n:
377 {==}
378 case SCon{+h, t} 1n+p:
379 %take_append_drop(t, p) : {SCon{h, String.append(String.take(t, p), String.drop(t, p))} == SCon{h, _} : String}
380 {==}
381
382# Taking n characters leaves min(n, length) of them.
383law length_take:
384 for s: String
385 for n: Nat
386 {String.length(String.take(s, n)) == Nat.min(n, String.length(s)) : Nat}
387
388def length_take(s, n):
389 match s n:
390 case SNil{} _:
391 Equal.sym(Nat, Nat.min(n, 0n), 0n, MNat.min_zero(n))
392 case SCon{h, t} 0n:
393 {==}
394 case SCon{h, t} 1n+p:
395 %length_take(t, p) : {1n+String.length(String.take(t, p)) == 1n+_ : Nat}
396 {==}
397
398# Dropping n characters leaves length - n of them.
399law length_drop:
400 for s: String
401 for n: Nat
402 {String.length(String.drop(s, n)) == Nat.sub(String.length(s), n) : Nat}
403
404def length_drop(s, n):
405 match s n:
406 case SNil{} _:
407 Equal.sym(Nat, Nat.sub(0n, n), 0n, MNat.zero_sub(n))
408 case SCon{h, t} 0n:
409 {==}
410 case SCon{h, t} 1n+p:
411 length_drop(t, p)
412
413# Converting a character list to a string and back gives the list.
414law to_list_from_list:
415 for cs: List<&2, Char>
416 {String.to_list(String.from_list(cs)) == cs : List<&2, Char>}
417
418def to_list_from_list(cs):
419 match cs:
420 case Nil{}:
421 {==}
422 case +h <> t:
423 %to_list_from_list(t) : {h <> String.to_list(String.from_list(t)) == h <> _ : List<&2, Char>}
424 {==}
425
426# Converting a string to a character list and back gives the string.
427law from_list_to_list:
428 for s: String
429 {String.from_list(String.to_list(s)) == s : String}
430
431def from_list_to_list(s):
432 match s:
433 case SNil{}:
434 {==}
435 case SCon{+h, t}:
436 %from_list_to_list(t) : {SCon{h, String.from_list(String.to_list(t))} == SCon{h, _} : String}
437 {==}
438
439# The characters of an append are the characters of each part, appended.
440law to_list_append:
441 for a: String
442 for -b: String
443 {String.to_list(String.append(a, b)) == List.append(&2, Char, String.to_list(a), String.to_list(b)) : List<&2, Char>}
444
445def to_list_append(a, b):
446 match a:
447 case SNil{}:
448 {==}
449 case SCon{+h, t}:
450 %to_list_append(t, b) : {h <> String.to_list(String.append(t, b)) == h <> _ : List<&2, Char>}
451 {==}
452
453# A string has as many characters as its character list.
454law length_to_list:
455 for s: String
456 {List.length(&2, Char, String.to_list(s)) == String.length(s) : Nat}
457
458def length_to_list(s):
459 match s:
460 case SNil{}:
461 {==}
462 case SCon{h, t}:
463 %length_to_list(t) : {1n+List.length(&2, Char, String.to_list(t)) == 1n+_ : Nat}
464 {==}
465
466# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
467
468# The empty string is a right identity for append: a ++ "" = a, reversed to rewrite toward the simple side.
469law append_nil_sym:
470 for a: String
471 {a == String.append(a, SNil{}) : String}
472
473def append_nil_sym(a):
474 Equal.sym(String, String.append(a, SNil{}), a, append_nil(a))
475
476# The empty string is a left identity for append: "" ++ a = a, reversed to rewrite toward the simple side.
477law nil_append_sym:
478 for -a: String
479 {a == String.append(SNil{}, a) : String}
480
481def nil_append_sym(a):
482 Equal.sym(String, String.append(SNil{}, a), a, nil_append(a))
483
484# Append is associative: (a ++ b) ++ c = a ++ (b ++ c), reversed to rewrite toward the simple side.
485law append_assoc_sym:
486 for a: String
487 for -b: String
488 for -c: String
489 {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}
490
491def append_assoc_sym(a, b, c):
492 Equal.sym(String, String.append(String.append(a, b), c), String.append(a, String.append(b, c)), append_assoc(a, b, c))
493
494# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
495law length_append_sym:
496 for a: String
497 for -b: String
498 {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}
499
500def length_append_sym(a, b):
501 Equal.sym(Nat, String.length(String.append(a, b)), Nat.add(String.length(a), String.length(b)), length_append(a, b))
502
503# The reverse accumulator loop appends the reversed string to the accumulator, reversed to rewrite toward the simple side.
504law reverse_go_spec_sym:
505 for s: String
506 for acc: String
507 {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}
508
509def reverse_go_spec_sym(s, acc):
510 Equal.sym(String, String.reverse.go(s, acc), String.append(String.reverse(s), acc), reverse_go_spec(s, acc))
511
512# Reversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a, reversed to rewrite toward the simple side.
513law reverse_append_sym:
514 for a: String
515 for b: String
516 {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}
517
518def reverse_append_sym(a, b):
519 Equal.sym(String, String.reverse(String.append(a, b)), String.append(String.reverse(b), String.reverse(a)), reverse_append(a, b))
520
521# Reversing twice gives the string back, reversed to rewrite toward the simple side.
522law reverse_reverse_sym:
523 for a: String
524 {a == String.reverse(String.reverse(a)) : String}
525
526def reverse_reverse_sym(a):
527 Equal.sym(String, String.reverse(String.reverse(a)), a, reverse_reverse(a))
528
529# Comparing a U32 with itself gives EQ, reversed to rewrite toward the simple side.
530law u32_cmp_refl_sym:
531 for x: U32
532 {EQ{} == U32.cmp(x, x) : Cmp}
533
534def u32_cmp_refl_sym(x):
535 Equal.sym(Cmp, U32.cmp(x, x), EQ{}, u32_cmp_refl(x))
536
537# Comparing a character with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
538law char_cmp_refl_sym:
539 for c: Char
540 {((c, c), EQ{}) == Char.cmp(c, c) : (Char & Char) & Cmp}
541
542def char_cmp_refl_sym(c):
543 Equal.sym((Char & Char) & Cmp, Char.cmp(c, c), ((c, c), EQ{}), char_cmp_refl(c))
544
545# Comparing a string with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
546law cmp_refl_sym:
547 for s: String
548 {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}
549
550def cmp_refl_sym(s):
551 Equal.sym((String & String) & Cmp, String.cmp(s, s), ((s, s), EQ{}), cmp_refl(s))
552
553# Every string is equal to itself under String.eq, reversed to rewrite toward the simple side.
554law eq_refl_sym:
555 for s: String
556 {True{} == String.eq(s, s) : Bool}
557
558def eq_refl_sym(s):
559 Equal.sym(Bool, String.eq(s, s), True{}, eq_refl(s))
560
561# Reversing preserves the length, reversed to rewrite toward the simple side.
562law length_reverse_sym:
563 for s: String
564 {String.length(s) == String.length(String.reverse(s)) : Nat}
565
566def length_reverse_sym(s):
567 Equal.sym(Nat, String.length(String.reverse(s)), String.length(s), length_reverse(s))
568
569# Reversing the empty string gives the empty string, reversed to rewrite toward the simple side.
570law reverse_nil_sym:
571 {SNil{} == String.reverse(SNil{}) : String}
572
573def reverse_nil_sym():
574 Equal.sym(String, String.reverse(SNil{}), SNil{}, reverse_nil())
575
576# Reversing a one-character string gives it back, reversed to rewrite toward the simple side.
577law reverse_singleton_sym:
578 for -c: Char
579 {SCon{c, SNil{}} == String.reverse(SCon{c, SNil{}}) : String}
580
581def reverse_singleton_sym(c):
582 Equal.sym(String, String.reverse(SCon{c, SNil{}}), SCon{c, SNil{}}, reverse_singleton(c))
583
584# A string is empty exactly when its length is zero, reversed to rewrite toward the simple side.
585law is_empty_iff_length_eq_zero_sym:
586 for s: String
587 {Nat.is_eq(String.length(s), 0n) == String.is_empty(s) : Bool}
588
589def is_empty_iff_length_eq_zero_sym(s):
590 Equal.sym(Bool, String.is_empty(s), Nat.is_eq(String.length(s), 0n), is_empty_iff_length_eq_zero(s))
591
592# An append is empty exactly when both parts are, reversed to rewrite toward the simple side.
593law is_empty_append_sym:
594 for a: String
595 for -b: String
596 {Bool.and(String.is_empty(a), String.is_empty(b)) == String.is_empty(String.append(a, b)) : Bool}
597
598def is_empty_append_sym(a, b):
599 Equal.sym(Bool, String.is_empty(String.append(a, b)), Bool.and(String.is_empty(a), String.is_empty(b)), is_empty_append(a, b))
600
601# The reverse is empty exactly when the string is, reversed to rewrite toward the simple side.
602law is_empty_reverse_sym:
603 for s: String
604 {String.is_empty(s) == String.is_empty(String.reverse(s)) : Bool}
605
606def is_empty_reverse_sym(s):
607 Equal.sym(Bool, String.is_empty(String.reverse(s)), String.is_empty(s), is_empty_reverse(s))
608
609# Taking n characters and appending the rest after dropping n gives the string back, reversed to rewrite toward the simple side.
610law take_append_drop_sym:
611 for s: String
612 for n: Nat
613 {s == String.append(String.take(s, n), String.drop(s, n)) : String}
614
615def take_append_drop_sym(s, n):
616 Equal.sym(String, String.append(String.take(s, n), String.drop(s, n)), s, take_append_drop(s, n))
617
618# Taking n characters leaves min(n, length) of them, reversed to rewrite toward the simple side.
619law length_take_sym:
620 for s: String
621 for n: Nat
622 {Nat.min(n, String.length(s)) == String.length(String.take(s, n)) : Nat}
623
624def length_take_sym(s, n):
625 Equal.sym(Nat, String.length(String.take(s, n)), Nat.min(n, String.length(s)), length_take(s, n))
626
627# Dropping n characters leaves length - n of them, reversed to rewrite toward the simple side.
628law length_drop_sym:
629 for s: String
630 for n: Nat
631 {Nat.sub(String.length(s), n) == String.length(String.drop(s, n)) : Nat}
632
633def length_drop_sym(s, n):
634 Equal.sym(Nat, String.length(String.drop(s, n)), Nat.sub(String.length(s), n), length_drop(s, n))
635
636# Converting a character list to a string and back gives the list, reversed to rewrite toward the simple side.
637law to_list_from_list_sym:
638 for cs: List<&2, Char>
639 {cs == String.to_list(String.from_list(cs)) : List<&2, Char>}
640
641def to_list_from_list_sym(cs):
642 Equal.sym(List<&2, Char>, String.to_list(String.from_list(cs)), cs, to_list_from_list(cs))
643
644# Converting a string to a character list and back gives the string, reversed to rewrite toward the simple side.
645law from_list_to_list_sym:
646 for s: String
647 {s == String.from_list(String.to_list(s)) : String}
648
649def from_list_to_list_sym(s):
650 Equal.sym(String, String.from_list(String.to_list(s)), s, from_list_to_list(s))
651
652# The characters of an append are the characters of each part, appended, reversed to rewrite toward the simple side.
653law to_list_append_sym:
654 for a: String
655 for -b: String
656 {List.append(&2, Char, String.to_list(a), String.to_list(b)) == String.to_list(String.append(a, b)) : List<&2, Char>}
657
658def to_list_append_sym(a, b):
659 Equal.sym(List<&2, Char>, String.to_list(String.append(a, b)), List.append(&2, Char, String.to_list(a), String.to_list(b)), to_list_append(a, b))
660
661# A string has as many characters as its character list, reversed to rewrite toward the simple side.
662law length_to_list_sym:
663 for s: String
664 {String.length(s) == List.length(&2, Char, String.to_list(s)) : Nat}
665
666def length_to_list_sym(s):
667 Equal.sym(Nat, List.length(&2, Char, String.to_list(s)), String.length(s), length_to_list(s))