algebra

IsAssoc

def IsAssoc (A : Type) (op : A -> A -> A) : Type

The proposition that a binary operation is associative: x op (y op z) = (x op y) op z.

IsLeftUnit

def IsLeftUnit (A : Type) (op : A -> A -> A) (e : A) : Type

The proposition that e is a left unit for op: e op x = x.

IsRightUnit

def IsRightUnit (A : Type) (op : A -> A -> A) (e : A) : Type

The proposition that e is a right unit for op: x op e = x.

IsMonoid

def IsMonoid (A : Type) (op : A -> A -> A) (e : A) : Type

The proposition that (A, op, e) is a monoid: op is associative and e is a two-sided unit.

natAddIsAssoc

def natAddIsAssoc : IsAssoc Nat add

Natural-number addition is associative.

natAddIsLeftUnit

def natAddIsLeftUnit : IsLeftUnit Nat add zero

Zero is a left unit for natural-number addition.

natAddIsRightUnit

def natAddIsRightUnit : IsRightUnit Nat add zero

Zero is a right unit for natural-number addition.

natAddIsMonoid

def natAddIsMonoid : IsMonoid Nat add zero

Natural numbers form a monoid under addition with unit zero.

natMulIsLeftUnit

def natMulIsLeftUnit : IsLeftUnit Nat mul (succ zero)

One is a left unit for natural-number multiplication.

natMulIsRightUnit

def natMulIsRightUnit : IsRightUnit Nat mul (succ zero)

One is a right unit for natural-number multiplication.

IsLeftInverse

def IsLeftInverse (A : Type) (op : A -> A -> A) (e : A) (inv : A -> A) : Type

The proposition that inv is a left inverse for op with unit e: inv x op x = e.

IsRightInverse

def IsRightInverse (A : Type) (op : A -> A -> A) (e : A) (inv : A -> A) : Type

The proposition that inv is a right inverse for op with unit e: x op inv x = e.

IsGroup

def IsGroup (A : Type) (op : A -> A -> A) (e : A) (inv : A -> A) : Type

The proposition that (A, op, e, inv) is a group: a monoid in which inv gives two-sided inverses.

addIntLeftInv

def addIntLeftInv (n : Int) : Int.add (Int.neg n) n = pos zero

Negation is a left inverse for integer addition: (-n) + n = 0.

addIntLeftInvPos

def addIntLeftInvPos (k : Nat) : Int.add (Int.neg (pos k)) (pos k) = pos zero

Left inverse law for integer addition on non-negative integers: (-k) + k = 0.

addIntLeftInvPosStep

def addIntLeftInvPosStep (j : Nat) : Int.add (negsucc j) (pos (succ j)) = pos zero

Left inverse law for integer addition on positive integers: negsucc j + (j + 1) = 0.

addIntRightInv

def addIntRightInv (n : Int) : Int.add n (Int.neg n) = pos zero

Negation is a right inverse for integer addition: n + (-n) = 0.

addIntRightInvPos

def addIntRightInvPos (k : Nat) : Int.add (pos k) (Int.neg (pos k)) = pos zero

Right inverse law for integer addition on non-negative integers: k + (-k) = 0.

addIntRightInvPosStep

def addIntRightInvPosStep (j : Nat) : Int.addNat (succ j) (negsucc j) = pos zero

Adding the natural number j + 1 to negsucc j gives zero.

addIntLeftInvNeg

def addIntLeftInvNeg (k : Nat) : Int.add (Int.neg (negsucc k)) (negsucc k) = pos zero

Left inverse law for integer addition on negative integers: -(negsucc k) + negsucc k = 0.

addIntRightInvNeg

def addIntRightInvNeg (k : Nat) : Int.add (negsucc k) (Int.neg (negsucc k)) = pos zero

Right inverse law for integer addition on negative integers: negsucc k + -(negsucc k) = 0.

addIntLeftId

def addIntLeftId (n : Int) : Int.add (pos zero) n = n

Zero is a left identity for integer addition: 0 + n = n.

intAddIsLeftUnit

def intAddIsLeftUnit : IsLeftUnit Int Int.add (pos zero)

Zero is a left unit for integer addition.

intAddIsRightUnit

def intAddIsRightUnit : IsRightUnit Int Int.add (pos zero)

Zero is a right unit for integer addition.

intAddIsLeftInverse

def intAddIsLeftInverse : IsLeftInverse Int Int.add (pos zero) Int.neg

Negation gives left inverses for integer addition.

intAddIsRightInverse

def intAddIsRightInverse : IsRightInverse Int Int.add (pos zero) Int.neg

