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.
3	import Base
4	import ./nat.bend as MNat
5	import ./bool.bend as MBool
6	
7	def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
8	  %e : Bool.pick(Type, _, Empty, Unit)
9	  Unit{}
10	
11	def 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.
20	law append_nil:
21	  for a: String
22	  {String.append(a, SNil{}) == a : String}
23	
24	def 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.
28	law nil_append:
29	  for -a: String
30	  {String.append(SNil{}, a) == a : String}
31	
32	def nil_append(a):
33	  {==}
34	
35	def 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).
44	law 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	
50	def 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	
53	def 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.
62	law 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	
67	def 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	
70	def 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.
81	law 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	
86	def 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	
89	def 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.
102	law 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	
107	def 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	
110	def 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.
121	law reverse_reverse:
122	  for a: String
123	  {String.reverse(String.reverse(a)) == a : String}
124	
125	def reverse_reverse(a):
126	  Equal.sym(String, a, String.reverse(String.reverse(a)), internal_reverse_reverse(a))
127	
128	def 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	
139	def 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.
146	law u32_cmp_refl:
147	  for x: U32
148	  {U32.cmp(x, x) == EQ{} : Cmp}
149	
150	def u32_cmp_refl(x):
151	  Equal.sym(Cmp, EQ{}, U32.cmp(x, x), internal_u32_cmp_refl(x))
152	
153	def 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.
160	law char_cmp_refl:
161	  for c: Char
162	  {Char.cmp(c, c) == ((c, c), EQ{}) : (Char & Char) & Cmp}
163	
164	def char_cmp_refl(c):
165	  Equal.sym((Char & Char) & Cmp, ((c, c), EQ{}), Char.cmp(c, c), internal_char_cmp_refl(c))
166	
167	def 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.
179	law cmp_refl:
180	  for s: String
181	  {String.cmp(s, s) == ((s, s), EQ{}) : (String & String) & Cmp}
182	
183	def 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.
187	law eq_refl:
188	  for s: String
189	  {String.eq(s, s) == True{} : Bool}
190	
191	def eq_refl(s):
192	  %internal_cmp_refl(s) : {Cmp.is_eq(Pair.snd(String & String, Cmp, _)) == True{} : Bool}
193	  {==}
194	
195	def 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	
204	def 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	
213	def 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.
227	law 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	
233	def 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.
240	law 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	
246	def 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	
252	def 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	
257	def 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	
261	def 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.
273	law 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	
279	def 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	
290	def 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.
299	law length_reverse:
300	  for s: String
301	  {String.length(String.reverse(s)) == String.length(s) : Nat}
302	
303	def 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.
308	law reverse_nil:
309	  {String.reverse(SNil{}) == SNil{} : String}
310	
311	def reverse_nil():
312	  {==}
313	
314	# Reversing a one-character string gives it back.
315	law reverse_singleton:
316	  for -c: Char
317	  {String.reverse(SCon{c, SNil{}}) == SCon{c, SNil{}} : String}
318	
319	def reverse_singleton(c):
320	  {==}
321	
322	# A string is empty exactly when its length is zero.
323	law is_empty_iff_length_eq_zero:
324	  for s: String
325	  {String.is_empty(s) == Nat.is_eq(String.length(s), 0n) : Bool}
326	
327	def 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.
335	law 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	
340	def is_empty_append(a, b):
341	  match a:
342	    case SNil{}:
343	      {==}
344	    case SCon{h, t}:
345	      {==}
346	
347	def 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.
355	law is_empty_reverse:
356	  for s: String
357	  {String.is_empty(String.reverse(s)) == String.is_empty(s) : Bool}
358	
359	def 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.
367	law 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	
372	def 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.
383	law 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	
388	def 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.
399	law 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	
404	def 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.
414	law to_list_from_list:
415	  for cs: List<&2, Char>
416	  {String.to_list(String.from_list(cs)) == cs : List<&2, Char>}
417	
418	def 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.
427	law from_list_to_list:
428	  for s: String
429	  {String.from_list(String.to_list(s)) == s : String}
430	
431	def 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.
440	law 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	
445	def 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.
454	law length_to_list:
455	  for s: String
456	  {List.length(&2, Char, String.to_list(s)) == String.length(s) : Nat}
457	
458	def 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.
469	law append_nil_sym:
470	  for a: String
471	  {a == String.append(a, SNil{}) : String}
472	
473	def 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.
477	law nil_append_sym:
478	  for -a: String
479	  {a == String.append(SNil{}, a) : String}
480	
481	def 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.
485	law 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	
491	def 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.
495	law 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	
500	def 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.
504	law 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	
509	def 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.
513	law 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	
518	def 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.
522	law reverse_reverse_sym:
523	  for a: String
524	  {a == String.reverse(String.reverse(a)) : String}
525	
526	def 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.
530	law u32_cmp_refl_sym:
531	  for x: U32
532	  {EQ{} == U32.cmp(x, x) : Cmp}
533	
534	def 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.
538	law char_cmp_refl_sym:
539	  for c: Char
540	  {((c, c), EQ{}) == Char.cmp(c, c) : (Char & Char) & Cmp}
541	
542	def 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.
546	law cmp_refl_sym:
547	  for s: String
548	  {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}
549	
550	def 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.
554	law eq_refl_sym:
555	  for s: String
556	  {True{} == String.eq(s, s) : Bool}
557	
558	def 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.
562	law length_reverse_sym:
563	  for s: String
564	  {String.length(s) == String.length(String.reverse(s)) : Nat}
565	
566	def 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.
570	law reverse_nil_sym:
571	  {SNil{} == String.reverse(SNil{}) : String}
572	
573	def 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.
577	law reverse_singleton_sym:
578	  for -c: Char
579	  {SCon{c, SNil{}} == String.reverse(SCon{c, SNil{}}) : String}
580	
581	def 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.
585	law 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	
589	def 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.
593	law 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	
598	def 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.
602	law is_empty_reverse_sym:
603	  for s: String
604	  {String.is_empty(s) == String.is_empty(String.reverse(s)) : Bool}
605	
606	def 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.
610	law 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	
615	def 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.
619	law 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	
624	def 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.
628	law 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	
633	def 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.
637	law to_list_from_list_sym:
638	  for cs: List<&2, Char>
639	  {cs == String.to_list(String.from_list(cs)) : List<&2, Char>}
640	
641	def 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.
645	law from_list_to_list_sym:
646	  for s: String
647	  {s == String.from_list(String.to_list(s)) : String}
648	
649	def 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.
653	law 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	
658	def 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.
662	law length_to_list_sym:
663	  for s: String
664	  {String.length(s) == List.length(&2, Char, String.to_list(s)) : Nat}
665	
666	def length_to_list_sym(s):
667	  Equal.sym(Nat, List.length(&2, Char, String.to_list(s)), String.length(s), length_to_list(s))