bool.bend
bend-mathlib@0.1.0.1 · 322 lines · 0 definitions
1import Base
2
3# Negating a boolean twice gives it back.
4law not_not:
5 for b: Bool
6 {Bool.not(Bool.not(b)) == b : Bool}
7
8def not_not(b):
9 match b:
10 case True{}:
11 {==}
12 case False{}:
13 {==}
14
15# Boolean and is commutative.
16law and_comm:
17 for a: Bool
18 for b: Bool
19 {Bool.and(a, b) == Bool.and(b, a) : Bool}
20
21def 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.
33law or_comm:
34 for a: Bool
35 for b: Bool
36 {Bool.or(a, b) == Bool.or(b, a) : Bool}
37
38def 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.
50law 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
56def and_assoc(a, b, c):
57 match a:
58 case True{}:
59 {==}
60 case False{}:
61 {==}
62
63# Boolean or is associative.
64law 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
70def 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.
78law and_true:
79 for a: Bool
80 {Bool.and(a, True{}) == a : Bool}
81
82def 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.
90law true_and:
91 for -a: Bool
92 {Bool.and(True{}, a) == a : Bool}
93
94def true_and(a):
95 {==}
96
97# False absorbs and on the right: a and false is false.
98law and_false:
99 for a: Bool
100 {Bool.and(a, False{}) == False{} : Bool}
101
102def 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.
110law false_and:
111 for -a: Bool
112 {Bool.and(False{}, a) == False{} : Bool}
113
114def false_and(a):
115 {==}
116
117# False is a right identity for or: a or false is a.
118law or_false:
119 for a: Bool
120 {Bool.or(a, False{}) == a : Bool}
121
122def 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.
130law false_or:
131 for -a: Bool
132 {Bool.or(False{}, a) == a : Bool}
133
134def false_or(a):
135 {==}
136
137# True absorbs or on the right: a or true is true.
138law or_true:
139 for a: Bool
140 {Bool.or(a, True{}) == True{} : Bool}
141
142def 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.
150law true_or:
151 for -a: Bool
152 {Bool.or(True{}, a) == True{} : Bool}
153
154def true_or(a):
155 {==}
156
157# De Morgan: not (a and b) is (not a) or (not b).
158law 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
163def 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).
171law 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
176def de_morgan_or(a, b):
177 match a:
178 case True{}:
179 {==}
180 case False{}:
181 {==}
182
183def 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.
188law true_ne_false:
189 {True{} != False{} : Bool}
190
191def 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.
197law not_not_sym:
198 for b: Bool
199 {b == Bool.not(Bool.not(b)) : Bool}
200
201def 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.
205law and_comm_sym:
206 for a: Bool
207 for b: Bool
208 {Bool.and(b, a) == Bool.and(a, b) : Bool}
209
210def 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.
214law or_comm_sym:
215 for a: Bool
216 for b: Bool
217 {Bool.or(b, a) == Bool.or(a, b) : Bool}
218
219def 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.
223law 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
229def 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.
233law 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
239def 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.
243law and_true_sym:
244 for a: Bool
245 {a == Bool.and(a, True{}) : Bool}
246
247def 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.
251law true_and_sym:
252 for -a: Bool
253 {a == Bool.and(True{}, a) : Bool}
254
255def 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.
259law and_false_sym:
260 for a: Bool
261 {False{} == Bool.and(a, False{}) : Bool}
262
263def 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.
267law false_and_sym:
268 for -a: Bool
269 {False{} == Bool.and(False{}, a) : Bool}
270
271def 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.
275law or_false_sym:
276 for a: Bool
277 {a == Bool.or(a, False{}) : Bool}
278
279def 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.
283law false_or_sym:
284 for -a: Bool
285 {a == Bool.or(False{}, a) : Bool}
286
287def 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.
291law or_true_sym:
292 for a: Bool
293 {True{} == Bool.or(a, True{}) : Bool}
294
295def 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.
299law true_or_sym:
300 for -a: Bool
301 {True{} == Bool.or(True{}, a) : Bool}
302
303def 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.
307law 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
312def 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.
316law 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
321def 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))