Lecture 4.2: Mathematics — Algebra

Central to nearly everything in mathematics is algebra

Today we introduce definitions and proofs about basic mathematical structures

mathlib

Lean's core library includes only basic algebraic definitions

More setup and especially tactics are found in mathlib: Lean's mathematical library

Syntactic classes

We start with "syntactic" type classes, which contain constants but no assumptions:

class has_mul (α : Type) := (mul : α → α → α)
class has_one (α : Type) := (one : α)
class has_inv (α : Type) := (inv : α → α)

For these type classes, the traditional symbols *, 1, and ⁻¹ are defined in Lean's core library (library/init/core.lean)

The "semantic" hierarchy is build on top of the syntactic type classes

Classes over a single binary operator

Many of the following structures are very simple, but provide a long list of derived facts and constants building on them (e.g. big operators)

Lean starts the algebraic hierarchy with one binary operator, called *:

Most of these structures have commutative versions, prefixed with comm_:

comm_semigroup, comm_monoid, comm_group

The multiplicative structures (over *, 1, ⁻¹) are copied to produce additive versions (over +, 0, -), prefixed with add_

The copying process is automated by the transport_multiplicative_to_additive tactic and the to_additive attribute provided by mathlib

add_semigroup, add_monoid, add_group
add_comm_semigroup, add_comm_monoid, add_comm_group,
add_left_cancel_semigroup, add_right_cancel_semigroup

Example instance for add_monoid: list with ++ and [] (which is also a add_left_cancel_semigroup and a add_right_cancel_semigroup)

Rings and fields

The additive and multiplicative structures are combined to form rings and fields

The commutative versions assume commutativity of *

By convention, ∀n, n / 0 = 0 in discrete_field

The hierarchy between ring and field is more fine-grained: (integral) domains, Euclidean rings, etc.

Ordered structures

Type classes combining orders and algebraic structures are also available:

ordered_cancel_comm_monoid, ordered_comm_group
ordered_semiring, linear_ordered_semiring, linear_ordered_comm_ring
linear_ordered_field

All these mathematical structures relate ≤ and < with the constants 0, 1, +, and * by monotonicity rules a ≤ b → c ≤ d → a + c ≤ b + d and cancellation rules x + b ≤ x + c → b ≤ c

Big operators

Big operators (∑ and ∏) allow us to sum (or multiply) a family of values

a1 + a2 + ... + aN

mathlib provides prod and sum operations over list (ordered, with duplicates), multiset (unordered, with duplicates), and finset (unordered, no duplicates)

The big operators list.prod, multiset.prod, and finset.prod are first introduced and then copied using the to_additive attribute

Big operators over lists for add_monoid:

list.sum []       = 0
list.sum (a :: l) = a + list.sum l

Big operators over multisets for add_comm_monoid:

multiset.sum ∅        = 0
multiset.sum {a}      = a
multiset.sum (a :: m) = a + multiset.sum m
multiset.sum (s ∪ t)  = multiset.sum s + multiset.sum t

Big operators over finsets for add_comm_monoid:

finset.sum f ∅            = 0
finset.sum f {a}          = f a
finset.sum f (insert a s) = f a + finset.sum f s               if a ∉ s
finset.sum f (s ∪ t)      = finset.sum f s + finset.sum f t    if s ∩ t = ∅

Notice the presence of an indexed-family f

mathlib provides a collections of lemmas describing how the big operators behave under reorderings, basic operators on list, multiset, and finset, morphisms, order relations, and more

Coercions

In mathematics, we have subset relations between different "types" of numbers:

ℕ ⊆ ℤ ⊆ ℚ ⊆ ℝ

In Lean, each is represented by its own type, with injective morphisms representing the subsets

Lean's coercion mechanism is set up to introduce these morphisms automatically, to lighten notation

The coercion operator is coe (written ↑) and can be setup to convert arbitrary types

For numbers we have

• coe : ℕ → α for a semiring α, which allows us to embed ℕ into another semiring

• coe : ℤ → α for a ring α, which allows us to embed ℤ into another ring

• coe : ℚ → α for a division ring α, which allows us to embed ℚ into another division ring

All of these coercions support the desirable morphism laws:

↑0       = 0
↑1       = 1
↑(a + b) = ↑a + ↑b
↑(a * b) = ↑a * ↑b
↑a ≤ ↑b  ↔ a ≤ b

Numerals

Number literals are represented as sequences of bit0 and bit1:

• 0, 1, bit0 n := n + n, bit1 n := n + n + 1

• 16 = bit0 (bit0 (bit0 (bit0 1)))

Tactics

ac_refl

Reflexivity modulo associativity and commutativity (is_associative and is_commutative type classes)

ring and abel

Normalizes ring terms or terms of commutative monoids and groups

norm_num

Normalizes numerals (dec_trivial only works for ℕ)

linarith

Decides linear arithmetic problems (e.g. 10 < 5 + 13 * x + 17 * y)

Demo

42_lecture.lean

Newly introduced syntax

Tactics

References

• Theorem Proving in Lean by Jeremy Avigad et al., Section 6.7