bool

Bool.notNot

def notNot (b : Bool) : not (not b) = b

Double negation: negating a boolean twice gives it back.

Bool.andTrueR

def andTrueR (b : Bool) : and b true = b

true is a right identity for and.

Bool.orFalseR

def orFalseR (b : Bool) : or b false = b

false is a right identity for or.

Bool.andFalseR

def andFalseR (b : Bool) : and b false = false

false is right-absorbing for and: and b false is false.

Bool.andFalseL

def andFalseL (b : Bool) : and false b = false

false is left-absorbing for and: and false b is false.

Bool.orTrueR

def orTrueR (b : Bool) : or b true = true

true is right-absorbing for or: or b true is true.

Bool.orTrueL

def orTrueL (b : Bool) : or true b = true

true is left-absorbing for or: or true b is true.

Bool.deMorganAnd

def deMorganAnd (a : Bool) (b : Bool) : not (and a b) = or (not a) (not b)

De Morgan’s law: not (a and b) = (not a) or (not b).

Bool.deMorganOr

def deMorganOr (a : Bool) (b : Bool) : not (or a b) = and (not a) (not b)

De Morgan’s law: not (a or b) = (not a) and (not b).

Bool.andIdem

def andIdem (b : Bool) : and b b = b

and is idempotent: and b b is b.

Bool.orIdem

def orIdem (b : Bool) : or b b = b

or is idempotent: or b b is b.

Bool.ite

def ite {A : Type} (cond : Bool) (then_val : A) (else_val : A) : A

If-then-else: returns the first value when the condition is true, otherwise the second.

Bool.iteTrue

def iteTrue {A : Type} (x : A) (y : A) : ite true x y = x

ite with a true condition returns the then-branch.

Bool.iteFalse

def iteFalse {A : Type} (x : A) (y : A) : ite false x y = y

ite with a false condition returns the else-branch.

Bool.trueNeqFalse

def trueNeqFalse : Not (true = false)

The constructors true and false are distinct, proved by encode-decode.

Bool.falseNeqTrue

def falseNeqTrue : Not (false = true)

The constructors false and true are distinct, proved by encode-decode.

Bool.boolDecEq

def boolDecEq : DecEq Bool

Decidable equality on Bool, by case analysis on both arguments.

Bool.xorFalseR

def xorFalseR (a : Bool) : xor a false = a

false is a right identity for xor.

Bool.xorTrueR

def xorTrueR (a : Bool) : xor a true = not a

xor with true on the right negates: xor a true is not a.

Bool.andOrAbsorb

def andOrAbsorb (a : Bool) (b : Bool) : and a (or a b) = a

Absorption law: a and (a or b) = a.

Bool.orAndAbsorb

def orAndAbsorb (a : Bool) (b : Bool) : or a (and a b) = a

Absorption law: a or (a and b) = a.

Bool.andDistribOr

def andDistribOr (a : Bool) (b : Bool) (c : Bool) : and a (or b c) = or (and a b) (and a c)

and distributes over or on the left.

Bool.orDistribAnd

def orDistribAnd (a : Bool) (b : Bool) (c : Bool) : or a (and b c) = and (or a b) (or a c)

or distributes over and on the left.

Bool.boolEq

def boolEq (a : Bool) (b : Bool) : Bool

Boolean equality test: true exactly when both arguments are equal.

Bool.boolEqRefl

def boolEqRefl (a : Bool) : boolEq a a = true

boolEq is reflexive: every boolean equals itself.

Bool.boolEqComm

def boolEqComm (a : Bool) (b : Bool) : boolEq a b = boolEq b a

boolEq is symmetric in its arguments.

Bool.xorAssoc

def xorAssoc (a : Bool) (b : Bool) (c : Bool) : xor a (xor b c) = xor (xor a b) c

xor is associative.

Bool.boolRec

def boolRec (C : Type) (ct : C) (cf : C) (b : Bool) : C