Negation gives right inverses for integer addition.

IsCommutative

def IsCommutative (A : Type) (op : A -> A -> A) : Type

The proposition that a binary operation is commutative: x op y = y op x.

natAddIsComm

def natAddIsComm : IsCommutative Nat add

Natural-number addition is commutative.

natMulIsComm

def natMulIsComm : IsCommutative Nat mul

Natural-number multiplication is commutative.

natMulIsAssoc

def natMulIsAssoc : IsAssoc Nat mul

Natural-number multiplication is associative.

IsSemigroup

def IsSemigroup (A : Type) (op : A -> A -> A) : Type

The proposition that (A, op) is a semigroup, i.e. op is associative.

natAddIsSemigroup

def natAddIsSemigroup : IsSemigroup Nat add

Natural numbers form a semigroup under addition.

natMulIsSemigroup

def natMulIsSemigroup : IsSemigroup Nat mul

Natural numbers form a semigroup under multiplication.

natMulIsMonoid

def natMulIsMonoid : IsMonoid Nat mul (succ zero)

Natural numbers form a monoid under multiplication with unit one.

IsDistribL

def IsDistribL (A : Type) (mul : A -> A -> A) (add : A -> A -> A) : Type

The proposition that mul distributes over add from the left: x * (y + z) = x * y + x * z.

IsDistribR

def IsDistribR (A : Type) (mul : A -> A -> A) (add : A -> A -> A) : Type

The proposition that mul distributes over add from the right: (x + y) * z = x * z + y * z.

IsRing

def IsRing (A : Type) (add : A -> A -> A) (mul : A -> A -> A) (zero_r : A) (one : A) (neg : A -> A) : Type

The proposition that (A, add, mul, 0, 1, neg) is a ring: an additive group, a multiplicative monoid, and two-sided distributivity.

IsAbelianGroup

def IsAbelianGroup (A : Type) (op : A -> A -> A) (e : A) (inv : A -> A) : Type

The proposition that (A, op, e, inv) is an abelian group: a group whose operation is commutative.

IsCommRing

def IsCommRing (A : Type) (add : A -> A -> A) (mul : A -> A -> A) (zero_r : A) (one : A) (neg : A -> A) : Type

The proposition that (A, add, mul, 0, 1, neg) is a commutative ring: a ring with commutative multiplication.

natMulDistribR

def natMulDistribR : IsDistribR Nat mul add

Natural-number multiplication distributes over addition from the right: (x + y) * z = x * z + y * z.

natMulDistribL

def natMulDistribL : IsDistribL Nat mul add

Natural-number multiplication distributes over addition from the left: x * (y + z) = x * y + x * z.

PreservesOp

def PreservesOp (A : Type) (B : Type) (opA : A -> A -> A) (opB : B -> B -> B) (f : A -> B) : Type

The proposition that f preserves the operation: f (x opA y) = f x opB f y.

PreservesUnit

def PreservesUnit (A : Type) (B : Type) (eA : A) (eB : B) (f : A -> B) : Type

The proposition that f sends the unit eA to the unit eB.

IsMonoidHom

def IsMonoidHom (A : Type) (B : Type) (opA : A -> A -> A) (opB : B -> B -> B) (eA : A) (eB : B) (f : A -> B) : Type

The proposition that f is a monoid homomorphism: it preserves the operation and the unit.

idIsMonoidHom

def idIsMonoidHom (A : Type) (op : A -> A -> A) (e : A) : IsMonoidHom A A op op e e (fun (x : A) => x)

The identity function is a monoid homomorphism.

compIsMonoidHom

def compIsMonoidHom (A : Type) (B : Type) (C : Type) (opA : A -> A -> A) (opB : B -> B -> B) (opC : C -> C -> C) (eA : A) (eB : B) (eC : C) (f : A -> B) (g : B -> C) (hf : IsMonoidHom A B opA opB eA eB f) (hg : IsMonoidHom B C opB opC eB eC g) : IsMonoidHom A C opA opC eA eC (fun (x : A) => g (f x))

The composite of two monoid homomorphisms is a monoid homomorphism.

monoid_power

def monoid_power (A : Type) (op : A -> A -> A) (e : A) (x : A) (n : Nat) : A

The n-th power of x in a monoid: x op (x op … e) with n copies of x.

nat_add_power

def nat_add_power (x : Nat) (n : Nat) : Nat

The n-th additive power of a natural number, i.e. n copies of x added together.

monoidPowerZero

def monoidPowerZero (A : Type) (op : A -> A -> A) (e : A) (x : A) : monoid_power A op e x zero = e

