bool.bend

bend-mathlib@0.8.1.0 · 783 lines · 71 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# False and True are different booleans, the other way round.
442law false_ne_true:
443  {False{} != True{} : Bool}
444
445def false_ne_true():
446  e => internal_false_ne_true(e)
447
448# If a and b is true then a is true.
449law eq_true_of_and_left:
450  for a: Bool
451  for -b: Bool
452  for h: {Bool.and(a, b) == True{} : Bool}
453  {a == True{} : Bool}
454
455def eq_true_of_and_left(a, b, h):
456  match a:
457    case True{}:
458      {==}
459    case False{}:
460      Empty.absurd({False{} == True{} : Bool}, internal_false_ne_true(h))
461
462# If a and b is true then b is true.
463law eq_true_of_and_right:
464  for a: Bool
465  for -b: Bool
466  for h: {Bool.and(a, b) == True{} : Bool}
467  {b == True{} : Bool}
468
469def eq_true_of_and_right(a, b, h):
470  match a:
471    case True{}:
472      h
473    case False{}:
474      Empty.absurd({b == True{} : Bool}, internal_false_ne_true(h))
475
476# If a and b are both true then a and b is true.
477law and_eq_true:
478  for a: Bool
479  for -b: Bool
480  for ha: {a == True{} : Bool}
481  for hb: {b == True{} : Bool}
482  {Bool.and(a, b) == True{} : Bool}
483
484def and_eq_true(a, b, ha, hb):
485  match a:
486    case True{}:
487      hb
488    case False{}:
489      Empty.absurd({Bool.and(False{}, b) == True{} : Bool}, internal_false_ne_true(ha))
490
491# If a or b is true and b is false then a is true.
492law eq_true_of_or_eq_false_right:
493  for a: Bool
494  for -b: Bool
495  for h: {Bool.or(a, b) == True{} : Bool}
496  for hb: {b == False{} : Bool}
497  {a == True{} : Bool}
498
499def eq_true_of_or_eq_false_right(a, b, h, hb):
500  match a:
501    case True{}:
502      {==}
503    case False{}:
504      Empty.absurd({False{} == True{} : Bool}, internal_false_ne_true(Equal.trans(Bool, False{}, b, True{}, Equal.sym(Bool, b, False{}, hb), h)))
505
506# If a or b is true and a is false then b is true.
507law eq_true_of_or_eq_false_left:
508  for a: Bool
509  for -b: Bool
510  for h: {Bool.or(a, b) == True{} : Bool}
511  for ha: {a == False{} : Bool}
512  {b == True{} : Bool}
513
514def eq_true_of_or_eq_false_left(a, b, h, ha):
515  match a:
516    case True{}:
517      Empty.absurd({b == True{} : Bool}, internal_true_ne_false(ha))
518    case False{}:
519      h
520
521# If not b is true then b is false.
522law eq_false_of_not_eq_true:
523  for b: Bool
524  for h: {Bool.not(b) == True{} : Bool}
525  {b == False{} : Bool}
526
527def eq_false_of_not_eq_true(b, h):
528  match b:
529    case True{}:
530      Empty.absurd({True{} == False{} : Bool}, internal_false_ne_true(h))
531    case False{}:
532      {==}
533
534# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
535
536# Negating a boolean twice gives it back, reversed to rewrite toward the simple side.
537law not_not_sym:
538  for b: Bool
539  {b == Bool.not(Bool.not(b)) : Bool}
540
541def not_not_sym(b):
542  Equal.sym(Bool, Bool.not(Bool.not(b)), b, not_not(b))
543
544# Boolean and is commutative, reversed to rewrite toward the simple side.
545law and_comm_sym:
546  for a: Bool
547  for b: Bool
548  {Bool.and(b, a) == Bool.and(a, b) : Bool}
549
550def and_comm_sym(a, b):
551  Equal.sym(Bool, Bool.and(a, b), Bool.and(b, a), and_comm(a, b))
552
553# Boolean or is commutative, reversed to rewrite toward the simple side.
554law or_comm_sym:
555  for a: Bool
556  for b: Bool
557  {Bool.or(b, a) == Bool.or(a, b) : Bool}
558
559def or_comm_sym(a, b):
560  Equal.sym(Bool, Bool.or(a, b), Bool.or(b, a), or_comm(a, b))
561
562# Boolean and is associative, reversed to rewrite toward the simple side.
563law and_assoc_sym:
564  for a: Bool
565  for -b: Bool
566  for -c: Bool
567  {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}
568
569def and_assoc_sym(a, b, c):
570  Equal.sym(Bool, Bool.and(Bool.and(a, b), c), Bool.and(a, Bool.and(b, c)), and_assoc(a, b, c))
571
572# Boolean or is associative, reversed to rewrite toward the simple side.
573law or_assoc_sym:
574  for a: Bool
575  for -b: Bool
576  for -c: Bool
577  {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}
578
579def or_assoc_sym(a, b, c):
580  Equal.sym(Bool, Bool.or(Bool.or(a, b), c), Bool.or(a, Bool.or(b, c)), or_assoc(a, b, c))
581
582# True is a right identity for and: a and true is a, reversed to rewrite toward the simple side.
583law and_true_sym:
584  for a: Bool
585  {a == Bool.and(a, True{}) : Bool}
586
587def and_true_sym(a):
588  Equal.sym(Bool, Bool.and(a, True{}), a, and_true(a))
589
590# True is a left identity for and: true and a is a, reversed to rewrite toward the simple side.
591law true_and_sym:
592  for -a: Bool
593  {a == Bool.and(True{}, a) : Bool}
594
595def true_and_sym(a):
596  Equal.sym(Bool, Bool.and(True{}, a), a, true_and(a))
597
598# False absorbs and on the right: a and false is false, reversed to rewrite toward the simple side.
599law and_false_sym:
600  for a: Bool
601  {False{} == Bool.and(a, False{}) : Bool}
602
603def and_false_sym(a):
604  Equal.sym(Bool, Bool.and(a, False{}), False{}, and_false(a))
605
606# False absorbs and on the left: false and a is false, reversed to rewrite toward the simple side.
607law false_and_sym:
608  for -a: Bool
609  {False{} == Bool.and(False{}, a) : Bool}
610
611def false_and_sym(a):
612  Equal.sym(Bool, Bool.and(False{}, a), False{}, false_and(a))
613
614# False is a right identity for or: a or false is a, reversed to rewrite toward the simple side.
615law or_false_sym:
616  for a: Bool
617  {a == Bool.or(a, False{}) : Bool}
618
619def or_false_sym(a):
620  Equal.sym(Bool, Bool.or(a, False{}), a, or_false(a))
621
622# False is a left identity for or: false or a is a, reversed to rewrite toward the simple side.
623law false_or_sym:
624  for -a: Bool
625  {a == Bool.or(False{}, a) : Bool}
626
627def false_or_sym(a):
628  Equal.sym(Bool, Bool.or(False{}, a), a, false_or(a))
629
630# True absorbs or on the right: a or true is true, reversed to rewrite toward the simple side.
631law or_true_sym:
632  for a: Bool
633  {True{} == Bool.or(a, True{}) : Bool}
634
635def or_true_sym(a):
636  Equal.sym(Bool, Bool.or(a, True{}), True{}, or_true(a))
637
638# True absorbs or on the left: true or a is true, reversed to rewrite toward the simple side.
639law true_or_sym:
640  for -a: Bool
641  {True{} == Bool.or(True{}, a) : Bool}
642
643def true_or_sym(a):
644  Equal.sym(Bool, Bool.or(True{}, a), True{}, true_or(a))
645
646# De Morgan: not (a and b) is (not a) or (not b), reversed to rewrite toward the simple side.
647law de_morgan_and_sym:
648  for a: Bool
649  for -b: Bool
650  {Bool.or(Bool.not(a), Bool.not(b)) == Bool.not(Bool.and(a, b)) : Bool}
651
652def de_morgan_and_sym(a, b):
653  Equal.sym(Bool, Bool.not(Bool.and(a, b)), Bool.or(Bool.not(a), Bool.not(b)), de_morgan_and(a, b))
654
655# De Morgan: not (a or b) is (not a) and (not b), reversed to rewrite toward the simple side.
656law de_morgan_or_sym:
657  for a: Bool
658  for -b: Bool
659  {Bool.and(Bool.not(a), Bool.not(b)) == Bool.not(Bool.or(a, b)) : Bool}
660
661def de_morgan_or_sym(a, b):
662  Equal.sym(Bool, Bool.not(Bool.or(a, b)), Bool.and(Bool.not(a), Bool.not(b)), de_morgan_or(a, b))
663
664# And with itself: a and a is a, reversed to rewrite toward the simple side.
665law and_self_sym:
666  for a: Bool
667  {a == Bool.and(a, a) : Bool}
668
669def and_self_sym(a):
670  Equal.sym(Bool, Bool.and(a, a), a, and_self(a))
671
672# Or with itself: a or a is a, reversed to rewrite toward the simple side.
673law or_self_sym:
674  for a: Bool
675  {a == Bool.or(a, a) : Bool}
676
677def or_self_sym(a):
678  Equal.sym(Bool, Bool.or(a, a), a, or_self(a))
679
680# A boolean and its negation are never both true: a and (not a) is false, reversed to rewrite toward the simple side.
681law and_not_self_sym:
682  for a: Bool
683  {False{} == Bool.and(a, Bool.not(a)) : Bool}
684
685def and_not_self_sym(a):
686  Equal.sym(Bool, Bool.and(a, Bool.not(a)), False{}, and_not_self(a))
687
688# A boolean or its negation is always true: a or (not a) is true, reversed to rewrite toward the simple side.
689law or_not_self_sym:
690  for a: Bool
691  {True{} == Bool.or(a, Bool.not(a)) : Bool}
692
693def or_not_self_sym(a):
694  Equal.sym(Bool, Bool.or(a, Bool.not(a)), True{}, or_not_self(a))
695
696# And distributes over or: a and (b or c) is (a and b) or (a and c), reversed to rewrite toward the simple side.
697law and_or_distrib_left_sym:
698  for a: Bool
699  for -b: Bool
700  for -c: Bool
701  {Bool.or(Bool.and(a, b), Bool.and(a, c)) == Bool.and(a, Bool.or(b, c)) : Bool}
702
703def and_or_distrib_left_sym(a, b, c):
704  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))
705
706# Or distributes over and: a or (b and c) is (a or b) and (a or c), reversed to rewrite toward the simple side.
707law or_and_distrib_left_sym:
708  for a: Bool
709  for -b: Bool
710  for -c: Bool
711  {Bool.and(Bool.or(a, b), Bool.or(a, c)) == Bool.or(a, Bool.and(b, c)) : Bool}
712
713def or_and_distrib_left_sym(a, b, c):
714  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))
715
716# Absorption: a and (a or b) is a, reversed to rewrite toward the simple side.
717law and_or_absorb_sym:
718  for a: Bool
719  for -b: Bool
720  {a == Bool.and(a, Bool.or(a, b)) : Bool}
721
722def and_or_absorb_sym(a, b):
723  Equal.sym(Bool, Bool.and(a, Bool.or(a, b)), a, and_or_absorb(a, b))
724
725# Absorption: a or (a and b) is a, reversed to rewrite toward the simple side.
726law or_and_absorb_sym:
727  for a: Bool
728  for -b: Bool
729  {a == Bool.or(a, Bool.and(a, b)) : Bool}
730
731def or_and_absorb_sym(a, b):
732  Equal.sym(Bool, Bool.or(a, Bool.and(a, b)), a, or_and_absorb(a, b))
733
734# Exclusive or is commutative, reversed to rewrite toward the simple side.
735law xor_comm_sym:
736  for a: Bool
737  for b: Bool
738  {Bool.xor(b, a) == Bool.xor(a, b) : Bool}
739
740def xor_comm_sym(a, b):
741  Equal.sym(Bool, Bool.xor(a, b), Bool.xor(b, a), xor_comm(a, b))
742
743# Exclusive or is associative, reversed to rewrite toward the simple side.
744law xor_assoc_sym:
745  for a: Bool
746  for b: Bool
747  for c: Bool
748  {Bool.xor(a, Bool.xor(b, c)) == Bool.xor(Bool.xor(a, b), c) : Bool}
749
750def xor_assoc_sym(a, b, c):
751  Equal.sym(Bool, Bool.xor(Bool.xor(a, b), c), Bool.xor(a, Bool.xor(b, c)), xor_assoc(a, b, c))
752
753# A boolean xor itself is false, reversed to rewrite toward the simple side.
754law xor_self_sym:
755  for a: Bool
756  {False{} == Bool.xor(a, a) : Bool}
757
758def xor_self_sym(a):
759  Equal.sym(Bool, Bool.xor(a, a), False{}, xor_self(a))
760
761# False is an identity for xor: a xor false is a, reversed to rewrite toward the simple side.
762law xor_false_sym:
763  for a: Bool
764  {a == Bool.xor(a, False{}) : Bool}
765
766def xor_false_sym(a):
767  Equal.sym(Bool, Bool.xor(a, False{}), a, xor_false(a))
768
769# Xor with true negates: a xor true is not a, reversed to rewrite toward the simple side.
770law xor_true_sym:
771  for a: Bool
772  {Bool.not(a) == Bool.xor(a, True{}) : Bool}
773
774def xor_true_sym(a):
775  Equal.sym(Bool, Bool.xor(a, True{}), Bool.not(a), xor_true(a))
776
777# Comparing a boolean with itself gives EQ, reversed to rewrite toward the simple side.
778law cmp_refl_sym:
779  for b: Bool
780  {EQ{} == Bool.cmp(b, b) : Cmp}
781
782def cmp_refl_sym(b):
783  Equal.sym(Cmp, Bool.cmp(b, b), EQ{}, cmp_refl(b))