~/bend-docscommunity

bool.bend checks

raw source on the hub · import bend-mathlib@0.2.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 not_not_sym provedsource · line 410 · 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 418 · 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 427 · 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 436 · 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 446 · 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 456 · 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 464 · 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 472 · 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 480 · 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 488 · 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 496 · 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 504 · 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 512 · 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 520 · 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 529 · 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 538 · 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 546 · 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 554 · 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 562 · 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 570 · 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 580 · 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 590 · 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 599 · 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 608 · 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 617 · 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 627 · 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 635 · 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 643 · 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.

Definitions

def internal_true_ne_false source · line 184 · raw

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