The zeroth power in a monoid is the unit: x^0 = e.

evenTwo

def evenTwo : isEven (succ (succ zero)) = true

Two is even.

IsIdempotent

def IsIdempotent (A : Type) (op : A -> A -> A) : Type

The proposition that a binary operation is idempotent: x op x = x.

boolAndIsIdempotent

def boolAndIsIdempotent : IsIdempotent Bool and

Boolean conjunction is idempotent.

boolOrIsIdempotent

def boolOrIsIdempotent : IsIdempotent Bool or

Boolean disjunction is idempotent.

IsAbsorbing

def IsAbsorbing (A : Type) (mul_op : A -> A -> A) (zero_el : A) : Type

The proposition that zero_el absorbs mul_op from the right: x * 0 = 0.

natMulIsAbsorbing

def natMulIsAbsorbing : IsAbsorbing Nat mul zero

Zero absorbs natural-number multiplication from the right: x * 0 = 0.

NatLE

def NatLE (m : Nat) (n : Nat) : Type

Less-than-or-equal on natural numbers witnessed by a difference: m <= n when m + k = n for some k.

natLERefl

def natLERefl (n : Nat) : NatLE n n

Every natural number is at most itself.

natLEZero

def natLEZero (n : Nat) : NatLE zero n

Zero is at most every natural number.

natLESucc

def natLESucc (m : Nat) (n : Nat) (p : NatLE m n) : NatLE m (succ n)

If m <= n then m <= n + 1.

boolAndIsAssoc

def boolAndIsAssoc : IsAssoc Bool and

Boolean conjunction is associative.

boolOrIsAssoc

def boolOrIsAssoc : IsAssoc Bool or

Boolean disjunction is associative.

boolAndTrueLeftUnit

def boolAndTrueLeftUnit : IsLeftUnit Bool and true

True is a left unit for Boolean conjunction.

boolAndTrueRightUnit

def boolAndTrueRightUnit : IsRightUnit Bool and true

True is a right unit for Boolean conjunction.

boolAndIsMonoid

def boolAndIsMonoid : IsMonoid Bool and true

Booleans form a monoid under conjunction with unit true.

boolOrFalseLeftUnit

def boolOrFalseLeftUnit : IsLeftUnit Bool or false

False is a left unit for Boolean disjunction.

boolOrFalseRightUnit

def boolOrFalseRightUnit : IsRightUnit Bool or false

False is a right unit for Boolean disjunction.

boolOrIsMonoid

def boolOrIsMonoid : IsMonoid Bool or false

Booleans form a monoid under disjunction with unit false.

boolAndIsComm

def boolAndIsComm : IsCommutative Bool and

Boolean conjunction is commutative.

boolOrIsComm

def boolOrIsComm : IsCommutative Bool or

Boolean disjunction is commutative.

IsLeftDistrib

def IsLeftDistrib (A : Type) (add_op : A -> A -> A) (mul_op : A -> A -> A) : Type

The proposition that mul_op distributes over add_op from the left: a * (b + c) = a * b + a * c.

IsRightDistrib

def IsRightDistrib (A : Type) (add_op : A -> A -> A) (mul_op : A -> A -> A) : Type

The proposition that mul_op distributes over add_op from the right: (a + b) * c = a * c + b * c.

natMulIsLeftDistrib

def natMulIsLeftDistrib : IsLeftDistrib Nat add mul

Natural-number multiplication distributes over addition from the left.

natMulIsRightDistrib

def natMulIsRightDistrib : IsRightDistrib Nat add mul

Natural-number multiplication distributes over addition from the right.

leSuccSelf

def leSuccSelf (n : Nat) : NatLE n (succ n)

Every natural number is at most its successor: n <= n + 1.

leAdd

def leAdd (m : Nat) (n : Nat) : NatLE m (add m n)

A natural number is at most itself plus anything: m <= m + n.

IsZeroAnnihilatingL

def IsZeroAnnihilatingL (A : Type) (mul_op : A -> A -> A) (zero_el : A) : Type

The proposition that zero_el annihilates mul_op from the left: 0 * x = 0.

natMulIsZeroAnnihilatingL

def natMulIsZeroAnnihilatingL : IsZeroAnnihilatingL Nat mul zero

Zero annihilates natural-number multiplication from the left: 0 * x = 0.

IsSemiring

def IsSemiring (A : Type) (add_op : A -> A -> A) (mul_op : A -> A -> A) (zero_el : A) (one_el : A) : Type

The proposition that (A, add, mul, 0, 1) is a semiring: a commutative additive monoid, a multiplicative monoid, two-sided distributivity, and zero annihilating on both sides.

