1	# bend-mathlib/maybe.bend: Maybe monad and map laws over &2.
2	import Base
3	
4	# Left identity: binding a pure value applies the function.
5	law maybe_pure_bind:
6	  for ~A: Data
7	  for ~B: Data
8	  for -f: A -> Maybe<&2, B>
9	  for -x: A
10	  {Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) == f(x) : Maybe<&2, B>}
11	
12	def maybe_pure_bind(A, B, f, x):
13	  {==}
14	
15	# Right identity: binding pure is the identity.
16	law maybe_bind_pure:
17	  for ~A: Data
18	  for m: Maybe<&2, A>
19	  {Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) == m : Maybe<&2, A>}
20	
21	def maybe_bind_pure(A, m):
22	  match m:
23	    case None{}:
24	      {==}
25	    case Some{x}:
26	      {==}
27	
28	# Bind is associative.
29	law maybe_bind_assoc:
30	  for ~A: Data
31	  for ~B: Data
32	  for ~C: Data
33	  for -f: A -> Maybe<&2, B>
34	  for -g: B -> Maybe<&2, C>
35	  for m: Maybe<&2, A>
36	  {Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) == Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) : Maybe<&2, C>}
37	
38	def maybe_bind_assoc(A, B, C, f, g, m):
39	  match m:
40	    case None{}:
41	      {==}
42	    case Some{x}:
43	      {==}
44	
45	# Mapping a pure value is pure of the mapped value.
46	law maybe_map_pure:
47	  for ~A: Data
48	  for ~B: Data
49	  for -f: A -> B
50	  for -x: A
51	  {Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)) == Maybe.pure(&2, B, f(x)) : Maybe<&2, B>}
52	
53	def maybe_map_pure(A, B, f, x):
54	  {==}
55	
56	# Mapping a composition maps the composition.
57	law maybe_map_compose:
58	  for ~A: Data
59	  for ~B: Data
60	  for ~C: Data
61	  for -f: A -> B
62	  for -g: B -> C
63	  for m: Maybe<&2, A>
64	  {Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) == Maybe.map(&2, A, C, x => g(f(x)), m) : Maybe<&2, C>}
65	
66	def maybe_map_compose(A, B, C, f, g, m):
67	  match m:
68	    case None{}:
69	      {==}
70	    case Some{x}:
71	      {==}
72	
73	# Mapping the identity gives the value back.
74	law maybe_map_id:
75	  for ~A: Data
76	  for m: Maybe<&2, A>
77	  {Maybe.map(&2, A, A, x => x, m) == m : Maybe<&2, A>}
78	
79	def maybe_map_id(A, m):
80	  match m:
81	    case None{}:
82	      {==}
83	    case Some{x}:
84	      {==}
85	
86	# Binding a function that always fails gives None.
87	law maybe_bind_none:
88	  for ~A: Data
89	  for ~B: Data
90	  for m: Maybe<&2, A>
91	  {Maybe.bind(&2, A, B, m, x => None{}) == None{} : Maybe<&2, B>}
92	
93	def maybe_bind_none(A, B, m):
94	  match m:
95	    case None{}:
96	      {==}
97	    case Some{x}:
98	      {==}
99	
100	# Mapping is binding the function followed by pure.
101	law maybe_map_eq_bind:
102	  for ~A: Data
103	  for ~B: Data
104	  for ~f: A -> B
105	  for m: Maybe<&2, A>
106	  {Maybe.map(&2, A, B, f, m) == Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))) : Maybe<&2, B>}
107	
108	def maybe_map_eq_bind(A, B, f, m):
109	  match m:
110	    case None{}:
111	      {==}
112	    case Some{x}:
113	      {==}
114	
115	# Mapping keeps whether a value is present.
116	law maybe_is_some_map:
117	  for ~A: Data
118	  for ~B: Data
119	  for ~f: A -> B
120	  for m: Maybe<&2, A>
121	  {Maybe.is_some(&2, B, Maybe.map(&2, A, B, f, m)) == Maybe.is_some(&2, A, m) : Bool}
122	
123	def maybe_is_some_map(A, B, f, m):
124	  match m:
125	    case None{}:
126	      {==}
127	    case Some{x}:
128	      {==}
129	
130	# Mapping keeps whether a value is absent.
131	law maybe_is_none_map:
132	  for ~A: Data
133	  for ~B: Data
134	  for ~f: A -> B
135	  for m: Maybe<&2, A>
136	  {Maybe.is_none(&2, B, Maybe.map(&2, A, B, f, m)) == Maybe.is_none(&2, A, m) : Bool}
137	
138	def maybe_is_none_map(A, B, f, m):
139	  match m:
140	    case None{}:
141	      {==}
142	    case Some{x}:
143	      {==}
144	
145	# The default of a map, with the mapped default, is the mapped default of the original.
146	law maybe_default_map:
147	  for ~A: Data
148	  for ~B: Data
149	  for ~f: A -> B
150	  for m: Maybe<&2, A>
151	  for -d: A
152	  {Maybe.default(&2, B, Maybe.map(&2, A, B, f, m), f(d)) == f(Maybe.default(&2, A, m, d)) : B}
153	
154	def maybe_default_map(A, B, f, m, d):
155	  match m:
156	    case None{}:
157	      {==}
158	    case Some{x}:
159	      {==}
160	
161	# None is a right identity for or.
162	law maybe_or_none:
163	  for ~A: Data
164	  for m: Maybe<&2, A>
165	  {Maybe.or(&2, A, m, None{}) == m : Maybe<&2, A>}
166	
167	def maybe_or_none(A, m):
168	  match m:
169	    case None{}:
170	      {==}
171	    case Some{x}:
172	      {==}
173	
174	# Or is associative.
175	law maybe_or_assoc:
176	  for ~A: Data
177	  for m: Maybe<&2, A>
178	  for -n: Maybe<&2, A>
179	  for -k: Maybe<&2, A>
180	  {Maybe.or(&2, A, Maybe.or(&2, A, m, n), k) == Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)) : Maybe<&2, A>}
181	
182	def maybe_or_assoc(A, m, n, k):
183	  match m:
184	    case None{}:
185	      {==}
186	    case Some{x}:
187	      {==}
188	
189	# Binding after a map binds the composition.
190	law maybe_bind_map:
191	  for ~A: Data
192	  for ~B: Data
193	  for ~C: Data
194	  for ~f: A -> B
195	  for ~g: B -> Maybe<&2, C>
196	  for m: Maybe<&2, A>
197	  {Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g) == Maybe.bind(&2, A, C, m, x => g(f(x))) : Maybe<&2, C>}
198	
199	def maybe_bind_map(A, B, C, f, g, m):
200	  match m:
201	    case None{}:
202	      {==}
203	    case Some{x}:
204	      {==}
205	
206	# Mapping after a bind maps inside the bound function.
207	law maybe_map_bind:
208	  for ~A: Data
209	  for ~B: Data
210	  for ~C: Data
211	  for ~f: A -> Maybe<&2, B>
212	  for ~g: B -> C
213	  for m: Maybe<&2, A>
214	  {Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)) == Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))) : Maybe<&2, C>}
215	
216	def maybe_map_bind(A, B, C, f, g, m):
217	  match m:
218	    case None{}:
219	      {==}
220	    case Some{x}:
221	      {==}
222	
223	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
224	
225	# Left identity: binding a pure value applies the function, reversed to rewrite toward the simple side.
226	law maybe_pure_bind_sym:
227	  for ~A: Data
228	  for ~B: Data
229	  for -f: A -> Maybe<&2, B>
230	  for -x: A
231	  {f(x) == Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) : Maybe<&2, B>}
232	
233	def maybe_pure_bind_sym(A, B, f, x):
234	  Equal.sym(Maybe<&2, B>, Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f), f(x), maybe_pure_bind(~A, ~B, f, x))
235	
236	# Right identity: binding pure is the identity, reversed to rewrite toward the simple side.
237	law maybe_bind_pure_sym:
238	  for ~A: Data
239	  for m: Maybe<&2, A>
240	  {m == Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) : Maybe<&2, A>}
241	
242	def maybe_bind_pure_sym(A, m):
243	  Equal.sym(Maybe<&2, A>, Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)), m, maybe_bind_pure(~A, m))
244	
245	# Bind is associative, reversed to rewrite toward the simple side.
246	law maybe_bind_assoc_sym:
247	  for ~A: Data
248	  for ~B: Data
249	  for ~C: Data
250	  for -f: A -> Maybe<&2, B>
251	  for -g: B -> Maybe<&2, C>
252	  for m: Maybe<&2, A>
253	  {Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) == Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) : Maybe<&2, C>}
254	
255	def maybe_bind_assoc_sym(A, B, C, f, g, m):
256	  Equal.sym(Maybe<&2, C>, Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g), Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)), maybe_bind_assoc(~A, ~B, ~C, f, g, m))
257	
258	# Mapping a pure value is pure of the mapped value, reversed to rewrite toward the simple side.
259	law maybe_map_pure_sym:
260	  for ~A: Data
261	  for ~B: Data
262	  for -f: A -> B
263	  for -x: A
264	  {Maybe.pure(&2, B, f(x)) == Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)) : Maybe<&2, B>}
265	
266	def maybe_map_pure_sym(A, B, f, x):
267	  Equal.sym(Maybe<&2, B>, Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)), Maybe.pure(&2, B, f(x)), maybe_map_pure(~A, ~B, f, x))
268	
269	# Mapping a composition maps the composition, reversed to rewrite toward the simple side.
270	law maybe_map_compose_sym:
271	  for ~A: Data
272	  for ~B: Data
273	  for ~C: Data
274	  for -f: A -> B
275	  for -g: B -> C
276	  for m: Maybe<&2, A>
277	  {Maybe.map(&2, A, C, x => g(f(x)), m) == Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) : Maybe<&2, C>}
278	
279	def maybe_map_compose_sym(A, B, C, f, g, m):
280	  Equal.sym(Maybe<&2, C>, Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)), Maybe.map(&2, A, C, x => g(f(x)), m), maybe_map_compose(~A, ~B, ~C, f, g, m))
281	
282	# Mapping the identity gives the value back, reversed to rewrite toward the simple side.
283	law maybe_map_id_sym:
284	  for ~A: Data
285	  for m: Maybe<&2, A>
286	  {m == Maybe.map(&2, A, A, x => x, m) : Maybe<&2, A>}
287	
288	def maybe_map_id_sym(A, m):
289	  Equal.sym(Maybe<&2, A>, Maybe.map(&2, A, A, x => x, m), m, maybe_map_id(~A, m))
290	
291	# Binding a function that always fails gives None, reversed to rewrite toward the simple side.
292	law maybe_bind_none_sym:
293	  for ~A: Data
294	  for ~B: Data
295	  for m: Maybe<&2, A>
296	  {None{} == Maybe.bind(&2, A, B, m, x => None{}) : Maybe<&2, B>}
297	
298	def maybe_bind_none_sym(A, B, m):
299	  Equal.sym(Maybe<&2, B>, Maybe.bind(&2, A, B, m, x => None{}), None{}, maybe_bind_none(~A, ~B, m))
300	
301	# Mapping is binding the function followed by pure, reversed to rewrite toward the simple side.
302	law maybe_map_eq_bind_sym:
303	  for ~A: Data
304	  for ~B: Data
305	  for ~f: A -> B
306	  for m: Maybe<&2, A>
307	  {Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))) == Maybe.map(&2, A, B, f, m) : Maybe<&2, B>}
308	
309	def maybe_map_eq_bind_sym(A, B, f, m):
310	  Equal.sym(Maybe<&2, B>, Maybe.map(&2, A, B, f, m), Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))), maybe_map_eq_bind(~A, ~B, ~f, m))
311	
312	# Mapping keeps whether a value is present, reversed to rewrite toward the simple side.
313	law maybe_is_some_map_sym:
314	  for ~A: Data
315	  for ~B: Data
316	  for ~f: A -> B
317	  for m: Maybe<&2, A>
318	  {Maybe.is_some(&2, A, m) == Maybe.is_some(&2, B, Maybe.map(&2, A, B, f, m)) : Bool}
319	
320	def maybe_is_some_map_sym(A, B, f, m):
321	  Equal.sym(Bool, Maybe.is_some(&2, B, Maybe.map(&2, A, B, f, m)), Maybe.is_some(&2, A, m), maybe_is_some_map(~A, ~B, ~f, m))
322	
323	# Mapping keeps whether a value is absent, reversed to rewrite toward the simple side.
324	law maybe_is_none_map_sym:
325	  for ~A: Data
326	  for ~B: Data
327	  for ~f: A -> B
328	  for m: Maybe<&2, A>
329	  {Maybe.is_none(&2, A, m) == Maybe.is_none(&2, B, Maybe.map(&2, A, B, f, m)) : Bool}
330	
331	def maybe_is_none_map_sym(A, B, f, m):
332	  Equal.sym(Bool, Maybe.is_none(&2, B, Maybe.map(&2, A, B, f, m)), Maybe.is_none(&2, A, m), maybe_is_none_map(~A, ~B, ~f, m))
333	
334	# The default of a map, with the mapped default, is the mapped default of the original, reversed to rewrite toward the simple side.
335	law maybe_default_map_sym:
336	  for ~A: Data
337	  for ~B: Data
338	  for ~f: A -> B
339	  for m: Maybe<&2, A>
340	  for -d: A
341	  {f(Maybe.default(&2, A, m, d)) == Maybe.default(&2, B, Maybe.map(&2, A, B, f, m), f(d)) : B}
342	
343	def maybe_default_map_sym(A, B, f, m, d):
344	  Equal.sym(B, Maybe.default(&2, B, Maybe.map(&2, A, B, f, m), f(d)), f(Maybe.default(&2, A, m, d)), maybe_default_map(~A, ~B, ~f, m, d))
345	
346	# None is a right identity for or, reversed to rewrite toward the simple side.
347	law maybe_or_none_sym:
348	  for ~A: Data
349	  for m: Maybe<&2, A>
350	  {m == Maybe.or(&2, A, m, None{}) : Maybe<&2, A>}
351	
352	def maybe_or_none_sym(A, m):
353	  Equal.sym(Maybe<&2, A>, Maybe.or(&2, A, m, None{}), m, maybe_or_none(~A, m))
354	
355	# Or is associative, reversed to rewrite toward the simple side.
356	law maybe_or_assoc_sym:
357	  for ~A: Data
358	  for m: Maybe<&2, A>
359	  for -n: Maybe<&2, A>
360	  for -k: Maybe<&2, A>
361	  {Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)) == Maybe.or(&2, A, Maybe.or(&2, A, m, n), k) : Maybe<&2, A>}
362	
363	def maybe_or_assoc_sym(A, m, n, k):
364	  Equal.sym(Maybe<&2, A>, Maybe.or(&2, A, Maybe.or(&2, A, m, n), k), Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)), maybe_or_assoc(~A, m, n, k))
365	
366	# Binding after a map binds the composition, reversed to rewrite toward the simple side.
367	law maybe_bind_map_sym:
368	  for ~A: Data
369	  for ~B: Data
370	  for ~C: Data
371	  for ~f: A -> B
372	  for ~g: B -> Maybe<&2, C>
373	  for m: Maybe<&2, A>
374	  {Maybe.bind(&2, A, C, m, x => g(f(x))) == Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g) : Maybe<&2, C>}
375	
376	def maybe_bind_map_sym(A, B, C, f, g, m):
377	  Equal.sym(Maybe<&2, C>, Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g), Maybe.bind(&2, A, C, m, x => g(f(x))), maybe_bind_map(~A, ~B, ~C, ~f, ~g, m))
378	
379	# Mapping after a bind maps inside the bound function, reversed to rewrite toward the simple side.
380	law maybe_map_bind_sym:
381	  for ~A: Data
382	  for ~B: Data
383	  for ~C: Data
384	  for ~f: A -> Maybe<&2, B>
385	  for ~g: B -> C
386	  for m: Maybe<&2, A>
387	  {Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))) == Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)) : Maybe<&2, C>}
388	
389	def maybe_map_bind_sym(A, B, C, f, g, m):
390	  Equal.sym(Maybe<&2, C>, Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)), Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))), maybe_map_bind(~A, ~B, ~C, ~f, ~g, m))