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.
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	# Base 2.0.38 defines String.order directly, not through String.cmp (PLAN F39); these prove the two agree.
187	def 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	
198	def 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	
209	def 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	
216	def 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	
225	def 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.
237	def 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	
240	def 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	
244	def 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.
249	law eq_refl:
250	  for s: String
251	  {String.eq(s, s) == True{} : Bool}
252	
253	def 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	
259	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}:
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	
268	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}:
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	
277	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)}:
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.
291	law 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	
297	def 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.
304	law 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	
310	def 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	
316	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}:
317	  match rr:
318	    case ((a, b), c):
319	      {==}
320	
321	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}:
322	  %e : {Cmp.is_eq(_) == True{} : Bool}
323	  h
324	
325	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: {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.
337	law 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	
343	def 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	
354	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}:
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.
363	law length_reverse:
364	  for s: String
365	  {String.length(String.reverse(s)) == String.length(s) : Nat}
366	
367	def 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.
372	law reverse_nil:
373	  {String.reverse(SNil{}) == SNil{} : String}
374	
375	def reverse_nil():
376	  {==}
377	
378	# Reversing a one-character string gives it back.
379	law reverse_singleton:
380	  for -c: Char
381	  {String.reverse(SCon{c, SNil{}}) == SCon{c, SNil{}} : String}
382	
383	def reverse_singleton(c):
384	  {==}
385	
386	# A string is empty exactly when its length is zero.
387	law is_empty_iff_length_eq_zero:
388	  for s: String
389	  {String.is_empty(s) == Nat.is_eq(String.length(s), 0n) : Bool}
390	
391	def 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.
399	law 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	
404	def is_empty_append(a, b):
405	  match a:
406	    case SNil{}:
407	      {==}
408	    case SCon{h, t}:
409	      {==}
410	
411	def 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.
419	law is_empty_reverse:
420	  for s: String
421	  {String.is_empty(String.reverse(s)) == String.is_empty(s) : Bool}
422	
423	def 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.
431	law 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	
436	def 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.
447	law 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	
452	def 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.
463	law 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	
468	def 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.
478	law to_list_from_list:
479	  for cs: List<&2, Char>
480	  {String.to_list(String.from_list(cs)) == cs : List<&2, Char>}
481	
482	def 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.
491	law from_list_to_list:
492	  for s: String
493	  {String.from_list(String.to_list(s)) == s : String}
494	
495	def 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.
504	law 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	
509	def 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.
518	law length_to_list:
519	  for s: String
520	  {List.length(&2, Char, String.to_list(s)) == String.length(s) : Nat}
521	
522	def 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.
533	law append_nil_sym:
534	  for a: String
535	  {a == String.append(a, SNil{}) : String}
536	
537	def 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.
541	law nil_append_sym:
542	  for -a: String
543	  {a == String.append(SNil{}, a) : String}
544	
545	def 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.
549	law 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	
555	def 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.
559	law 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	
564	def 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.
568	law 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	
573	def 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.
577	law 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	
582	def 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.
586	law reverse_reverse_sym:
587	  for a: String
588	  {a == String.reverse(String.reverse(a)) : String}
589	
590	def 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.
594	law u32_cmp_refl_sym:
595	  for x: U32
596	  {EQ{} == U32.cmp(x, x) : Cmp}
597	
598	def 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.
602	law char_cmp_refl_sym:
603	  for c: Char
604	  {((c, c), EQ{}) == Char.cmp(c, c) : (Char & Char) & Cmp}
605	
606	def 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.
610	law cmp_refl_sym:
611	  for s: String
612	  {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}
613	
614	def 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.
618	law eq_refl_sym:
619	  for s: String
620	  {True{} == String.eq(s, s) : Bool}
621	
622	def 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.
626	law length_reverse_sym:
627	  for s: String
628	  {String.length(s) == String.length(String.reverse(s)) : Nat}
629	
630	def 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.
634	law reverse_nil_sym:
635	  {SNil{} == String.reverse(SNil{}) : String}
636	
637	def 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.
641	law reverse_singleton_sym:
642	  for -c: Char
643	  {SCon{c, SNil{}} == String.reverse(SCon{c, SNil{}}) : String}
644	
645	def 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.
649	law 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	
653	def 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.
657	law 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	
662	def 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.
666	law is_empty_reverse_sym:
667	  for s: String
668	  {String.is_empty(s) == String.is_empty(String.reverse(s)) : Bool}
669	
670	def 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.
674	law 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	
679	def 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.
683	law 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	
688	def 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.
692	law 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	
697	def 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.
701	law to_list_from_list_sym:
702	  for cs: List<&2, Char>
703	  {cs == String.to_list(String.from_list(cs)) : List<&2, Char>}
704	
705	def 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.
709	law from_list_to_list_sym:
710	  for s: String
711	  {s == String.from_list(String.to_list(s)) : String}
712	
713	def 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.
717	law 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	
722	def 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.
726	law length_to_list_sym:
727	  for s: String
728	  {String.length(s) == List.length(&2, Char, String.to_list(s)) : Nat}
729	
730	def length_to_list_sym(s):
731	  Equal.sym(Nat, List.length(&2, Char, String.to_list(s)), String.length(s), length_to_list(s))