natIsSemiring

def natIsSemiring : IsSemiring Nat add mul zero (succ zero)

Natural numbers form a semiring under addition and multiplication.

IsCommSemiring

def IsCommSemiring (A : Type) (add_op : A -> A -> A) (mul_op : A -> A -> A) (zero_el : A) (one_el : A) : Type

The proposition that (A, add, mul, 0, 1) is a commutative semiring: a semiring with commutative multiplication.

natIsCommSemiring

def natIsCommSemiring : IsCommSemiring Nat add mul zero (succ zero)

Natural numbers form a commutative semiring under addition and multiplication.

monoidPowerOne

def monoidPowerOne (A : Type) (op : A -> A -> A) (e : A) (x : A) : monoid_power A op e x (succ zero) = op x e

The first power in a monoid unfolds to x op e.

natAddPowerOne

def natAddPowerOne (x : Nat) : nat_add_power x (succ zero) = add x zero

The first additive power of x unfolds to x + 0.

nat_mul_power

def nat_mul_power (x : Nat) (n : Nat) : Nat

The n-th multiplicative power of a natural number, x^n, computed as a monoid power with unit one.

natMulPowerZero

def natMulPowerZero (x : Nat) : nat_mul_power x zero = succ zero

The zeroth multiplicative power is one: x^0 = 1.

natMulPowerOne

def natMulPowerOne (x : Nat) : nat_mul_power x (succ zero) = mul x (succ zero)

The first multiplicative power unfolds to x * 1.

boolAndDistribOr

def boolAndDistribOr : IsLeftDistrib Bool or and

Conjunction distributes over disjunction from the left: a && (b || c) = (a && b) || (a && c).

boolOrDistribAnd

def boolOrDistribAnd : IsLeftDistrib Bool and or

Disjunction distributes over conjunction from the left: a || (b && c) = (a || b) && (a || c).

boolAndOrAbsorb

def boolAndOrAbsorb : (a : Bool) -> (b : Bool) -> and a (or a b) = a

Absorption law for Booleans: a && (a || b) = a.

boolOrAndAbsorb

def boolOrAndAbsorb : (a : Bool) -> (b : Bool) -> or a (and a b) = a

Absorption law for Booleans: a || (a && b) = a.

IsInvolutive

def IsInvolutive (A : Type) (f : A -> A) : Type

The proposition that f is an involution: f (f x) = x.

boolNotIsInvolutiveInst

def boolNotIsInvolutiveInst : IsInvolutive Bool not

Boolean negation is an involution.

intNegIsInvolutive

def intNegIsInvolutive : IsInvolutive Int Int.neg

Integer negation is an involution: -(-n) = n.

IsInjective

def IsInjective (A : Type) (B : Type) (f : A -> B) : Type

The proposition that f is injective: f x = f y implies x = y.

succIsInjective

def succIsInjective : IsInjective Nat Nat succ

The successor function on natural numbers is injective.

posIsInjective

def posIsInjective : IsInjective Nat Int pos

The embedding of natural numbers into integers is injective.

leAntisym_zero

def leAntisym_zero : NatLE zero zero

Zero is at most zero.

IsCommMonoid

def IsCommMonoid (A : Type) (op : A -> A -> A) (e : A) : Type

The proposition that (A, op, e) is a commutative monoid.

natAddIsCommMonoid

def natAddIsCommMonoid : IsCommMonoid Nat add zero

Natural numbers form a commutative monoid under addition.

natMulIsCommMonoid

def natMulIsCommMonoid : IsCommMonoid Nat mul (succ zero)

Natural numbers form a commutative monoid under multiplication.

boolAndIsCommMonoid

def boolAndIsCommMonoid : IsCommMonoid Bool and true

Booleans form a commutative monoid under conjunction with unit true.

boolOrIsCommMonoid

def boolOrIsCommMonoid : IsCommMonoid Bool or false

Booleans form a commutative monoid under disjunction with unit false.

IsLeftCancellative

def IsLeftCancellative (A : Type) (op : A -> A -> A) : Type

The proposition that op is left cancellative: a op b = a op c implies b = c.

natAddIsLeftCancellativeAux

def natAddIsLeftCancellativeAux (a : Nat) (b : Nat) (c : Nat) (p : add a b = add a c) : b = c

Left cancellation for natural-number addition: a + b = a + c implies b = c, by recursion on a.

natAddIsLeftCancellative

def natAddIsLeftCancellative : IsLeftCancellative Nat add

Natural-number addition is left cancellative.

IsRightCancellative