Non-dependent recursor for Bool: picks the first value for true, the second for false.

Bool.boolRecTrue

def boolRecTrue (C : Type) (ct : C) (cf : C) : boolRec C ct cf true = ct

boolRec computes to its true case on true.

Bool.boolRecFalse

def boolRecFalse (C : Type) (ct : C) (cf : C) : boolRec C ct cf false = cf

boolRec computes to its false case on false.

Bool.xorNotL

def xorNotL (a : Bool) (b : Bool) : xor (not a) b = not (xor a b)

Negating the left argument of xor negates the result.

Bool.xorNotR

def xorNotR (a : Bool) (b : Bool) : xor a (not b) = not (xor a b)

Negating the right argument of xor negates the result.

Bool.nand

def nand (a : Bool) (b : Bool) : Bool

Boolean NAND: the negation of and.

Bool.nor

def nor (a : Bool) (b : Bool) : Bool

Boolean NOR: the negation of or.

Bool.iff

def iff (a : Bool) (b : Bool) : Bool

Boolean biconditional: true when each argument implies the other.

Bool.impliesTrue

def impliesTrue (a : Bool) : implies a true = true

Anything implies true.

Bool.impliesSelf

def impliesSelf (a : Bool) : implies a a = true

Every boolean implies itself.

Bool.boolCases

def boolCases (b : Bool) : or (boolEq b true) (boolEq b false) = true

Every boolean is either true or false, stated as a boolean test.

Bool.xorNeqBoolEq

def xorNeqBoolEq (a : Bool) (b : Bool) : xor a b = not (boolEq a b)

xor is the negation of boolean equality.

Bool.andDistribXor

def andDistribXor (a : Bool) (b : Bool) (c : Bool) : and a (xor b c) = xor (and a b) (and a c)

and distributes over xor on the left.

Bool.nandComm

def nandComm (a : Bool) (b : Bool) : nand a b = nand b a

nand is commutative.

Bool.norComm

def norComm (a : Bool) (b : Bool) : nor a b = nor b a

nor is commutative.

Bool.impliesAsOr

def impliesAsOr (a : Bool) (b : Bool) : implies a b = or (not a) b

Boolean implication unfolds definitionally to (not a) or b.

Bool.iffRefl

def iffRefl (a : Bool) : iff a a = true

iff is reflexive: every boolean is equivalent to itself.

Bool.iffComm

def iffComm (a : Bool) (b : Bool) : iff a b = iff b a

iff is symmetric in its arguments.

Bool.majority

def majority (a : Bool) (b : Bool) (c : Bool) : Bool

Majority vote of three booleans: true when at least two of them are true.

Bool.cond

def cond {A : Type} (b : Bool) (x : A) (y : A) : A

Conditional expression: the first value when the boolean is true, otherwise the second.

Bool.boolToNat

def boolToNat (b : Bool) : Nat

Converts a boolean to a natural number: true to 1 and false to 0.

Bool.condTrueId

def condTrueId {A : Type} (x : A) (y : A) : cond true x y = x

cond with true returns its first value.

Bool.condFalseId

def condFalseId {A : Type} (x : A) (y : A) : cond false x y = y

cond with false returns its second value.

Bool.condSame

def condSame {A : Type} (b : Bool) (x : A) : cond b x x = x

cond with identical branches returns that value regardless of the condition.

Bool.all3

def all3 (a : Bool) (b : Bool) (c : Bool) : Bool

true when all three booleans are true.

Bool.any3

def any3 (a : Bool) (b : Bool) (c : Bool) : Bool

true when at least one of three booleans is true.

Bool.countTrue3

def countTrue3 (a : Bool) (b : Bool) (c : Bool) : Nat

Counts how many of three booleans are true.

Bool.allTrue

def allTrue (xs : List Bool) : Bool

true when every boolean in the list is true (the empty list gives true).

Bool.anyTrue

def anyTrue (xs : List Bool) : Bool

