~/bend-docscommunity

bool.bend checks

raw source on the hub · import bend-mathlib@0.6.0.0/bool.bend as MBool

bend-mathlib/bool.bend: Bool algebra (not, and, or, xor).

1 import
import Base

Laws

law not_not provedsource · line 5 · raw

@b:Bool -> {Bool.not(Bool.not(b)) == b : Bool}

Negating a boolean twice gives it back.

law and_comm provedsource · line 17 · raw

@a:Bool -> @b:Bool -> {Bool.and(a, b) == Bool.and(b, a) : Bool}

Boolean and is commutative.

law or_comm provedsource · line 34 · raw

@a:Bool -> @b:Bool -> {Bool.or(a, b) == Bool.or(b, a) : Bool}

Boolean or is commutative.

law and_assoc provedsource · line 51 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}

Boolean and is associative.

law or_assoc provedsource · line 65 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}

Boolean or is associative.

law and_true provedsource · line 79 · raw

@a:Bool -> {Bool.and(a, True{}) == a : Bool}

True is a right identity for and: a and true is a.

law true_and provedsource · line 91 · raw

@-a:Bool -> {Bool.and(True{}, a) == a : Bool}

True is a left identity for and: true and a is a.

law and_false provedsource · line 99 · raw

@a:Bool -> {Bool.and(a, False{}) == False{} : Bool}

False absorbs and on the right: a and false is false.

law false_and provedsource · line 111 · raw

@-a:Bool -> {Bool.and(False{}, a) == False{} : Bool}

False absorbs and on the left: false and a is false.

law or_false provedsource · line 119 · raw

@a:Bool -> {Bool.or(a, False{}) == a : Bool}

False is a right identity for or: a or false is a.

law false_or provedsource · line 131 · raw

@-a:Bool -> {Bool.or(False{}, a) == a : Bool}

False is a left identity for or: false or a is a.

law or_true provedsource · line 139 · raw

@a:Bool -> {Bool.or(a, True{}) == True{} : Bool}

True absorbs or on the right: a or true is true.

law true_or provedsource · line 151 · raw

@-a:Bool -> {Bool.or(True{}, a) == True{} : Bool}

True absorbs or on the left: true or a is true.

law de_morgan_and provedsource · line 159 · raw

@a:Bool -> @-b:Bool -> {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}

De Morgan: not (a and b) is (not a) or (not b).

law de_morgan_or provedsource · line 172 · raw

@a:Bool -> @-b:Bool -> {Bool.not(Bool.or(a, b)) == Bool.and(Bool.not(a), Bool.not(b)) : Bool}

De Morgan: not (a or b) is (not a) and (not b).

law true_ne_false provedsource · line 189 · raw

@_:{True{} == False{} : Bool} -> Empty

True and False are different booleans.

law and_self provedsource · line 196 · raw

@a:Bool -> {Bool.and(a, a) == a : Bool}

And with itself: a and a is a.

law or_self provedsource · line 208 · raw

@a:Bool -> {Bool.or(a, a) == a : Bool}

Or with itself: a or a is a.

law and_not_self provedsource · line 220 · raw

@a:Bool -> {Bool.and(a, Bool.not(a)) == False{} : Bool}

A boolean and its negation are never both true: a and (not a) is false.

law or_not_self provedsource · line 232 · raw

@a:Bool -> {Bool.or(a, Bool.not(a)) == True{} : Bool}

A boolean or its negation is always true: a or (not a) is true.

law and_or_distrib_left provedsource · line 244 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.and(a, Bool.or(b, c)) == Bool.or(Bool.and(a, b), Bool.and(a, c)) : Bool}

And distributes over or: a and (b or c) is (a and b) or (a and c).

law or_and_distrib_left provedsource · line 258 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.or(a, Bool.and(b, c)) == Bool.and(Bool.or(a, b), Bool.or(a, c)) : Bool}

Or distributes over and: a or (b and c) is (a or b) and (a or c).

law and_or_absorb provedsource · line 272 · raw

@a:Bool -> @-b:Bool -> {Bool.and(a, Bool.or(a, b)) == a : Bool}

Absorption: a and (a or b) is a.

law or_and_absorb provedsource · line 285 · raw

@a:Bool -> @-b:Bool -> {Bool.or(a, Bool.and(a, b)) == a : Bool}

Absorption: a or (a and b) is a.

law xor_comm provedsource · line 298 · raw

@a:Bool -> @b:Bool -> {Bool.xor(a, b) == Bool.xor(b, a) : Bool}

Exclusive or is commutative.

law xor_assoc provedsource · line 315 · raw

@a:Bool -> @b:Bool -> @c:Bool -> {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}

Exclusive or is associative.

law xor_self provedsource · line 341 · raw

@a:Bool -> {Bool.xor(a, a) == False{} : Bool}