def IsRightCancellative (A : Type) (op : A -> A -> A) : Type

The proposition that op is right cancellative: b op a = c op a implies b = c.

predSuccPath

def predSuccPath (n : Nat) : pred (succ n) = n

The predecessor of a successor: pred (n + 1) = n.

succPredPath

def succPredPath (n : Nat) : succ (pred (succ n)) = succ n

Successor after predecessor on a successor: succ (pred (n + 1)) = n + 1.

IsAnticommutative

def IsAnticommutative (A : Type) (op : A -> A -> A) (inv : A -> A) : Type

The proposition that op is anticommutative with respect to inv: x op y = inv (y op x).

IsSelfInverse

def IsSelfInverse (A : Type) (op : A -> A -> A) (e : A) : Type

The proposition that every element is its own inverse: x op x = e.

boolXorIsSelfInverse

def boolXorIsSelfInverse : IsSelfInverse Bool xor false

Every Boolean is its own inverse under xor: xor x x = false.

IsUnital

def IsUnital (A : Type) (op : A -> A -> A) (e : A) : Type

The proposition that e is a two-sided unit for op.

natAddIsUnital

def natAddIsUnital : IsUnital Nat add zero

Zero is a two-sided unit for natural-number addition.

natMulIsUnital

def natMulIsUnital : IsUnital Nat mul (succ zero)

One is a two-sided unit for natural-number multiplication.

boolAndIsUnital

def boolAndIsUnital : IsUnital Bool and true

True is a two-sided unit for Boolean conjunction.

boolOrIsUnital

def boolOrIsUnital : IsUnital Bool or false

False is a two-sided unit for Boolean disjunction.

IsJoinSemilattice

def IsJoinSemilattice (A : Type) (join : A -> A -> A) : Type

The proposition that join is associative, commutative and idempotent.

IsMeetSemilattice

def IsMeetSemilattice (A : Type) (meet : A -> A -> A) : Type

The proposition that meet is associative, commutative and idempotent.

boolOrIsJoinSL

def boolOrIsJoinSL : IsJoinSemilattice Bool or

Booleans form a join semilattice under disjunction.

boolAndIsMeetSL

def boolAndIsMeetSL : IsMeetSemilattice Bool and

Booleans form a meet semilattice under conjunction.

IsLattice

def IsLattice (A : Type) (join : A -> A -> A) (meet : A -> A -> A) : Type

The proposition that join and meet form a lattice: both are semilattices and the absorption laws hold.

boolIsLattice

def boolIsLattice : IsLattice Bool or and

Booleans form a lattice with disjunction as join and conjunction as meet.

IsBoundedLattice

def IsBoundedLattice (A : Type) (join : A -> A -> A) (meet : A -> A -> A) (top : A) (bot : A) : Type

The proposition that (A, join, meet) is a lattice with top as the unit for meet and bot as the unit for join.

mulSuccSucc

theorem mulSuccSucc (m : Nat) (n : Nat) : mul m (succ (succ n)) = add m (add m (mul m n))

Multiplying by n + 2 on the right: m * (n + 2) = m + (m + m * n).

mulSuccSuccL

def mulSuccSuccL (m : Nat) (n : Nat) : mul (succ (succ m)) n = add n (add n (mul m n))

Multiplying by m + 2 on the left: (m + 2) * n = n + (n + m * n).

IsSemiringLaws

def IsSemiringLaws (A : Type) (add_op : A -> A -> A) (mul_op : A -> A -> A) (zero_el : A) (one_el : A) : Type

The semiring laws for (A, add, mul, 0, 1) listed one by one in a single product.

natSemiringLaws

def natSemiringLaws : IsSemiringLaws Nat add mul zero (succ zero)

Natural numbers satisfy every semiring law listed in IsSemiringLaws.

doubleDistrib

def doubleDistrib (m : Nat) (n : Nat) : mul (succ (succ zero)) (add m n) = add (mul (succ (succ zero)) m) (mul (succ (succ zero)) n)

Multiplication by two distributes over addition: 2 * (m + n) = 2 * m + 2 * n.

mulDistribSucc

def mulDistribSucc (m : Nat) (n : Nat) : mul m (succ n) = add m (mul m n)

Multiplication by a successor on the right: m * (n + 1) = m + m * n.

tripleDistrib

def tripleDistrib (m : Nat) (n : Nat) : mul (succ (succ (succ zero))) (add m n) = add (mul (succ (succ (succ zero))) m) (mul (succ (succ (succ zero))) n)

Multiplication by three distributes over addition: 3 * (m + n) = 3 * m + 3 * n.