true when some boolean in the list is true (the empty list gives false).

Bool.allTrueConsTrue

def allTrueConsTrue (xs : List Bool) : allTrue (cons true xs) = allTrue xs

Prepending true does not change allTrue.

Bool.anyTrueConsFalse

def anyTrueConsFalse (xs : List Bool) : anyTrue (cons false xs) = anyTrue xs

Prepending false does not change anyTrue.

Bool.allTrueConsFalse

def allTrueConsFalse (xs : List Bool) : allTrue (cons false xs) = false

A list starting with false has allTrue equal to false.

Bool.anyTrueConsTrue

def anyTrueConsTrue (xs : List Bool) : anyTrue (cons true xs) = true

A list starting with true has anyTrue equal to true.

Bool.andComplement

def andComplement (a : Bool) : and a (not a) = false

Complement law: a and (not a) = false.

Bool.orComplement

def orComplement (a : Bool) : or a (not a) = true

Complement law: a or (not a) = true.

Bool.andComplementL

def andComplementL (a : Bool) : and (not a) a = false

Complement law with the negation on the left: (not a) and a = false.

Bool.orComplementL

def orComplementL (a : Bool) : or (not a) a = true

Complement law with the negation on the left: (not a) or a = true.

Bool.eqBool

def eqBool (a : Bool) (b : Bool) : Bool

Boolean equality test: true exactly when both arguments are equal (same as boolEq).

Bool.eqBoolRefl

def eqBoolRefl (a : Bool) : eqBool a a = true

eqBool is reflexive: every boolean equals itself.

Bool.eqBoolComm

def eqBoolComm (a : Bool) (b : Bool) : eqBool a b = eqBool b a

eqBool is symmetric in its arguments.

Bool.eqBoolNotNot

def eqBoolNotNot (a : Bool) (b : Bool) : eqBool (not a) (not b) = eqBool a b

Negating both arguments does not change eqBool.

Bool.xorIsNotEqBool

def xorIsNotEqBool (a : Bool) (b : Bool) : xor a b = not (eqBool a b)

xor is the negation of eqBool.

Bool.xorCancel

def xorCancel (a : Bool) (b : Bool) : xor a (xor a b) = b

xor with the same value twice cancels: a xor (a xor b) = b.

Bool.xorCancelR

def xorCancelR (a : Bool) (b : Bool) : xor (xor a b) b = a

xor with the same value twice cancels on the right: (a xor b) xor b = a.

Bool.xorFalseL

def xorFalseL (b : Bool) : xor false b = b

false is a left identity for xor.

Bool.xorTrueL

def xorTrueL (b : Bool) : xor true b = not b

xor with true on the left negates: xor true b is not b.

Bool.xorNotNot

def xorNotNot (a : Bool) (b : Bool) : xor (not a) (not b) = xor a b

Negating both arguments does not change xor.

Bool.boolMeet

def boolMeet (a : Bool) (b : Bool) : Bool

Lattice meet on Bool, which is and.

Bool.boolJoin

def boolJoin (a : Bool) (b : Bool) : Bool

Lattice join on Bool, which is or.

Bool.boolTop

def boolTop : Bool

Top element of the boolean lattice, true.

Bool.boolBot

def boolBot : Bool

Bottom element of the boolean lattice, false.

Bool.boolMeetComm

def boolMeetComm (a : Bool) (b : Bool) : boolMeet a b = boolMeet b a

Lattice meet on Bool is commutative.

Bool.boolJoinComm

def boolJoinComm (a : Bool) (b : Bool) : boolJoin a b = boolJoin b a

Lattice join on Bool is commutative.

Bool.boolMeetAssoc

def boolMeetAssoc (a : Bool) (b : Bool) (c : Bool) : boolMeet a (boolMeet b c) = boolMeet (boolMeet a b) c

Lattice meet on Bool is associative.

Bool.boolJoinAssoc

