string.bend

bend-mathlib@0.8.1.0 · 731 lines · 78 definitions

1# bend-mathlib/string.bend: String append, reverse and length, and comparison.
2# Comparison descends String.eq -> String.order -> String.cmp -> Char.cmp -> U32.cmp -> Word.cmp.
3import Base
4import bend-mathlib@0.8.1.0/nat.bend as MNat
5import bend-mathlib@0.8.1.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# Base 2.0.38 defines String.order directly, not through String.cmp (PLAN F39); these prove the two agree.
187def internal_order_go_lt(a: String, b: String) -> {String.order.go(a, b, LT{}) == LT{} : Cmp}:
188  match a b:
189    case SNil{} SNil{}:
190      {==}
191    case SNil{} SCon{h, t}:
192      {==}
193    case SCon{h, t} SNil{}:
194      {==}
195    case SCon{Chr{x}, t1} SCon{Chr{y}, t2}:
196      {==}
197
198def internal_order_go_gt(a: String, b: String) -> {String.order.go(a, b, GT{}) == GT{} : Cmp}:
199  match a b:
200    case SNil{} SNil{}:
201      {==}
202    case SNil{} SCon{h, t}:
203      {==}
204    case SCon{h, t} SNil{}:
205      {==}
206    case SCon{Chr{x}, t1} SCon{Chr{y}, t2}:
207      {==}
208
209def internal_cmp_rec_snd(h1: Char, h2: Char, rr: (String & String) & Cmp) -> {Pair.snd(String & String, Cmp, String.cmp.rec(h1, h2, rr)) == Pair.snd(String & String, Cmp, rr) : Cmp}:
210  match rr:
211    case (ts, r):
212      match ts:
213        case (t1, t2):
214          {==}
215
216def internal_order_step(+t1: String, +t2: String, h1: Char, h2: Char, c: Cmp, ih: {String.order.go(t1, t2, EQ{}) == Pair.snd(String & String, Cmp, String.cmp(t1, t2)) : Cmp}) -> {String.order.go(t1, t2, c) == Pair.snd(String & String, Cmp, String.cmp.fin(t1, t2, ((h1, h2), c))) : Cmp}:
217  match c:
218    case LT{}:
219      internal_order_go_lt(t1, t2)
220    case EQ{}:
221      Equal.trans(Cmp, String.order.go(t1, t2, EQ{}), Pair.snd(String & String, Cmp, String.cmp(t1, t2)), Pair.snd(String & String, Cmp, String.cmp.rec(h1, h2, String.cmp(t1, t2))), ih, Equal.sym(Cmp, Pair.snd(String & String, Cmp, String.cmp.rec(h1, h2, String.cmp(t1, t2))), Pair.snd(String & String, Cmp, String.cmp(t1, t2)), internal_cmp_rec_snd(h1, h2, String.cmp(t1, t2))))
222    case GT{}:
223      internal_order_go_gt(t1, t2)
224
225def internal_order_cmp_go(+a: String, +b: String) -> {String.order(a, b) == Pair.snd(String & String, Cmp, String.cmp(a, b)) : Cmp}:
226  match a b:
227    case SNil{} SNil{}:
228      {==}
229    case SNil{} SCon{h, t}:
230      {==}
231    case SCon{h, t} SNil{}:
232      {==}
233    case SCon{Chr{x}, t1} SCon{Chr{y}, t2}:
234      internal_order_step(t1, t2, Chr{x}, Chr{y}, U32.cmp(x, y), internal_order_cmp_go(t1, t2))
235
236# Proofs about String.eq unfold String.order only through this.
237def internal_order_cmp(+a: String, +b: String) -> {Pair.snd(String & String, Cmp, String.cmp(a, b)) == String.order(a, b) : Cmp}:
238  Equal.sym(Cmp, String.order(a, b), Pair.snd(String & String, Cmp, String.cmp(a, b)), internal_order_cmp_go(a, b))
239
240def internal_eq_true_cmp(+a: String, +b: String, h: {String.eq(a, b) == True{} : Bool}) -> {Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp(a, b))) == True{} : Bool}:
241  %Equal.sym(Cmp, Pair.snd(String & String, Cmp, String.cmp(a, b)), String.order(a, b), internal_order_cmp(a, b)) : {Cmp.is_eq(_) == True{} : Bool}
242  h
243
244def internal_cmp_true_eq(+a: String, +b: String, h: {Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp(a, b))) == True{} : Bool}) -> {String.eq(a, b) == True{} : Bool}:
245  %internal_order_cmp(a, b) : {Cmp.is_eq(_) == True{} : Bool}
246  h
247
248# Every string is equal to itself under String.eq.
249law eq_refl:
250  for s: String
251  {String.eq(s, s) == True{} : Bool}
252
253def eq_refl(s):
254  +s = s
255  %internal_order_cmp(s, s) : {Cmp.is_eq(_) == True{} : Bool}
256  %internal_cmp_refl(s) : {Cmp.is_eq(Pair.snd(String & String, Cmp, _)) == True{} : Bool}
257  {==}
258
259def internal_fin_head(ab: Bool, bb: Bool, c: Cmp, h: {Cmp.is_eq(Word.cmp.fin(ab, bb, c)) == True{} : Bool}) -> {ab == bb : Bool}:
260  match c:
261    case LT{}:
262      Empty.absurd({ab == bb : Bool}, internal_false_ne_true(h))
263    case EQ{}:
264      MBool.eq_of_cmp_eq(ab, bb, h)
265    case GT{}:
266      Empty.absurd({ab == bb : Bool}, internal_false_ne_true(h))
267
268def 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}:
269  match c:
270    case LT{}:
271      Empty.absurd({Cmp.is_eq(LT{}) == True{} : Bool}, internal_false_ne_true(h))
272    case EQ{}:
273      {==}
274    case GT{}:
275      Empty.absurd({Cmp.is_eq(GT{}) == True{} : Bool}, internal_false_ne_true(h))
276
277def 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)}:
278  match n:
279    case 0n:
280      match a b:
281        case WNil{} WNil{}:
282          {==}
283    case 1n+ +p:
284      match a b:
285        case WCon{+ab, +at} WCon{+bb, +bt}:
286          %internal_fin_head(ab, bb, Word.cmp(p, at, bt), h) : {WCon{ab, at} == WCon{_, bt} : Word(1n+p)}
287          %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)}
288          {==}
289
290# Two U32s that U32.is_eq calls equal are equal.
291law u32_eq_of_is_eq:
292  for a: U32
293  for b: U32
294  for h: {U32.is_eq(a, b) == True{} : Bool}
295  {a == b : U32}
296
297def u32_eq_of_is_eq(a, b, h):
298  match a b:
299    case U32{x} U32{y}:
300      %internal_word_eq(32n, x, y, h) : {U32{x} == U32{_} : U32}
301      {==}
302
303# Two characters that Char.is_eq calls equal are equal.
304law char_eq_of_is_eq:
305  for a: Char
306  for b: Char
307  for h: {Char.is_eq(a, b) == True{} : Bool}
308  {a == b : Char}
309
310def char_eq_of_is_eq(a, b, h):
311  match a b:
312    case Chr{x} Chr{y}:
313      %u32_eq_of_is_eq(x, y, h) : {Chr{x} == Chr{_} : Char}
314      {==}
315
316def 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}:
317  match rr:
318    case ((a, b), c):
319      {==}
320
321def 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}:
322  %e : {Cmp.is_eq(_) == True{} : Bool}
323  h
324
325def 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: {Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp(t1, t2))) == True{} : Bool} -> {t1 == t2 : String}) -> {SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}:
326  match c:
327    case LT{}:
328      Empty.absurd({SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}, internal_false_ne_true(h))
329    case GT{}:
330      Empty.absurd({SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}, internal_false_ne_true(h))
331    case EQ{}:
332      %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}
333      %ih(Equal.trans(Bool, Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp(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)))), Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp(t1, t2))), internal_rec_is_eq(Chr{x}, Chr{y}, String.cmp(t1, t2))), h)) : {SCon{Chr{x}, t1} == SCon{Chr{x}, _} : String}
334      {==}
335
336# Two strings that String.eq calls equal are equal.
337law eq_of_eq_true:
338  for a: String
339  for b: String
340  for h: {String.eq(a, b) == True{} : Bool}
341  {a == b : String}
342
343def eq_of_eq_true(a, b, h):
344  match a b:
345    case SNil{} SNil{}:
346      {==}
347    case SNil{} SCon{x, t}:
348      Empty.absurd({SNil{} == SCon{x, t} : String}, internal_false_ne_true(h))
349    case SCon{x, t} SNil{}:
350      Empty.absurd({SCon{x, t} == SNil{} : String}, internal_false_ne_true(h))
351    case SCon{Chr{+x}, +t1} SCon{Chr{+y}, +t2}:
352      internal_step(x, y, t1, t2, U32.cmp(x, y), {==}, internal_eq_true_cmp(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}, h), hh => eq_of_eq_true(t1, t2, internal_cmp_true_eq(t1, t2, hh)))
353
354def internal_length_reverse_go(s: String, -acc: String) -> {Nat.add(String.length(s), String.length(acc)) == String.length(String.reverse.go(s, acc)) : Nat}:
355  match s:
356    case SNil{}:
357      {==}
358    case SCon{h, +t}:
359      %MNat.add_succ(String.length(t), String.length(acc)) : {_ == String.length(String.reverse.go(t, SCon{h, acc})) : Nat}
360      internal_length_reverse_go(t, SCon{h, acc})
361
362# Reversing preserves the length.
363law length_reverse:
364  for s: String
365  {String.length(String.reverse(s)) == String.length(s) : Nat}
366
367def length_reverse(s):
368  +s = s
369  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)))
370
371# Reversing the empty string gives the empty string.
372law reverse_nil:
373  {String.reverse(SNil{}) == SNil{} : String}
374
375def reverse_nil():
376  {==}
377
378# Reversing a one-character string gives it back.
379law reverse_singleton:
380  for -c: Char
381  {String.reverse(SCon{c, SNil{}}) == SCon{c, SNil{}} : String}
382
383def reverse_singleton(c):
384  {==}
385
386# A string is empty exactly when its length is zero.
387law is_empty_iff_length_eq_zero:
388  for s: String
389  {String.is_empty(s) == Nat.is_eq(String.length(s), 0n) : Bool}
390
391def is_empty_iff_length_eq_zero(s):
392  match s:
393    case SNil{}:
394      {==}
395    case SCon{h, t}:
396      {==}
397
398# An append is empty exactly when both parts are.
399law is_empty_append:
400  for a: String
401  for -b: String
402  {String.is_empty(String.append(a, b)) == Bool.and(String.is_empty(a), String.is_empty(b)) : Bool}
403
404def is_empty_append(a, b):
405  match a:
406    case SNil{}:
407      {==}
408    case SCon{h, t}:
409      {==}
410
411def internal_is_empty_reverse_go(s: String, -c: Char, -acc: String) -> {String.is_empty(String.reverse.go(s, SCon{c, acc})) == False{} : Bool}:
412  match s:
413    case SNil{}:
414      {==}
415    case SCon{h, t}:
416      internal_is_empty_reverse_go(t, h, SCon{c, acc})
417
418# The reverse is empty exactly when the string is.
419law is_empty_reverse:
420  for s: String
421  {String.is_empty(String.reverse(s)) == String.is_empty(s) : Bool}
422
423def is_empty_reverse(s):
424  match s:
425    case SNil{}:
426      {==}
427    case SCon{h, t}:
428      internal_is_empty_reverse_go(t, h, SNil{})
429
430# Taking n characters and appending the rest after dropping n gives the string back.
431law take_append_drop:
432  for s: String
433  for n: Nat
434  {String.append(String.take(s, n), String.drop(s, n)) == s : String}
435
436def take_append_drop(s, n):
437  match s n:
438    case SNil{} _:
439      {==}
440    case SCon{h, t} 0n:
441      {==}
442    case SCon{+h, t} 1n+p:
443      %take_append_drop(t, p) : {SCon{h, String.append(String.take(t, p), String.drop(t, p))} == SCon{h, _} : String}
444      {==}
445
446# Taking n characters leaves min(n, length) of them.
447law length_take:
448  for s: String
449  for n: Nat
450  {String.length(String.take(s, n)) == Nat.min(n, String.length(s)) : Nat}
451
452def length_take(s, n):
453  match s n:
454    case SNil{} _:
455      Equal.sym(Nat, Nat.min(n, 0n), 0n, MNat.min_zero(n))
456    case SCon{h, t} 0n:
457      {==}
458    case SCon{h, t} 1n+p:
459      %length_take(t, p) : {1n+String.length(String.take(t, p)) == 1n+_ : Nat}
460      {==}
461
462# Dropping n characters leaves length - n of them.
463law length_drop:
464  for s: String
465  for n: Nat
466  {String.length(String.drop(s, n)) == Nat.sub(String.length(s), n) : Nat}
467
468def length_drop(s, n):
469  match s n:
470    case SNil{} _:
471      Equal.sym(Nat, Nat.sub(0n, n), 0n, MNat.zero_sub(n))
472    case SCon{h, t} 0n:
473      {==}
474    case SCon{h, t} 1n+p:
475      length_drop(t, p)
476
477# Converting a character list to a string and back gives the list.
478law to_list_from_list:
479  for cs: List<&2, Char>
480  {String.to_list(String.from_list(cs)) == cs : List<&2, Char>}
481
482def to_list_from_list(cs):
483  match cs:
484    case Nil{}:
485      {==}
486    case +h <> t:
487      %to_list_from_list(t) : {h <> String.to_list(String.from_list(t)) == h <> _ : List<&2, Char>}
488      {==}
489
490# Converting a string to a character list and back gives the string.
491law from_list_to_list:
492  for s: String
493  {String.from_list(String.to_list(s)) == s : String}
494
495def from_list_to_list(s):
496  match s:
497    case SNil{}:
498      {==}
499    case SCon{+h, t}:
500      %from_list_to_list(t) : {SCon{h, String.from_list(String.to_list(t))} == SCon{h, _} : String}
501      {==}
502
503# The characters of an append are the characters of each part, appended.
504law to_list_append:
505  for a: String
506  for -b: String
507  {String.to_list(String.append(a, b)) == List.append(&2, Char, String.to_list(a), String.to_list(b)) : List<&2, Char>}
508
509def to_list_append(a, b):
510  match a:
511    case SNil{}:
512      {==}
513    case SCon{+h, t}:
514      %to_list_append(t, b) : {h <> String.to_list(String.append(t, b)) == h <> _ : List<&2, Char>}
515      {==}
516
517# A string has as many characters as its character list.
518law length_to_list:
519  for s: String
520  {List.length(&2, Char, String.to_list(s)) == String.length(s) : Nat}
521
522def length_to_list(s):
523  match s:
524    case SNil{}:
525      {==}
526    case SCon{h, t}:
527      %length_to_list(t) : {1n+List.length(&2, Char, String.to_list(t)) == 1n+_ : Nat}
528      {==}
529
530# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
531
532# The empty string is a right identity for append: a ++ "" = a, reversed to rewrite toward the simple side.
533law append_nil_sym:
534  for a: String
535  {a == String.append(a, SNil{}) : String}
536
537def append_nil_sym(a):
538  Equal.sym(String, String.append(a, SNil{}), a, append_nil(a))
539
540# The empty string is a left identity for append: "" ++ a = a, reversed to rewrite toward the simple side.
541law nil_append_sym:
542  for -a: String
543  {a == String.append(SNil{}, a) : String}
544
545def nil_append_sym(a):
546  Equal.sym(String, String.append(SNil{}, a), a, nil_append(a))
547
548# Append is associative: (a ++ b) ++ c = a ++ (b ++ c), reversed to rewrite toward the simple side.
549law append_assoc_sym:
550  for a: String
551  for -b: String
552  for -c: String
553  {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}
554
555def append_assoc_sym(a, b, c):
556  Equal.sym(String, String.append(String.append(a, b), c), String.append(a, String.append(b, c)), append_assoc(a, b, c))
557
558# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
559law length_append_sym:
560  for a: String
561  for -b: String
562  {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}
563
564def length_append_sym(a, b):
565  Equal.sym(Nat, String.length(String.append(a, b)), Nat.add(String.length(a), String.length(b)), length_append(a, b))
566
567# The reverse accumulator loop appends the reversed string to the accumulator, reversed to rewrite toward the simple side.
568law reverse_go_spec_sym:
569  for s: String
570  for acc: String
571  {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}
572
573def reverse_go_spec_sym(s, acc):
574  Equal.sym(String, String.reverse.go(s, acc), String.append(String.reverse(s), acc), reverse_go_spec(s, acc))
575
576# Reversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a, reversed to rewrite toward the simple side.
577law reverse_append_sym:
578  for a: String
579  for b: String
580  {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}
581
582def reverse_append_sym(a, b):
583  Equal.sym(String, String.reverse(String.append(a, b)), String.append(String.reverse(b), String.reverse(a)), reverse_append(a, b))
584
585# Reversing twice gives the string back, reversed to rewrite toward the simple side.
586law reverse_reverse_sym:
587  for a: String
588  {a == String.reverse(String.reverse(a)) : String}
589
590def reverse_reverse_sym(a):
591  Equal.sym(String, String.reverse(String.reverse(a)), a, reverse_reverse(a))
592
593# Comparing a U32 with itself gives EQ, reversed to rewrite toward the simple side.
594law u32_cmp_refl_sym:
595  for x: U32
596  {EQ{} == U32.cmp(x, x) : Cmp}
597
598def u32_cmp_refl_sym(x):
599  Equal.sym(Cmp, U32.cmp(x, x), EQ{}, u32_cmp_refl(x))
600
601# Comparing a character with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
602law char_cmp_refl_sym:
603  for c: Char
604  {((c, c), EQ{}) == Char.cmp(c, c) : (Char & Char) & Cmp}
605
606def char_cmp_refl_sym(c):
607  Equal.sym((Char & Char) & Cmp, Char.cmp(c, c), ((c, c), EQ{}), char_cmp_refl(c))
608
609# Comparing a string with itself gives EQ and hands both back, reversed to rewrite toward the simple side.
610law cmp_refl_sym:
611  for s: String
612  {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}
613
614def cmp_refl_sym(s):
615  Equal.sym((String & String) & Cmp, String.cmp(s, s), ((s, s), EQ{}), cmp_refl(s))
616
617# Every string is equal to itself under String.eq, reversed to rewrite toward the simple side.
618law eq_refl_sym:
619  for s: String
620  {True{} == String.eq(s, s) : Bool}
621
622def eq_refl_sym(s):
623  Equal.sym(Bool, String.eq(s, s), True{}, eq_refl(s))
624
625# Reversing preserves the length, reversed to rewrite toward the simple side.
626law length_reverse_sym:
627  for s: String
628  {String.length(s) == String.length(String.reverse(s)) : Nat}
629
630def length_reverse_sym(s):
631  Equal.sym(Nat, String.length(String.reverse(s)), String.length(s), length_reverse(s))
632
633# Reversing the empty string gives the empty string, reversed to rewrite toward the simple side.
634law reverse_nil_sym:
635  {SNil{} == String.reverse(SNil{}) : String}
636
637def reverse_nil_sym():
638  Equal.sym(String, String.reverse(SNil{}), SNil{}, reverse_nil())
639
640# Reversing a one-character string gives it back, reversed to rewrite toward the simple side.
641law reverse_singleton_sym:
642  for -c: Char
643  {SCon{c, SNil{}} == String.reverse(SCon{c, SNil{}}) : String}
644
645def reverse_singleton_sym(c):
646  Equal.sym(String, String.reverse(SCon{c, SNil{}}), SCon{c, SNil{}}, reverse_singleton(c))
647
648# A string is empty exactly when its length is zero, reversed to rewrite toward the simple side.
649law is_empty_iff_length_eq_zero_sym:
650  for s: String
651  {Nat.is_eq(String.length(s), 0n) == String.is_empty(s) : Bool}
652
653def is_empty_iff_length_eq_zero_sym(s):
654  Equal.sym(Bool, String.is_empty(s), Nat.is_eq(String.length(s), 0n), is_empty_iff_length_eq_zero(s))
655
656# An append is empty exactly when both parts are, reversed to rewrite toward the simple side.
657law is_empty_append_sym:
658  for a: String
659  for -b: String
660  {Bool.and(String.is_empty(a), String.is_empty(b)) == String.is_empty(String.append(a, b)) : Bool}
661
662def is_empty_append_sym(a, b):
663  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))
664
665# The reverse is empty exactly when the string is, reversed to rewrite toward the simple side.
666law is_empty_reverse_sym:
667  for s: String
668  {String.is_empty(s) == String.is_empty(String.reverse(s)) : Bool}
669
670def is_empty_reverse_sym(s):
671  Equal.sym(Bool, String.is_empty(String.reverse(s)), String.is_empty(s), is_empty_reverse(s))
672
673# Taking n characters and appending the rest after dropping n gives the string back, reversed to rewrite toward the simple side.
674law take_append_drop_sym:
675  for s: String
676  for n: Nat
677  {s == String.append(String.take(s, n), String.drop(s, n)) : String}
678
679def take_append_drop_sym(s, n):
680  Equal.sym(String, String.append(String.take(s, n), String.drop(s, n)), s, take_append_drop(s, n))
681
682# Taking n characters leaves min(n, length) of them, reversed to rewrite toward the simple side.
683law length_take_sym:
684  for s: String
685  for n: Nat
686  {Nat.min(n, String.length(s)) == String.length(String.take(s, n)) : Nat}
687
688def length_take_sym(s, n):
689  Equal.sym(Nat, String.length(String.take(s, n)), Nat.min(n, String.length(s)), length_take(s, n))
690
691# Dropping n characters leaves length - n of them, reversed to rewrite toward the simple side.
692law length_drop_sym:
693  for s: String
694  for n: Nat
695  {Nat.sub(String.length(s), n) == String.length(String.drop(s, n)) : Nat}
696
697def length_drop_sym(s, n):
698  Equal.sym(Nat, String.length(String.drop(s, n)), Nat.sub(String.length(s), n), length_drop(s, n))
699
700# Converting a character list to a string and back gives the list, reversed to rewrite toward the simple side.
701law to_list_from_list_sym:
702  for cs: List<&2, Char>
703  {cs == String.to_list(String.from_list(cs)) : List<&2, Char>}
704
705def to_list_from_list_sym(cs):
706  Equal.sym(List<&2, Char>, String.to_list(String.from_list(cs)), cs, to_list_from_list(cs))
707
708# Converting a string to a character list and back gives the string, reversed to rewrite toward the simple side.
709law from_list_to_list_sym:
710  for s: String
711  {s == String.from_list(String.to_list(s)) : String}
712
713def from_list_to_list_sym(s):
714  Equal.sym(String, String.from_list(String.to_list(s)), s, from_list_to_list(s))
715
716# The characters of an append are the characters of each part, appended, reversed to rewrite toward the simple side.
717law to_list_append_sym:
718  for a: String
719  for -b: String
720  {List.append(&2, Char, String.to_list(a), String.to_list(b)) == String.to_list(String.append(a, b)) : List<&2, Char>}
721
722def to_list_append_sym(a, b):
723  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))
724
725# A string has as many characters as its character list, reversed to rewrite toward the simple side.
726law length_to_list_sym:
727  for s: String
728  {String.length(s) == List.length(&2, Char, String.to_list(s)) : Nat}
729
730def length_to_list_sym(s):
731  Equal.sym(Nat, List.length(&2, Char, String.to_list(s)), String.length(s), length_to_list(s))