6. Discrete Mathematics
Discrete Mathematics is the study of finite sets, objects, and structures. We can count the elements of a finite set, and we can compute finite sums or products over its elements, we can compute maximums and minimums, and so on. We can also study objects that are generated by finitely many applications of certain generating functions, we can define functions by structural recursion, and prove theorems by structural induction. This chapters describes parts of Mathlib that support these activities.
6.1. Finsets and Fintypes
6.2. Counting Arguments
6.3. Inductively Defined Types
We have seen that Nat is a inductive structure:
inductive Nat where -- ``Nat`` is a Type defined by induction
| zero : Nat
| succ (n : Nat) : Nat
The data type List α is defined inductively:
namespace MyListSpace
inductive List (α : Type*) where
| nil : List α -- empty list
| cons : α → List α → List α -- constructor: take two args (α, List α), return [α, ...List α]
end MyListSpace
Lean defines:
[]fornilarg₁ :: arg₂forcons arg₁ arg₂;arg₁must be an element,arg₂must be a list.::is right-associativeYou can write
[a, b, c]fora :: b :: c :: [], because:
a :: b :: c :: [] = a :: b :: (c :: []) = a :: (b :: [c]) = a :: [b, c] = [a, b, c]
def append {α : Type*} : List α → List α → List α -- take two args (List α, List α)
-- bs is a List
| [], bs => bs -- append bs to [] leads to bs
-- ``a :: as`` is a List [``a``, ..., ``as``]
| a :: as, bs => a :: (append as bs) -- ``a :: (append as bs)``: [``a``, ..., ``as``, ...``bs``]
def map {α β : Type*} (f : α → β) : List α → List β
| [] => []
| a :: as => f a :: map f as -- applies f to every element of the list
#eval append [1, 2, 3] [4, 5, 6]
#eval map (fun n => n^2) [1, 2, 3, 4, 5]
The functions append and map are also defined in the standard library.
append as bscan be written asas ++ bs.