def boolJoinAssoc (a : Bool) (b : Bool) (c : Bool) : boolJoin a (boolJoin b c) = boolJoin (boolJoin a b) c

Lattice join on Bool is associative.

Bool.boolMeetTop

def boolMeetTop (a : Bool) : boolMeet a boolTop = a

Top is an identity for meet.

Bool.boolMeetBot

def boolMeetBot (a : Bool) : boolMeet a boolBot = boolBot

Bottom is absorbing for meet.

Bool.boolJoinBot

def boolJoinBot (a : Bool) : boolJoin a boolBot = a

Bottom is an identity for join.

Bool.boolJoinTop

def boolJoinTop (a : Bool) : boolJoin a boolTop = boolTop

Top is absorbing for join.

Bool.boolMeetIdem

def boolMeetIdem (a : Bool) : boolMeet a a = a

Lattice meet on Bool is idempotent.

Bool.boolJoinIdem

def boolJoinIdem (a : Bool) : boolJoin a a = a

Lattice join on Bool is idempotent.

Bool.boolMeetAbsorb

def boolMeetAbsorb (a : Bool) (b : Bool) : boolMeet a (boolJoin a b) = a

Lattice absorption: meet a (join a b) = a.

Bool.boolJoinAbsorb

def boolJoinAbsorb (a : Bool) (b : Bool) : boolJoin a (boolMeet a b) = a

Lattice absorption: join a (meet a b) = a.

Bool.nandSelf

def nandSelf (a : Bool) : nand a a = not a

nand of a value with itself is its negation.

Bool.norSelf

def norSelf (a : Bool) : nor a a = not a

nor of a value with itself is its negation.

Bool.nandTrueL

def nandTrueL (b : Bool) : nand true b = not b

nand true b is not b.

Bool.nandFalseL

def nandFalseL (b : Bool) : nand false b = true

nand false b is true.

Bool.norFalseL

def norFalseL (b : Bool) : nor false b = not b

nor false b is not b.

Bool.norTrueL

def norTrueL (b : Bool) : nor true b = false

nor true b is false.

Bool.nandTrueR

def nandTrueR (a : Bool) : nand a true = not a

nand a true is not a.

Bool.nandFalseR

def nandFalseR (a : Bool) : nand a false = true

nand a false is true.

Bool.norFalseR

def norFalseR (a : Bool) : nor a false = not a

nor a false is not a.

Bool.norTrueR

def norTrueR (a : Bool) : nor a true = false

nor a true is false.

Bool.doubleNand

def doubleNand (a : Bool) (b : Bool) : nand (nand a b) (nand a b) = and a b

and expressed with NAND alone: nand (nand a b) (nand a b) = a and b.

Bool.notInjective

def notInjective (a : Bool) (b : Bool) (p : not a = not b) : a = b

not is injective: equal negations imply equal booleans.

Bool.iteSame

def iteSame {A : Type} (b : Bool) (x : A) : ite b x x = x

ite with identical branches returns that value regardless of the condition.

Bool.iteIsCond

def iteIsCond {A : Type} (b : Bool) (x : A) (y : A) : ite b x y = cond b x y

ite and cond compute the same result.

Bool.iteNot

def iteNot {A : Type} (b : Bool) (x : A) (y : A) : ite (not b) x y = ite b y x

Negating the condition of ite swaps its branches.

Bool.notAndTrue

def notAndTrue (a : Bool) : not (and a true) = not a

not (a and true) = not a.

Bool.notAndFalse

def notAndFalse (a : Bool) : not (and a false) = true

not (a and false) = true.

Bool.notOrTrue

def notOrTrue (a : Bool) : not (or a true) = false

not (a or true) = false.

Bool.notOrFalse

def notOrFalse (a : Bool) : not (or a false) = not a

not (a or false) = not a.

Bool.meetDistribXor

def meetDistribXor (a : Bool) (b : Bool) (c : Bool) : boolMeet a (xor b c) = xor (boolMeet a b) (boolMeet a c)