A boolean xor itself is false.

law xor_false provedsource · line 353 · raw

@a:Bool -> {Bool.xor(a, False{}) == a : Bool}

False is an identity for xor: a xor false is a.

law xor_true provedsource · line 365 · raw

@a:Bool -> {Bool.xor(a, True{}) == Bool.not(a) : Bool}

Xor with true negates: a xor true is not a.

law not_inj provedsource · line 377 · raw

@a:Bool -> @b:Bool -> @h:{Bool.not(a) == Bool.not(b) : Bool} -> {a == b : Bool}

Negation is injective: not a = not b implies a = b.

law eq_true_of_ne_false provedsource · line 395 · raw

@a:Bool -> @h:(@_:{a == False{} : Bool} -> Empty) -> {a == True{} : Bool}

A boolean that is not false is true.

law cmp_refl provedsource · line 412 · raw

@b:Bool -> {Bool.cmp(b, b) == EQ{} : Cmp}

Comparing a boolean with itself gives EQ.

law eq_of_cmp_eq provedsource · line 424 · raw

@a:Bool -> @b:Bool -> @h:{Cmp.is_eq(Bool.cmp(a, b)) == True{} : Bool} -> {a == b : Bool}

Two booleans that compare EQ are equal.

law false_ne_true provedsource · line 442 · raw

@_:{False{} == True{} : Bool} -> Empty

False and True are different booleans, the other way round.

law eq_true_of_and_left provedsource · line 449 · raw

@a:Bool -> @-b:Bool -> @h:{Bool.and(a, b) == True{} : Bool} -> {a == True{} : Bool}

If a and b is true then a is true.

law eq_true_of_and_right provedsource · line 463 · raw

@a:Bool -> @-b:Bool -> @h:{Bool.and(a, b) == True{} : Bool} -> {b == True{} : Bool}

If a and b is true then b is true.

law and_eq_true provedsource · line 477 · raw

@a:Bool -> @-b:Bool -> @ha:{a == True{} : Bool} -> @hb:{b == True{} : Bool} -> {Bool.and(a, b) == True{} : Bool}

If a and b are both true then a and b is true.

law eq_true_of_or_eq_false_right provedsource · line 492 · raw

@a:Bool -> @-b:Bool -> @h:{Bool.or(a, b) == True{} : Bool} -> @hb:{b == False{} : Bool} -> {a == True{} : Bool}

If a or b is true and b is false then a is true.

law eq_true_of_or_eq_false_left provedsource · line 507 · raw

@a:Bool -> @-b:Bool -> @h:{Bool.or(a, b) == True{} : Bool} -> @ha:{a == False{} : Bool} -> {b == True{} : Bool}

If a or b is true and a is false then b is true.

law eq_false_of_not_eq_true provedsource · line 522 · raw

@b:Bool -> @h:{Bool.not(b) == True{} : Bool} -> {b == False{} : Bool}

If not b is true then b is false.

law not_not_sym provedsource · line 537 · raw

@b:Bool -> {b == Bool.not(Bool.not(b)) : Bool}

Negating a boolean twice gives it back, reversed to rewrite toward the simple side.

law and_comm_sym provedsource · line 545 · raw

@a:Bool -> @b:Bool -> {Bool.and(b, a) == Bool.and(a, b) : Bool}

Boolean and is commutative, reversed to rewrite toward the simple side.

law or_comm_sym provedsource · line 554 · raw

@a:Bool -> @b:Bool -> {Bool.or(b, a) == Bool.or(a, b) : Bool}

Boolean or is commutative, reversed to rewrite toward the simple side.

law and_assoc_sym provedsource · line 563 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}

Boolean and is associative, reversed to rewrite toward the simple side.

law or_assoc_sym provedsource · line 573 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}

Boolean or is associative, reversed to rewrite toward the simple side.

law and_true_sym provedsource · line 583 · raw

@a:Bool -> {a == Bool.and(a, True{}) : Bool}

True is a right identity for and: a and true is a, reversed to rewrite toward the simple side.

law true_and_sym provedsource · line 591 · raw

@-a:Bool -> {a == Bool.and(True{}, a) : Bool}

True is a left identity for and: true and a is a, reversed to rewrite toward the simple side.

law and_false_sym provedsource · line 599 · raw

@a:Bool -> {False{} == Bool.and(a, False{}) : Bool}

False absorbs and on the right: a and false is false, reversed to rewrite toward the simple side.

law false_and_sym provedsource · line 607 · raw

@-a:Bool -> {False{} == Bool.and(False{}, a) : Bool}

False absorbs and on the left: false and a is false, reversed to rewrite toward the simple side.

law or_false_sym provedsource · line 615 · raw

@a:Bool -> {a == Bool.or(a, False{}) : Bool}

False is a right identity for or: a or false is a, reversed to rewrite toward the simple side.