doubleSucc

def doubleSucc (n : Nat) : double (succ n) = succ (succ (double n))

Doubling a successor adds two: double (n + 1) = double n + 2.

mulTwoEqDouble

def mulTwoEqDouble (n : Nat) : mul (succ (succ zero)) n = double n

Multiplying by two is doubling: 2 * n = double n.

addLeftComm

theorem addLeftComm (a : Nat) (b : Nat) (c : Nat) : add a (add b c) = add b (add a c)

Left commutativity of natural-number addition: a + (b + c) = b + (a + c).

addRightComm

theorem addRightComm (a : Nat) (b : Nat) (c : Nat) : add (add a b) c = add (add a c) b

Right commutativity of natural-number addition: (a + b) + c = (a + c) + b.

mulLeftComm

theorem mulLeftComm (a : Nat) (b : Nat) (c : Nat) : mul a (mul b c) = mul b (mul a c)

Left commutativity of natural-number multiplication: a * (b * c) = b * (a * c).

addCommV3

theorem addCommV3 (m : Nat) (n : Nat) : add m n = add n m

Natural-number addition is commutative: m + n = n + m (proved by tactics).

leSuccSucc

def leSuccSucc (m : Nat) (n : Nat) (p : NatLE m n) : NatLE (succ m) (succ n)

Less-than-or-equal is preserved by successor: m <= n implies m + 1 <= n + 1.

GT

def GT (m : Nat) (n : Nat) : Type

Strict greater-than on natural numbers: m > n when n + 1 <= m.

boolXorIsAssoc

def boolXorIsAssoc : IsAssoc Bool xor

Boolean xor is associative.

boolXorFalseLeftUnit

def boolXorFalseLeftUnit : IsLeftUnit Bool xor false

False is a left unit for Boolean xor.

boolXorFalseRightUnit

def boolXorFalseRightUnit : IsRightUnit Bool xor false

False is a right unit for Boolean xor.

boolXorIsComm

def boolXorIsComm : IsCommutative Bool xor

Boolean xor is commutative.

boolXorIsMonoid

def boolXorIsMonoid : IsMonoid Bool xor false

Booleans form a monoid under xor with unit false.

boolXorIsCommMonoid

def boolXorIsCommMonoid : IsCommMonoid Bool xor false

Booleans form a commutative monoid under xor with unit false.

IsHomomorphism

def IsHomomorphism (A : Type) (B : Type) (opA : A -> A -> A) (opB : B -> B -> B) (f : A -> B) : Type

The proposition that f preserves a binary operation: f (x opA y) = f x opB f y.

IsEndomorphism

def IsEndomorphism (A : Type) (op : A -> A -> A) (f : A -> A) : Type

The proposition that f : A -> A preserves the operation op.

idIsEndomorphism

def idIsEndomorphism (A : Type) (op : A -> A -> A) : IsEndomorphism A op (fun (x : A) => x)

The identity function preserves any binary operation.

notIsHomAndOr

def notIsHomAndOr : IsHomomorphism Bool Bool and or not

De Morgan as a homomorphism: not (a && b) = not a || not b.

notIsHomOrAnd

def notIsHomOrAnd : IsHomomorphism Bool Bool or and not

De Morgan as a homomorphism: not (a || b) = not a && not b.

IsAction

def IsAction (M : Type) (A : Type) (mul_act : M -> M -> M) (e : M) (act : M -> A -> A) : Type

The proposition that act is an action of the monoid (M, mul_act, e) on A: the unit acts trivially and acting by m * n is acting by n then m.

symAddZeroR

def symAddZeroR (m : Nat) : m = add m zero

Adding zero on the right, read backwards: m = m + 0.

congSucc

def congSucc (m : Nat) (n : Nat) (p : m = n) : succ m = succ n

The successor function respects equality: m = n implies m + 1 = n + 1.

succAddCancel

def succAddCancel (m : Nat) (n : Nat) (k : Nat) (p : succ (add m k) = succ (add n k)) : add m k = add n k

Cancels a successor on both sides: (m + k) + 1 = (n + k) + 1 implies m + k = n + k.

natAddRightCancel

def natAddRightCancel (a : Nat) (b : Nat) (c : Nat) (p : add b a = add c a) : b = c

Right cancellation for natural-number addition: b + a = c + a implies b = c.

iterateSuccZero

theorem iterateSuccZero (n : Nat) : iterate n succ zero = n

Applying the successor n times to zero gives n.

squareIsPower2

def squareIsPower2 (n : Nat) : square n = Nat.pow n (succ (succ zero))