Lattice meet on Bool distributes over xor.

Bool.nandAsDeMorgan

def nandAsDeMorgan (a : Bool) (b : Bool) : nand a b = or (not a) (not b)

nand equals (not a) or (not b), by De Morgan.

Bool.norAsDeMorgan

def norAsDeMorgan (a : Bool) (b : Bool) : nor a b = and (not a) (not b)

nor equals (not a) and (not b), by De Morgan.

Bool.impliesFalseL

def impliesFalseL (b : Bool) : implies false b = true

false implies anything.

Bool.iffIsEqBool

def iffIsEqBool (a : Bool) (b : Bool) : iff a b = eqBool a b

iff agrees with eqBool.

Bool.boolToNatAnd

def boolToNatAnd (a : Bool) (b : Bool) : boolToNat (and a b) = boolToNat (ite a b false)

boolToNat of and a b equals boolToNat of ite a b false.

Bool.boolToNatNotNot

def boolToNatNotNot (a : Bool) : boolToNat (not (not a)) = boolToNat a

Double negation does not change boolToNat.

Bool.boolMeetDistribJoin

def boolMeetDistribJoin (a : Bool) (b : Bool) (c : Bool) : boolMeet a (boolJoin b c) = boolJoin (boolMeet a b) (boolMeet a c)

Lattice meet on Bool distributes over join.

Bool.boolJoinDistribMeet

def boolJoinDistribMeet (a : Bool) (b : Bool) (c : Bool) : boolJoin a (boolMeet b c) = boolMeet (boolJoin a b) (boolJoin a c)

Lattice join on Bool distributes over meet.

Bool.boolMeetComplement

def boolMeetComplement (a : Bool) : boolMeet a (not a) = boolBot

Lattice complement: the meet of a value and its negation is bottom.

Bool.boolJoinComplement

def boolJoinComplement (a : Bool) : boolJoin a (not a) = boolTop

Lattice complement: the join of a value and its negation is top.

Bool.simpAndTrue

theorem simpAndTrue (b : Bool) : and true b = b

true is a left identity for and, proved with simp.

Bool.simpOrFalse

theorem simpOrFalse (b : Bool) : or false b = b

false is a left identity for or, proved with simp.

Bool.Empty_Bool

data Empty_Bool

An empty type used as the target of trueNeqFalseTac.

Bool.trueNeqFalseTac

theorem trueNeqFalseTac (h : true = false) : Empty_Bool

A proof of true = false yields an element of the empty type Empty_Bool, proved with discriminate.

Bool.natToBool

def natToBool (n : Nat) : Bool

Converts a natural number to a boolean: zero to false, any successor to true.

Bool.bool3and

def bool3and (a : Bool) (b : Bool) (c : Bool) : Bool

Three-way conjunction, grouped as (a and b) and c.

Bool.bool3or

def bool3or (a : Bool) (b : Bool) (c : Bool) : Bool

Three-way disjunction, grouped as (a or b) or c.

Bool.conditional

def conditional {A : Type} (b : Bool) (t : A) (f : A) : A

If-then-else as a function: the first value when the boolean is true, otherwise the second.

Bool.natToBoolBoolToNat

def natToBoolBoolToNat (b : Bool) : natToBool (boolToNat b) = b

Converting a boolean to a number and back returns the original boolean.

Bool.natToBoolSucc

def natToBoolSucc (n : Nat) : natToBool (succ n) = true

Every successor converts to true.

Bool.bool3andIsAnd

def bool3andIsAnd (a : Bool) (b : Bool) (c : Bool) : bool3and a b c = and (and a b) c

bool3and unfolds to (a and b) and c.

Bool.bool3andFalseL

def bool3andFalseL (b : Bool) (c : Bool) : bool3and false b c = false

bool3and with false first is false.

Bool.bool3andTrueL

def bool3andTrueL (b : Bool) (c : Bool) : bool3and true b c = and b c

bool3and with true first is the and of the other two.