law false_or_sym provedsource · line 623 · raw

@-a:Bool -> {a == Bool.or(False{}, a) : Bool}

False is a left identity for or: false or a is a, reversed to rewrite toward the simple side.

law or_true_sym provedsource · line 631 · raw

@a:Bool -> {True{} == Bool.or(a, True{}) : Bool}

True absorbs or on the right: a or true is true, reversed to rewrite toward the simple side.

law true_or_sym provedsource · line 639 · raw

@-a:Bool -> {True{} == Bool.or(True{}, a) : Bool}

True absorbs or on the left: true or a is true, reversed to rewrite toward the simple side.

law de_morgan_and_sym provedsource · line 647 · raw

@a:Bool -> @-b:Bool -> {Bool.or(Bool.not(a), Bool.not(b)) == Bool.not(Bool.and(a, b)) : Bool}

De Morgan: not (a and b) is (not a) or (not b), reversed to rewrite toward the simple side.

law de_morgan_or_sym provedsource · line 656 · raw

@a:Bool -> @-b:Bool -> {Bool.and(Bool.not(a), Bool.not(b)) == Bool.not(Bool.or(a, b)) : Bool}

De Morgan: not (a or b) is (not a) and (not b), reversed to rewrite toward the simple side.

law and_self_sym provedsource · line 665 · raw

@a:Bool -> {a == Bool.and(a, a) : Bool}

And with itself: a and a is a, reversed to rewrite toward the simple side.

law or_self_sym provedsource · line 673 · raw

@a:Bool -> {a == Bool.or(a, a) : Bool}

Or with itself: a or a is a, reversed to rewrite toward the simple side.

law and_not_self_sym provedsource · line 681 · raw

@a:Bool -> {False{} == Bool.and(a, Bool.not(a)) : Bool}

A boolean and its negation are never both true: a and (not a) is false, reversed to rewrite toward the simple side.

law or_not_self_sym provedsource · line 689 · raw

@a:Bool -> {True{} == Bool.or(a, Bool.not(a)) : Bool}

A boolean or its negation is always true: a or (not a) is true, reversed to rewrite toward the simple side.

law and_or_distrib_left_sym provedsource · line 697 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.or(Bool.and(a, b), Bool.and(a, c)) == Bool.and(a, Bool.or(b, c)) : Bool}

And distributes over or: a and (b or c) is (a and b) or (a and c), reversed to rewrite toward the simple side.

law or_and_distrib_left_sym provedsource · line 707 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.and(Bool.or(a, b), Bool.or(a, c)) == Bool.or(a, Bool.and(b, c)) : Bool}

Or distributes over and: a or (b and c) is (a or b) and (a or c), reversed to rewrite toward the simple side.

law and_or_absorb_sym provedsource · line 717 · raw

@a:Bool -> @-b:Bool -> {a == Bool.and(a, Bool.or(a, b)) : Bool}

Absorption: a and (a or b) is a, reversed to rewrite toward the simple side.

law or_and_absorb_sym provedsource · line 726 · raw

@a:Bool -> @-b:Bool -> {a == Bool.or(a, Bool.and(a, b)) : Bool}

Absorption: a or (a and b) is a, reversed to rewrite toward the simple side.

law xor_comm_sym provedsource · line 735 · raw

@a:Bool -> @b:Bool -> {Bool.xor(b, a) == Bool.xor(a, b) : Bool}

Exclusive or is commutative, reversed to rewrite toward the simple side.

law xor_assoc_sym provedsource · line 744 · raw

@a:Bool -> @b:Bool -> @c:Bool -> {Bool.xor(a, Bool.xor(b, c)) == Bool.xor(Bool.xor(a, b), c) : Bool}

Exclusive or is associative, reversed to rewrite toward the simple side.

law xor_self_sym provedsource · line 754 · raw

@a:Bool -> {False{} == Bool.xor(a, a) : Bool}

A boolean xor itself is false, reversed to rewrite toward the simple side.

law xor_false_sym provedsource · line 762 · raw

@a:Bool -> {a == Bool.xor(a, False{}) : Bool}

False is an identity for xor: a xor false is a, reversed to rewrite toward the simple side.

law xor_true_sym provedsource · line 770 · raw

@a:Bool -> {Bool.not(a) == Bool.xor(a, True{}) : Bool}

Xor with true negates: a xor true is not a, reversed to rewrite toward the simple side.

law cmp_refl_sym provedsource · line 778 · raw

@b:Bool -> {EQ{} == Bool.cmp(b, b) : Cmp}

Comparing a boolean with itself gives EQ, reversed to rewrite toward the simple side.

Definitions

def internal_true_ne_false source · line 184 · raw

@e:{True{} == False{} : Bool} -> Empty

def internal_false_ne_true source · line 407 · raw

@e:{False{} == True{} : Bool} -> Empty