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