1	import Base
2	
3	# Negating a boolean twice gives it back.
4	law not_not:
5	  for b: Bool
6	  {Bool.not(Bool.not(b)) == b : Bool}
7	
8	def not_not(b):
9	  match b:
10	    case True{}:
11	      {==}
12	    case False{}:
13	      {==}
14	
15	# Boolean and is commutative.
16	law and_comm:
17	  for a: Bool
18	  for b: Bool
19	  {Bool.and(a, b) == Bool.and(b, a) : Bool}
20	
21	def and_comm(a, b):
22	  match a b:
23	    case True{} True{}:
24	      {==}
25	    case True{} False{}:
26	      {==}
27	    case False{} True{}:
28	      {==}
29	    case False{} False{}:
30	      {==}
31	
32	# Boolean or is commutative.
33	law or_comm:
34	  for a: Bool
35	  for b: Bool
36	  {Bool.or(a, b) == Bool.or(b, a) : Bool}
37	
38	def or_comm(a, b):
39	  match a b:
40	    case True{} True{}:
41	      {==}
42	    case True{} False{}:
43	      {==}
44	    case False{} True{}:
45	      {==}
46	    case False{} False{}:
47	      {==}
48	
49	# Boolean and is associative.
50	law and_assoc:
51	  for a: Bool
52	  for -b: Bool
53	  for -c: Bool
54	  {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}
55	
56	def and_assoc(a, b, c):
57	  match a:
58	    case True{}:
59	      {==}
60	    case False{}:
61	      {==}
62	
63	# Boolean or is associative.
64	law or_assoc:
65	  for a: Bool
66	  for -b: Bool
67	  for -c: Bool
68	  {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}
69	
70	def or_assoc(a, b, c):
71	  match a:
72	    case True{}:
73	      {==}
74	    case False{}:
75	      {==}
76	
77	# True is a right identity for and: a and true is a.
78	law and_true:
79	  for a: Bool
80	  {Bool.and(a, True{}) == a : Bool}
81	
82	def and_true(a):
83	  match a:
84	    case True{}:
85	      {==}
86	    case False{}:
87	      {==}
88	
89	# True is a left identity for and: true and a is a.
90	law true_and:
91	  for -a: Bool
92	  {Bool.and(True{}, a) == a : Bool}
93	
94	def true_and(a):
95	  {==}
96	
97	# False absorbs and on the right: a and false is false.
98	law and_false:
99	  for a: Bool
100	  {Bool.and(a, False{}) == False{} : Bool}
101	
102	def and_false(a):
103	  match a:
104	    case True{}:
105	      {==}
106	    case False{}:
107	      {==}
108	
109	# False absorbs and on the left: false and a is false.
110	law false_and:
111	  for -a: Bool
112	  {Bool.and(False{}, a) == False{} : Bool}
113	
114	def false_and(a):
115	  {==}
116	
117	# False is a right identity for or: a or false is a.
118	law or_false:
119	  for a: Bool
120	  {Bool.or(a, False{}) == a : Bool}
121	
122	def or_false(a):
123	  match a:
124	    case True{}:
125	      {==}
126	    case False{}:
127	      {==}
128	
129	# False is a left identity for or: false or a is a.
130	law false_or:
131	  for -a: Bool
132	  {Bool.or(False{}, a) == a : Bool}
133	
134	def false_or(a):
135	  {==}
136	
137	# True absorbs or on the right: a or true is true.
138	law or_true:
139	  for a: Bool
140	  {Bool.or(a, True{}) == True{} : Bool}
141	
142	def or_true(a):
143	  match a:
144	    case True{}:
145	      {==}
146	    case False{}:
147	      {==}
148	
149	# True absorbs or on the left: true or a is true.
150	law true_or:
151	  for -a: Bool
152	  {Bool.or(True{}, a) == True{} : Bool}
153	
154	def true_or(a):
155	  {==}
156	
157	# De Morgan: not (a and b) is (not a) or (not b).
158	law de_morgan_and:
159	  for a: Bool
160	  for -b: Bool
161	  {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}
162	
163	def de_morgan_and(a, b):
164	  match a:
165	    case True{}:
166	      {==}
167	    case False{}:
168	      {==}
169	
170	# De Morgan: not (a or b) is (not a) and (not b).
171	law de_morgan_or:
172	  for a: Bool
173	  for -b: Bool
174	  {Bool.not(Bool.or(a, b)) == Bool.and(Bool.not(a), Bool.not(b)) : Bool}
175	
176	def de_morgan_or(a, b):
177	  match a:
178	    case True{}:
179	      {==}
180	    case False{}:
181	      {==}
182	
183	def internal_true_ne_false(e: {True{} == False{} : Bool}) -> Empty:
184	  %e : Bool.pick(Type, _, Unit, Empty)
185	  Unit{}
186	
187	# True and False are different booleans.
188	law true_ne_false:
189	  {True{} != False{} : Bool}
190	
191	def true_ne_false():
192	  e => internal_true_ne_false(e)
193	
194	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
195	
196	# Negating a boolean twice gives it back, reversed to rewrite toward the simple side.
197	law not_not_sym:
198	  for b: Bool
199	  {b == Bool.not(Bool.not(b)) : Bool}
200	
201	def not_not_sym(b):
202	  Equal.sym(Bool, Bool.not(Bool.not(b)), b, not_not(b))
203	
204	# Boolean and is commutative, reversed to rewrite toward the simple side.
205	law and_comm_sym:
206	  for a: Bool
207	  for b: Bool
208	  {Bool.and(b, a) == Bool.and(a, b) : Bool}
209	
210	def and_comm_sym(a, b):
211	  Equal.sym(Bool, Bool.and(a, b), Bool.and(b, a), and_comm(a, b))
212	
213	# Boolean or is commutative, reversed to rewrite toward the simple side.
214	law or_comm_sym:
215	  for a: Bool
216	  for b: Bool
217	  {Bool.or(b, a) == Bool.or(a, b) : Bool}
218	
219	def or_comm_sym(a, b):
220	  Equal.sym(Bool, Bool.or(a, b), Bool.or(b, a), or_comm(a, b))
221	
222	# Boolean and is associative, reversed to rewrite toward the simple side.
223	law and_assoc_sym:
224	  for a: Bool
225	  for -b: Bool
226	  for -c: Bool
227	  {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}
228	
229	def and_assoc_sym(a, b, c):
230	  Equal.sym(Bool, Bool.and(Bool.and(a, b), c), Bool.and(a, Bool.and(b, c)), and_assoc(a, b, c))
231	
232	# Boolean or is associative, reversed to rewrite toward the simple side.
233	law or_assoc_sym:
234	  for a: Bool
235	  for -b: Bool
236	  for -c: Bool
237	  {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}
238	
239	def or_assoc_sym(a, b, c):
240	  Equal.sym(Bool, Bool.or(Bool.or(a, b), c), Bool.or(a, Bool.or(b, c)), or_assoc(a, b, c))
241	
242	# True is a right identity for and: a and true is a, reversed to rewrite toward the simple side.
243	law and_true_sym:
244	  for a: Bool
245	  {a == Bool.and(a, True{}) : Bool}
246	
247	def and_true_sym(a):
248	  Equal.sym(Bool, Bool.and(a, True{}), a, and_true(a))
249	
250	# True is a left identity for and: true and a is a, reversed to rewrite toward the simple side.
251	law true_and_sym:
252	  for -a: Bool
253	  {a == Bool.and(True{}, a) : Bool}
254	
255	def true_and_sym(a):
256	  Equal.sym(Bool, Bool.and(True{}, a), a, true_and(a))
257	
258	# False absorbs and on the right: a and false is false, reversed to rewrite toward the simple side.
259	law and_false_sym:
260	  for a: Bool
261	  {False{} == Bool.and(a, False{}) : Bool}
262	
263	def and_false_sym(a):
264	  Equal.sym(Bool, Bool.and(a, False{}), False{}, and_false(a))
265	
266	# False absorbs and on the left: false and a is false, reversed to rewrite toward the simple side.
267	law false_and_sym:
268	  for -a: Bool
269	  {False{} == Bool.and(False{}, a) : Bool}
270	
271	def false_and_sym(a):
272	  Equal.sym(Bool, Bool.and(False{}, a), False{}, false_and(a))
273	
274	# False is a right identity for or: a or false is a, reversed to rewrite toward the simple side.
275	law or_false_sym:
276	  for a: Bool
277	  {a == Bool.or(a, False{}) : Bool}
278	
279	def or_false_sym(a):
280	  Equal.sym(Bool, Bool.or(a, False{}), a, or_false(a))
281	
282	# False is a left identity for or: false or a is a, reversed to rewrite toward the simple side.
283	law false_or_sym:
284	  for -a: Bool
285	  {a == Bool.or(False{}, a) : Bool}
286	
287	def false_or_sym(a):
288	  Equal.sym(Bool, Bool.or(False{}, a), a, false_or(a))
289	
290	# True absorbs or on the right: a or true is true, reversed to rewrite toward the simple side.
291	law or_true_sym:
292	  for a: Bool
293	  {True{} == Bool.or(a, True{}) : Bool}
294	
295	def or_true_sym(a):
296	  Equal.sym(Bool, Bool.or(a, True{}), True{}, or_true(a))
297	
298	# True absorbs or on the left: true or a is true, reversed to rewrite toward the simple side.
299	law true_or_sym:
300	  for -a: Bool
301	  {True{} == Bool.or(True{}, a) : Bool}
302	
303	def true_or_sym(a):
304	  Equal.sym(Bool, Bool.or(True{}, a), True{}, true_or(a))
305	
306	# De Morgan: not (a and b) is (not a) or (not b), reversed to rewrite toward the simple side.
307	law de_morgan_and_sym:
308	  for a: Bool
309	  for -b: Bool
310	  {Bool.or(Bool.not(a), Bool.not(b)) == Bool.not(Bool.and(a, b)) : Bool}
311	
312	def de_morgan_and_sym(a, b):
313	  Equal.sym(Bool, Bool.not(Bool.and(a, b)), Bool.or(Bool.not(a), Bool.not(b)), de_morgan_and(a, b))
314	
315	# De Morgan: not (a or b) is (not a) and (not b), reversed to rewrite toward the simple side.
316	law de_morgan_or_sym:
317	  for a: Bool
318	  for -b: Bool
319	  {Bool.and(Bool.not(a), Bool.not(b)) == Bool.not(Bool.or(a, b)) : Bool}
320	
321	def de_morgan_or_sym(a, b):
322	  Equal.sym(Bool, Bool.not(Bool.or(a, b)), Bool.and(Bool.not(a), Bool.not(b)), de_morgan_or(a, b))