Bool.bool3andFalseM

def bool3andFalseM (a : Bool) (c : Bool) : bool3and a false c = false

bool3and with false in the middle is false.

Bool.bool3andFalseR

def bool3andFalseR (a : Bool) (b : Bool) : bool3and a b false = false

bool3and with false last is false.

Bool.bool3orIsOr

def bool3orIsOr (a : Bool) (b : Bool) (c : Bool) : bool3or a b c = or (or a b) c

bool3or unfolds to (a or b) or c.

Bool.bool3orTrueL

def bool3orTrueL (b : Bool) (c : Bool) : bool3or true b c = true

bool3or with true first is true.

Bool.bool3orFalseL

def bool3orFalseL (b : Bool) (c : Bool) : bool3or false b c = or b c

bool3or with false first is the or of the other two.

Bool.bool3orTrueM

def bool3orTrueM (a : Bool) (c : Bool) : bool3or a true c = true

bool3or with true in the middle is true.

Bool.bool3orTrueR

def bool3orTrueR (a : Bool) (b : Bool) : bool3or a b true = true

bool3or with true last is true.

Bool.majorityIdem12

def majorityIdem12 (a : Bool) (b : Bool) : majority a a b = a

When the first two votes agree, majority returns that vote.

Bool.majorityIdem13

def majorityIdem13 (a : Bool) (b : Bool) : majority a b a = a

When the first and third votes agree, majority returns that vote.

Bool.majorityAllSame

def majorityAllSame (a : Bool) : majority a a a = a

majority of three equal votes is that vote.

Bool.conditionalTrue

def conditionalTrue {A : Type} (t : A) (f : A) : conditional true t f = t

conditional with true returns its first value.

Bool.conditionalFalse

def conditionalFalse {A : Type} (t : A) (f : A) : conditional false t f = f

conditional with false returns its second value.

Bool.conditionalSame

def conditionalSame {A : Type} (b : Bool) (x : A) : conditional b x x = x

conditional with identical branches returns that value regardless of the condition.

Bool.conditionalNot

def conditionalNot {A : Type} (b : Bool) (x : A) (y : A) : conditional (not b) x y = conditional b y x

Negating the condition of conditional swaps its branches.

Bool.conditionalIsIte

def conditionalIsIte {A : Type} (b : Bool) (x : A) (y : A) : conditional b x y = ite b x y

conditional and ite compute the same result.

Bool.natToBoolAdd

def natToBoolAdd (m : Nat) : natToBool (add (succ zero) m) = true

One plus any natural number converts to true.

Bool.boolToNatOr

def boolToNatOr (a : Bool) (b : Bool) : boolToNat (or a b) = boolToNat (ite a true b)

boolToNat of or a b equals boolToNat of ite a true b.

Bool.boolToNatNot

def boolToNatNot (b : Bool) : add (boolToNat b) (boolToNat (not b)) = succ zero

A boolean and its negation contribute exactly one true between them: their boolToNat values sum to 1.

Bool.bool3andAssoc

def bool3andAssoc (a : Bool) (b : Bool) (c : Bool) : and a (and b c) = and (and a b) c

and is associative.

Bool.bool3orAssoc

def bool3orAssoc (a : Bool) (b : Bool) (c : Bool) : or a (or b c) = or (or a b) c

or is associative.

Bool.notXorSelf

def notXorSelf (a : Bool) (b : Bool) : not (xor a b) = eqBool a b

The negation of xor is eqBool.

Bool.notBool3and

def notBool3and (a : Bool) (b : Bool) (c : Bool) : not (bool3and a b c) = bool3or (not a) (not b) (not c)

De Morgan for three: the negation of bool3and is bool3or of the negations.

Bool.notBool3or

def notBool3or (a : Bool) (b : Bool) (c : Bool) : not (bool3or a b c) = bool3and (not a) (not b) (not c)

De Morgan for three: the negation of bool3or is bool3and of the negations.