The square of n is its second power: square n = n^2.

IsMonotone

def IsMonotone (f : Nat -> Nat) : Type

The proposition that a function on natural numbers is monotone with respect to NatLE.

orDistribAndTac

theorem orDistribAndTac (a : Bool) (b : Bool) (c : Bool) : or a (and b c) = and (or a b) (or a c)

Disjunction distributes over conjunction: a || (b && c) = (a || b) && (a || c) (proved by tactics).

andDistribOrTac

theorem andDistribOrTac (a : Bool) (b : Bool) (c : Bool) : and a (or b c) = or (and a b) (and a c)

Conjunction distributes over disjunction: a && (b || c) = (a && b) || (a && c) (proved by tactics).

notNotTac

theorem notNotTac (b : Bool) : not (not b) = b

Boolean negation is involutive: not (not b) = b (proved by tactics).

IsSurjective

def IsSurjective (A : Type) (B : Type) (f : A -> B) : Type

The type saying f is surjective: every y in the codomain has a chosen preimage x with f x = y.

IsBijective

def IsBijective (A : Type) (B : Type) (f : A -> B) : Type

The type saying f is bijective: both injective and surjective.

IsLeftZero

def IsLeftZero (A : Type) (op : A -> A -> A) (e : A) : Type

The proposition that e is a left zero for op: e op x = e.

natMulLeftZero

def natMulLeftZero : IsLeftZero Nat mul zero

Zero is a left zero for natural-number multiplication: 0 * x = 0.

boolAndLeftZero

def boolAndLeftZero : IsLeftZero Bool and false

False is a left zero for conjunction: false && x = false.

boolOrLeftZero

def boolOrLeftZero : IsLeftZero Bool or true

True is a left zero for disjunction: true || x = true.

IsRightZero

def IsRightZero (A : Type) (op : A -> A -> A) (e : A) : Type

The proposition that e is a right zero for op: x op e = e.

natMulRightZero

def natMulRightZero : IsRightZero Nat mul zero

Zero is a right zero for natural-number multiplication: x * 0 = 0.

boolAndRightZero

def boolAndRightZero : IsRightZero Bool and false

False is a right zero for conjunction: x && false = false.

boolOrRightZero

def boolOrRightZero : IsRightZero Bool or true

True is a right zero for disjunction: x || true = true.

lengthMapV2

theorem lengthMapV2 {A : Type} {B : Type} (f : A -> B) (xs : List A) : length (map f xs) = length xs

Mapping a function over a list preserves its length (proved by tactics).

natAddSummary

def natAddSummary : IsCommMonoid Nat add zero

Natural numbers form a commutative monoid under addition.

natMulSummary

def natMulSummary : IsCommMonoid Nat mul (succ zero)

Natural numbers form a commutative monoid under multiplication.

natSemiringSummary

def natSemiringSummary : IsCommSemiring Nat add mul zero (succ zero)

Natural numbers form a commutative semiring.

boolAndSummary

def boolAndSummary : IsCommMonoid Bool and true

Booleans form a commutative monoid under conjunction.

boolOrSummary

def boolOrSummary : IsCommMonoid Bool or false

Booleans form a commutative monoid under disjunction.

boolXorSummary

def boolXorSummary : IsCommMonoid Bool xor false

Booleans form a commutative monoid under xor.

boolLatticeSummary

def boolLatticeSummary : IsLattice Bool or and

Booleans form a lattice under disjunction and conjunction.

andIdempTac

theorem andIdempTac (x : Bool) : and x x = x

Boolean conjunction is idempotent: x && x = x (proved by tactics).

orIdempTac

theorem orIdempTac (x : Bool) : or x x = x

Boolean disjunction is idempotent: x || x = x (proved by tactics).

IsDistribBoth

def IsDistribBoth (A : Type) (mul : A -> A -> A) (add : A -> A -> A) : Type

The proposition that mul distributes over add from both sides.

natDistribBoth

def natDistribBoth : IsDistribBoth Nat mul add

Natural-number multiplication distributes over addition from both sides.

IsFieldLaws

def IsFieldLaws (A : Type) (add : A -> A -> A) (mul : A -> A -> A) (zero_r : A) (one : A) (neg : A -> A) : Type

The field laws checked here: a commutative ring with commutative multiplication; multiplicative inverses are not included.

RatRaw

def RatRaw : Type

Raw rationals as unnormalized (numerator, denominator) pairs of integers.

rat_zero_raw

def rat_zero_raw : RatRaw

The raw rational zero, 0 / 1.

rat_one_raw

def rat_one_raw : RatRaw

