bool.bend
bend-mathlib@0.4.0.0 · 690 lines · 0 definitions
1# bend-mathlib/bool.bend: Bool algebra (not, and, or, xor).
2import Base
3
4# Negating a boolean twice gives it back.
5law not_not:
6 for b: Bool
7 {Bool.not(Bool.not(b)) == b : Bool}
8
9def not_not(b):
10 match b:
11 case True{}:
12 {==}
13 case False{}:
14 {==}
15
16# Boolean and is commutative.
17law and_comm:
18 for a: Bool
19 for b: Bool
20 {Bool.and(a, b) == Bool.and(b, a) : Bool}
21
22def and_comm(a, b):
23 match a b:
24 case True{} True{}:
25 {==}
26 case True{} False{}:
27 {==}
28 case False{} True{}:
29 {==}
30 case False{} False{}:
31 {==}
32
33# Boolean or is commutative.
34law or_comm:
35 for a: Bool
36 for b: Bool
37 {Bool.or(a, b) == Bool.or(b, a) : Bool}
38
39def or_comm(a, b):
40 match a b:
41 case True{} True{}:
42 {==}
43 case True{} False{}:
44 {==}
45 case False{} True{}:
46 {==}
47 case False{} False{}:
48 {==}
49
50# Boolean and is associative.
51law and_assoc:
52 for a: Bool
53 for -b: Bool
54 for -c: Bool
55 {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}
56
57def and_assoc(a, b, c):
58 match a:
59 case True{}:
60 {==}
61 case False{}:
62 {==}
63
64# Boolean or is associative.
65law or_assoc:
66 for a: Bool
67 for -b: Bool
68 for -c: Bool
69 {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}
70
71def or_assoc(a, b, c):
72 match a:
73 case True{}:
74 {==}
75 case False{}:
76 {==}
77
78# True is a right identity for and: a and true is a.
79law and_true:
80 for a: Bool
81 {Bool.and(a, True{}) == a : Bool}
82
83def and_true(a):
84 match a:
85 case True{}:
86 {==}
87 case False{}:
88 {==}
89
90# True is a left identity for and: true and a is a.
91law true_and:
92 for -a: Bool
93 {Bool.and(True{}, a) == a : Bool}
94
95def true_and(a):
96 {==}
97
98# False absorbs and on the right: a and false is false.
99law and_false:
100 for a: Bool
101 {Bool.and(a, False{}) == False{} : Bool}
102
103def and_false(a):
104 match a:
105 case True{}:
106 {==}
107 case False{}:
108 {==}
109
110# False absorbs and on the left: false and a is false.
111law false_and:
112 for -a: Bool
113 {Bool.and(False{}, a) == False{} : Bool}
114
115def false_and(a):
116 {==}
117
118# False is a right identity for or: a or false is a.
119law or_false:
120 for a: Bool
121 {Bool.or(a, False{}) == a : Bool}
122
123def or_false(a):
124 match a:
125 case True{}:
126 {==}
127 case False{}:
128 {==}
129
130# False is a left identity for or: false or a is a.
131law false_or:
132 for -a: Bool
133 {Bool.or(False{}, a) == a : Bool}
134
135def false_or(a):
136 {==}
137
138# True absorbs or on the right: a or true is true.
139law or_true:
140 for a: Bool
141 {Bool.or(a, True{}) == True{} : Bool}
142
143def or_true(a):
144 match a:
145 case True{}:
146 {==}
147 case False{}:
148 {==}
149
150# True absorbs or on the left: true or a is true.
151law true_or:
152 for -a: Bool
153 {Bool.or(True{}, a) == True{} : Bool}
154
155def true_or(a):
156 {==}
157
158# De Morgan: not (a and b) is (not a) or (not b).
159law de_morgan_and:
160 for a: Bool
161 for -b: Bool
162 {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}
163
164def de_morgan_and(a, b):
165 match a:
166 case True{}:
167 {==}
168 case False{}:
169 {==}
170
171# De Morgan: not (a or b) is (not a) and (not b).
172law de_morgan_or:
173 for a: Bool
174 for -b: Bool
175 {Bool.not(Bool.or(a, b)) == Bool.and(Bool.not(a), Bool.not(b)) : Bool}
176
177def de_morgan_or(a, b):
178 match a:
179 case True{}:
180 {==}
181 case False{}:
182 {==}
183
184def internal_true_ne_false(e: {True{} == False{} : Bool}) -> Empty:
185 %e : Bool.pick(Type, _, Unit, Empty)
186 Unit{}
187
188# True and False are different booleans.
189law true_ne_false:
190 {True{} != False{} : Bool}
191
192def true_ne_false():
193 e => internal_true_ne_false(e)
194
195# And with itself: a and a is a.
196law and_self:
197 for a: Bool
198 {Bool.and(a, a) == a : Bool}
199
200def and_self(a):
201 match a:
202 case True{}:
203 {==}
204 case False{}:
205 {==}
206
207# Or with itself: a or a is a.
208law or_self:
209 for a: Bool
210 {Bool.or(a, a) == a : Bool}
211
212def or_self(a):
213 match a:
214 case True{}:
215 {==}
216 case False{}:
217 {==}
218
219# A boolean and its negation are never both true: a and (not a) is false.
220law and_not_self:
221 for a: Bool
222 {Bool.and(a, Bool.not(a)) == False{} : Bool}
223
224def and_not_self(a):
225 match a:
226 case True{}:
227 {==}
228 case False{}:
229 {==}
230
231# A boolean or its negation is always true: a or (not a) is true.
232law or_not_self:
233 for a: Bool
234 {Bool.or(a, Bool.not(a)) == True{} : Bool}
235
236def or_not_self(a):
237 match a:
238 case True{}:
239 {==}
240 case False{}:
241 {==}
242
243# And distributes over or: a and (b or c) is (a and b) or (a and c).
244law and_or_distrib_left:
245 for a: Bool
246 for -b: Bool
247 for -c: Bool
248 {Bool.and(a, Bool.or(b, c)) == Bool.or(Bool.and(a, b), Bool.and(a, c)) : Bool}
249
250def and_or_distrib_left(a, b, c):
251 match a:
252 case True{}:
253 {==}
254 case False{}:
255 {==}
256
257# Or distributes over and: a or (b and c) is (a or b) and (a or c).
258law or_and_distrib_left:
259 for a: Bool
260 for -b: Bool
261 for -c: Bool
262 {Bool.or(a, Bool.and(b, c)) == Bool.and(Bool.or(a, b), Bool.or(a, c)) : Bool}
263
264def or_and_distrib_left(a, b, c):
265 match a:
266 case True{}:
267 {==}
268 case False{}:
269 {==}
270
271# Absorption: a and (a or b) is a.
272law and_or_absorb:
273 for a: Bool
274 for -b: Bool
275 {Bool.and(a, Bool.or(a, b)) == a : Bool}
276
277def and_or_absorb(a, b):
278 match a:
279 case True{}:
280 {==}
281 case False{}:
282 {==}
283
284# Absorption: a or (a and b) is a.
285law or_and_absorb:
286 for a: Bool
287 for -b: Bool
288 {Bool.or(a, Bool.and(a, b)) == a : Bool}
289
290def or_and_absorb(a, b):
291 match a:
292 case True{}:
293 {==}
294 case False{}:
295 {==}
296
297# Exclusive or is commutative.
298law xor_comm:
299 for a: Bool
300 for b: Bool
301 {Bool.xor(a, b) == Bool.xor(b, a) : Bool}
302
303def xor_comm(a, b):
304 match a b:
305 case True{} True{}:
306 {==}
307 case True{} False{}:
308 {==}
309 case False{} True{}:
310 {==}
311 case False{} False{}:
312 {==}
313
314# Exclusive or is associative.
315law xor_assoc:
316 for a: Bool
317 for b: Bool
318 for c: Bool
319 {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}
320
321def xor_assoc(a, b, c):
322 match a b c:
323 case True{} True{} True{}:
324 {==}
325 case True{} True{} False{}:
326 {==}
327 case True{} False{} True{}:
328 {==}
329 case True{} False{} False{}:
330 {==}
331 case False{} True{} True{}:
332 {==}
333 case False{} True{} False{}:
334 {==}
335 case False{} False{} True{}:
336 {==}
337 case False{} False{} False{}:
338 {==}
339
340# A boolean xor itself is false.
341law xor_self:
342 for a: Bool
343 {Bool.xor(a, a) == False{} : Bool}
344
345def xor_self(a):
346 match a:
347 case True{}:
348 {==}
349 case False{}:
350 {==}
351
352# False is an identity for xor: a xor false is a.
353law xor_false:
354 for a: Bool
355 {Bool.xor(a, False{}) == a : Bool}
356
357def xor_false(a):
358 match a:
359 case True{}:
360 {==}
361 case False{}:
362 {==}
363
364# Xor with true negates: a xor true is not a.
365law xor_true:
366 for a: Bool
367 {Bool.xor(a, True{}) == Bool.not(a) : Bool}
368
369def xor_true(a):
370 match a:
371 case True{}:
372 {==}
373 case False{}:
374 {==}
375
376# Negation is injective: not a = not b implies a = b.
377law not_inj:
378 for a: Bool
379 for b: Bool
380 for h: {Bool.not(a) == Bool.not(b) : Bool}
381 {a == b : Bool}
382
383def not_inj(a, b, h):
384 match a b:
385 case True{} True{}:
386 {==}
387 case True{} False{}:
388 Empty.absurd({True{} == False{} : Bool}, internal_true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
389 case False{} True{}:
390 Empty.absurd({False{} == True{} : Bool}, internal_true_ne_false(h))
391 case False{} False{}:
392 {==}
393
394# A boolean that is not false is true.
395law eq_true_of_ne_false:
396 for a: Bool
397 for h: {a == False{} : Bool} -> Empty
398 {a == True{} : Bool}
399
400def eq_true_of_ne_false(a, h):
401 match a:
402 case True{}:
403 {==}
404 case False{}:
405 Empty.absurd({False{} == True{} : Bool}, h({==}))
406
407def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
408 %e : Bool.pick(Type, _, Empty, Unit)
409 Unit{}
410
411# Comparing a boolean with itself gives EQ.
412law cmp_refl:
413 for b: Bool
414 {Bool.cmp(b, b) == EQ{} : Cmp}
415
416def cmp_refl(b):
417 match b:
418 case True{}:
419 {==}
420 case False{}:
421 {==}
422
423# Two booleans that compare EQ are equal.
424law eq_of_cmp_eq:
425 for a: Bool
426 for b: Bool
427 for h: {Cmp.is_eq(Bool.cmp(a, b)) == True{} : Bool}
428 {a == b : Bool}
429
430def eq_of_cmp_eq(a, b, h):
431 match a b:
432 case True{} True{}:
433 {==}
434 case False{} False{}:
435 {==}
436 case True{} False{}:
437 Empty.absurd({True{} == False{} : Bool}, internal_false_ne_true(h))
438 case False{} True{}:
439 Empty.absurd({False{} == True{} : Bool}, internal_false_ne_true(h))
440
441# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
442
443# Negating a boolean twice gives it back, reversed to rewrite toward the simple side.
444law not_not_sym:
445 for b: Bool
446 {b == Bool.not(Bool.not(b)) : Bool}
447
448def not_not_sym(b):
449 Equal.sym(Bool, Bool.not(Bool.not(b)), b, not_not(b))
450
451# Boolean and is commutative, reversed to rewrite toward the simple side.
452law and_comm_sym:
453 for a: Bool
454 for b: Bool
455 {Bool.and(b, a) == Bool.and(a, b) : Bool}
456
457def and_comm_sym(a, b):
458 Equal.sym(Bool, Bool.and(a, b), Bool.and(b, a), and_comm(a, b))
459
460# Boolean or is commutative, reversed to rewrite toward the simple side.
461law or_comm_sym:
462 for a: Bool
463 for b: Bool
464 {Bool.or(b, a) == Bool.or(a, b) : Bool}
465
466def or_comm_sym(a, b):
467 Equal.sym(Bool, Bool.or(a, b), Bool.or(b, a), or_comm(a, b))
468
469# Boolean and is associative, reversed to rewrite toward the simple side.
470law and_assoc_sym:
471 for a: Bool
472 for -b: Bool
473 for -c: Bool
474 {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}
475
476def and_assoc_sym(a, b, c):
477 Equal.sym(Bool, Bool.and(Bool.and(a, b), c), Bool.and(a, Bool.and(b, c)), and_assoc(a, b, c))
478
479# Boolean or is associative, reversed to rewrite toward the simple side.
480law or_assoc_sym:
481 for a: Bool
482 for -b: Bool
483 for -c: Bool
484 {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}
485
486def or_assoc_sym(a, b, c):
487 Equal.sym(Bool, Bool.or(Bool.or(a, b), c), Bool.or(a, Bool.or(b, c)), or_assoc(a, b, c))
488
489# True is a right identity for and: a and true is a, reversed to rewrite toward the simple side.
490law and_true_sym:
491 for a: Bool
492 {a == Bool.and(a, True{}) : Bool}
493
494def and_true_sym(a):
495 Equal.sym(Bool, Bool.and(a, True{}), a, and_true(a))
496
497# True is a left identity for and: true and a is a, reversed to rewrite toward the simple side.
498law true_and_sym:
499 for -a: Bool
500 {a == Bool.and(True{}, a) : Bool}
501
502def true_and_sym(a):
503 Equal.sym(Bool, Bool.and(True{}, a), a, true_and(a))
504
505# False absorbs and on the right: a and false is false, reversed to rewrite toward the simple side.
506law and_false_sym:
507 for a: Bool
508 {False{} == Bool.and(a, False{}) : Bool}
509
510def and_false_sym(a):
511 Equal.sym(Bool, Bool.and(a, False{}), False{}, and_false(a))
512
513# False absorbs and on the left: false and a is false, reversed to rewrite toward the simple side.
514law false_and_sym:
515 for -a: Bool
516 {False{} == Bool.and(False{}, a) : Bool}
517
518def false_and_sym(a):
519 Equal.sym(Bool, Bool.and(False{}, a), False{}, false_and(a))
520
521# False is a right identity for or: a or false is a, reversed to rewrite toward the simple side.
522law or_false_sym:
523 for a: Bool
524 {a == Bool.or(a, False{}) : Bool}
525
526def or_false_sym(a):
527 Equal.sym(Bool, Bool.or(a, False{}), a, or_false(a))
528
529# False is a left identity for or: false or a is a, reversed to rewrite toward the simple side.
530law false_or_sym:
531 for -a: Bool
532 {a == Bool.or(False{}, a) : Bool}
533
534def false_or_sym(a):
535 Equal.sym(Bool, Bool.or(False{}, a), a, false_or(a))
536
537# True absorbs or on the right: a or true is true, reversed to rewrite toward the simple side.
538law or_true_sym:
539 for a: Bool
540 {True{} == Bool.or(a, True{}) : Bool}
541
542def or_true_sym(a):
543 Equal.sym(Bool, Bool.or(a, True{}), True{}, or_true(a))
544
545# True absorbs or on the left: true or a is true, reversed to rewrite toward the simple side.
546law true_or_sym:
547 for -a: Bool
548 {True{} == Bool.or(True{}, a) : Bool}
549
550def true_or_sym(a):
551 Equal.sym(Bool, Bool.or(True{}, a), True{}, true_or(a))
552
553# De Morgan: not (a and b) is (not a) or (not b), reversed to rewrite toward the simple side.
554law de_morgan_and_sym:
555 for a: Bool
556 for -b: Bool
557 {Bool.or(Bool.not(a), Bool.not(b)) == Bool.not(Bool.and(a, b)) : Bool}
558
559def de_morgan_and_sym(a, b):
560 Equal.sym(Bool, Bool.not(Bool.and(a, b)), Bool.or(Bool.not(a), Bool.not(b)), de_morgan_and(a, b))
561
562# De Morgan: not (a or b) is (not a) and (not b), reversed to rewrite toward the simple side.
563law de_morgan_or_sym:
564 for a: Bool
565 for -b: Bool
566 {Bool.and(Bool.not(a), Bool.not(b)) == Bool.not(Bool.or(a, b)) : Bool}
567
568def de_morgan_or_sym(a, b):
569 Equal.sym(Bool, Bool.not(Bool.or(a, b)), Bool.and(Bool.not(a), Bool.not(b)), de_morgan_or(a, b))
570
571# And with itself: a and a is a, reversed to rewrite toward the simple side.
572law and_self_sym:
573 for a: Bool
574 {a == Bool.and(a, a) : Bool}
575
576def and_self_sym(a):
577 Equal.sym(Bool, Bool.and(a, a), a, and_self(a))
578
579# Or with itself: a or a is a, reversed to rewrite toward the simple side.
580law or_self_sym:
581 for a: Bool
582 {a == Bool.or(a, a) : Bool}
583
584def or_self_sym(a):
585 Equal.sym(Bool, Bool.or(a, a), a, or_self(a))
586
587# A boolean and its negation are never both true: a and (not a) is false, reversed to rewrite toward the simple side.
588law and_not_self_sym:
589 for a: Bool
590 {False{} == Bool.and(a, Bool.not(a)) : Bool}
591
592def and_not_self_sym(a):
593 Equal.sym(Bool, Bool.and(a, Bool.not(a)), False{}, and_not_self(a))
594
595# A boolean or its negation is always true: a or (not a) is true, reversed to rewrite toward the simple side.
596law or_not_self_sym:
597 for a: Bool
598 {True{} == Bool.or(a, Bool.not(a)) : Bool}
599
600def or_not_self_sym(a):
601 Equal.sym(Bool, Bool.or(a, Bool.not(a)), True{}, or_not_self(a))
602
603# And distributes over or: a and (b or c) is (a and b) or (a and c), reversed to rewrite toward the simple side.
604law and_or_distrib_left_sym:
605 for a: Bool
606 for -b: Bool
607 for -c: Bool
608 {Bool.or(Bool.and(a, b), Bool.and(a, c)) == Bool.and(a, Bool.or(b, c)) : Bool}
609
610def and_or_distrib_left_sym(a, b, c):
611 Equal.sym(Bool, Bool.and(a, Bool.or(b, c)), Bool.or(Bool.and(a, b), Bool.and(a, c)), and_or_distrib_left(a, b, c))
612
613# Or distributes over and: a or (b and c) is (a or b) and (a or c), reversed to rewrite toward the simple side.
614law or_and_distrib_left_sym:
615 for a: Bool
616 for -b: Bool
617 for -c: Bool
618 {Bool.and(Bool.or(a, b), Bool.or(a, c)) == Bool.or(a, Bool.and(b, c)) : Bool}
619
620def or_and_distrib_left_sym(a, b, c):
621 Equal.sym(Bool, Bool.or(a, Bool.and(b, c)), Bool.and(Bool.or(a, b), Bool.or(a, c)), or_and_distrib_left(a, b, c))
622
623# Absorption: a and (a or b) is a, reversed to rewrite toward the simple side.
624law and_or_absorb_sym:
625 for a: Bool
626 for -b: Bool
627 {a == Bool.and(a, Bool.or(a, b)) : Bool}
628
629def and_or_absorb_sym(a, b):
630 Equal.sym(Bool, Bool.and(a, Bool.or(a, b)), a, and_or_absorb(a, b))
631
632# Absorption: a or (a and b) is a, reversed to rewrite toward the simple side.
633law or_and_absorb_sym:
634 for a: Bool
635 for -b: Bool
636 {a == Bool.or(a, Bool.and(a, b)) : Bool}
637
638def or_and_absorb_sym(a, b):
639 Equal.sym(Bool, Bool.or(a, Bool.and(a, b)), a, or_and_absorb(a, b))
640
641# Exclusive or is commutative, reversed to rewrite toward the simple side.
642law xor_comm_sym:
643 for a: Bool
644 for b: Bool
645 {Bool.xor(b, a) == Bool.xor(a, b) : Bool}
646
647def xor_comm_sym(a, b):
648 Equal.sym(Bool, Bool.xor(a, b), Bool.xor(b, a), xor_comm(a, b))
649
650# Exclusive or is associative, reversed to rewrite toward the simple side.
651law xor_assoc_sym:
652 for a: Bool
653 for b: Bool
654 for c: Bool
655 {Bool.xor(a, Bool.xor(b, c)) == Bool.xor(Bool.xor(a, b), c) : Bool}
656
657def xor_assoc_sym(a, b, c):
658 Equal.sym(Bool, Bool.xor(Bool.xor(a, b), c), Bool.xor(a, Bool.xor(b, c)), xor_assoc(a, b, c))
659
660# A boolean xor itself is false, reversed to rewrite toward the simple side.
661law xor_self_sym:
662 for a: Bool
663 {False{} == Bool.xor(a, a) : Bool}
664
665def xor_self_sym(a):
666 Equal.sym(Bool, Bool.xor(a, a), False{}, xor_self(a))
667
668# False is an identity for xor: a xor false is a, reversed to rewrite toward the simple side.
669law xor_false_sym:
670 for a: Bool
671 {a == Bool.xor(a, False{}) : Bool}
672
673def xor_false_sym(a):
674 Equal.sym(Bool, Bool.xor(a, False{}), a, xor_false(a))
675
676# Xor with true negates: a xor true is not a, reversed to rewrite toward the simple side.
677law xor_true_sym:
678 for a: Bool
679 {Bool.not(a) == Bool.xor(a, True{}) : Bool}
680
681def xor_true_sym(a):
682 Equal.sym(Bool, Bool.xor(a, True{}), Bool.not(a), xor_true(a))
683
684# Comparing a boolean with itself gives EQ, reversed to rewrite toward the simple side.
685law cmp_refl_sym:
686 for b: Bool
687 {EQ{} == Bool.cmp(b, b) : Cmp}
688
689def cmp_refl_sym(b):
690 Equal.sym(Cmp, Bool.cmp(b, b), EQ{}, cmp_refl(b))