The raw rational one, 1 / 1.

IsAbsorbLeft

def IsAbsorbLeft (A : Type) (meet : A -> A -> A) (join : A -> A -> A) : Type

The absorption law of meet over join: meet a (join a b) = a.

IsAbsorbRight

def IsAbsorbRight (A : Type) (join : A -> A -> A) (meet : A -> A -> A) : Type

The absorption law of join over meet: join a (meet a b) = a.

IsModularLaw

def IsModularLaw (A : Type) (join : A -> A -> A) (meet : A -> A -> A) : Type

The modular law: whenever a <= c (that is, meet a c = a), join a (meet b c) = meet (join a b) c.

IsDistributiveLattice

def IsDistributiveLattice (A : Type) (join : A -> A -> A) (meet : A -> A -> A) : Type

The proposition that meet and join distribute over each other in both directions.

IsClosedUnderAdd

def IsClosedUnderAdd (A : Type) (add : A -> A -> A) (S : A -> Type) : Type

The proposition that the subset S is closed under add.

IsClosedUnderMul

def IsClosedUnderMul (A : Type) (mul : A -> A -> A) (S : A -> Type) : Type

The proposition that the subset S absorbs multiplication on the left: S y implies S (x * y) for every x.

IsIdeal

def IsIdeal (A : Type) (add : A -> A -> A) (mul : A -> A -> A) (S : A -> Type) : Type

The proposition that S is a left ideal: closed under addition and under multiplication by any ring element.

IsGroupAction

def IsGroupAction (G : Type) (X : Type) (act : G -> X -> X) (e : G) (op : G -> G -> G) : Type

The proposition that act is an action of (G, op, e) on X: the unit acts trivially and acting by g op h is acting by h then g.

trivialActIsGroupAction

def trivialActIsGroupAction (G : Type) (X : Type) (e : G) (op : G -> G -> G) : IsGroupAction G X (fun (g : G) => fun (x : X) => x) e op

The trivial action, where every element fixes every point, is a group action.

KernelPred

def KernelPred (A : Type) (B : Type) (eB : B) (f : A -> B) : A -> Type

The kernel of f as a predicate: x is in it when f x = eB.

ImagePred

def ImagePred (A : Type) (B : Type) (f : A -> B) : B -> Type

The image of f as a predicate: y is in it when some x has f x = y.

IsGroupHom

def IsGroupHom (A : Type) (B : Type) (opA : A -> A -> A) (opB : B -> B -> B) (f : A -> B) : Type

The proposition that f preserves the group operation: f (x opA y) = f x opB f y.

idIsGroupHom

def idIsGroupHom (A : Type) (op : A -> A -> A) : IsGroupHom A A op op (fun (x : A) => x)

The identity function is a group homomorphism.

compIsGroupHom

def compIsGroupHom (A : Type) (B : Type) (C : Type) (opA : A -> A -> A) (opB : B -> B -> B) (opC : C -> C -> C) (f : A -> B) (g : B -> C) (hf : IsGroupHom A B opA opB f) (hg : IsGroupHom B C opB opC g) : IsGroupHom A C opA opC (fun (x : A) => g (f x))

The composite of two group homomorphisms is a group homomorphism.

boolAndIsMonoid_via

def boolAndIsMonoid_via : IsMonoid Bool and true

Booleans form a monoid under conjunction with unit true.

boolOrIsMonoid_via

def boolOrIsMonoid_via : IsMonoid Bool or false

Booleans form a monoid under disjunction with unit false.

natAddMonCommPair

def natAddMonCommPair : (IsMonoid Nat add zero) × (IsCommutative Nat add)

Natural-number addition is a monoid and commutative, given as a pair.

pairNat

def pairNat (m : Nat) (n : Nat) : Nat × Nat

Builds a pair of natural numbers.

pairNatFst

def pairNatFst (m : Nat) (n : Nat) : fst (pairNat m n) = m

The first projection of pairNat m n is m.

pairNatSnd

def pairNatSnd (m : Nat) (n : Nat) : snd (pairNat m n) = n

The second projection of pairNat m n is n.

idIsId

def idIsId (A : Type) (x : A) : (fun (y : A) => y) x = x

Applying the identity function returns its argument.

alg_const

def alg_const (A : Type) (B : Type) (b : B) : A -> B

The constant function A -> B with value b.

constApplied

def constApplied (A : Type) (B : Type) (b : B) (x : A) : alg_const A B b x = b

The constant function with value b returns b at every point.

pairBool

def pairBool (a : Bool) (b : Bool) : Bool × Bool

Builds a pair of Booleans.