Copyright © 2018–2023 Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, and Jannis Limperg. See LICENSE.txt.

import LoVe.Lectures.LoVe06_InductivePredicates_Demo
import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Algebra.BigOperators.Group.Multiset

LoVe Demo 13: Basic Mathematical Structures

We introduce definitions and proofs about basic mathematical structures such as groups, fields, and linear orders.

set_option autoImplicit false
set_option tactic.hygienic false

namespace LoVe

Type Classes over a Single Binary Operator

Mathematically, a group is a set G with a binary operator ⬝ : G × G → G with the following properties, called group axioms:

Examples of groups are

In Lean, a type class for groups can be defined as follows:

namespace MonolithicGroup

class Group (α : Type) where
  mul          : α → α → α
  one          : α
  inv          : α → α
  mul_assoc    : ∀a b c, mul (mul a b) c = mul a (mul b c)
  one_mul      : ∀a, mul one a = a
  mul_left_inv : ∀a, mul (inv a) a = one


end MonolithicGroup

In Lean, however, group is part of a larger hierarchy of algebraic structures:

Type class Properties Examples
Semigroup associativity of * , , ,
Monoid Semigroup with unit 1 , , ,
LeftCancelSemigroup Semigroup with c * a = c * b → a = b
RightCancelSemigroup Semigroup with a * c = b * c → a = b
Group Monoid with inverse ⁻¹

Most of these structures have commutative versions: CommSemigroup, CommMonoid, CommGroup.

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

Type class Properties Examples
AddSemigroup associativity of + , , ,
AddMonoid AddSemigroup with unit 0 , , ,
AddLeftCancelSemigroup AddSemigroup with c + a = c + b → a = b , , ,
AddRightCancelSemigroup AddSemigroup with a + c = b + c → a = b , , ,
AddGroup AddMonoid with inverse - , ,
#print Group
#print AddGroup

Let us define our own type, of integers modulo 2, and register it as an additive group.

inductive Int2 : Type
  | zero
  | one


def Int2.add : Int2 → Int2 → Int2
  | Int2.zero, a         => a
  | Int2.one,  Int2.zero => Int2.one
  | Int2.one,  Int2.one  => Int2.zero


instance Int2.AddGroup : AddGroup Int2 :=
  { add          := Int2.add
    zero         := Int2.zero
    neg          := fun a ↦ a
    add_assoc    :=
      by
        intro a b c
        cases a <;>
          cases b <;>
          cases c <;>
          rfl
    zero_add     :=
      by
        intro a
        cases a <;>
          rfl
    add_zero     :=
      by
        intro a
        cases a <;>
          rfl
    add_left_neg :=
      by
        intro a
        cases a <;>
          rfl
    nsmul := @nsmulRec _ ⟨Int2.zero⟩ ⟨Int2.add⟩ -- ignore these last two lines
    zsmul := @zsmulRec _ ⟨Int2.zero⟩ ⟨Int2.add⟩ ⟨fun a ↦ a⟩ (@nsmulRec _ ⟨Int2.zero⟩ ⟨Int2.add⟩) }

These last two lines are a small implementation detail showing through -- these arguments are "morally" default arguments, but mathlib leaves them underspecified for power users. https://github.com/leanprover-community/mathlib4/pull/6262

#reduce Int2.one + 0 - 0 - Int2.one

Another example: Lists are an AddMonoid:

instance List.AddMonoid {α : Type} : AddMonoid (List α) :=
  { zero      := []
    add       := fun xs ys ↦ xs ++ ys
    add_assoc := List.append_assoc
    zero_add  := List.nil_append
    add_zero  := List.append_nil
    nsmul := @nsmulRec _ ⟨[]⟩ ⟨fun xs ys ↦ xs ++ ys⟩ }

Type Classes with Two Binary Operators

Mathematically, a field is a set F such that

In Lean, fields are also part of a larger hierarchy:

Type class Properties Examples
Semiring Monoid and AddCommMonoid with distributivity , , ,
CommSemiring Semiring with commutativity of * , , ,
Ring Monoid and AddCommGroup with distributivity , ,
CommRing Ring with commutativity of * , ,
DivisionRing Ring with multiplicative inverse ⁻¹ ,
Field DivisionRing with commutativity of * ,
#print Field

Let us continue with our example:

def Int2.mul : Int2 → Int2 → Int2
  | Int2.one,  a => a
  | Int2.zero, _ => Int2.zero

instance Int2.Field : Field Int2 :=
  { Int2.AddGroup with
    one            := Int2.one
    mul            := Int2.mul
    inv            := fun a ↦ a
    add_comm       :=
      by
        intro a b
        cases a <;>
          cases b <;>
          rfl
    exists_pair_ne :=
      by
        apply Exists.intro Int2.zero
        apply Exists.intro Int2.one
        simp
    zero_mul       :=
      by
        intro a
        rfl
    mul_zero       :=
      by
        intro a
        cases a <;>
          rfl
    one_mul        :=
      by
        intro a
        rfl
    mul_one        :=
      by
        intro a
        cases a <;>
          rfl
    mul_inv_cancel :=
      by
        intro a h
        cases a
        { apply False.elim
          apply h
          rfl }
        { rfl }
    inv_zero       := by rfl
    mul_assoc      := sorry
    mul_comm       := sorry
    left_distrib   := sorry
    right_distrib  := sorry

    nnqsmul := _ -- again, ignore these implementation details.
    qsmul := _ }

#reduce (1 : Int2) * 0 / (0 - 1)


#reduce (3 : Int2)


theorem ring_example (a b : Int2) :
  (a + b) ^ 3 = a ^ 3 + 3 * a ^ 2 * b + 3 * a * b ^ 2 + b ^ 3 :=
  by ring

ring proves equalities over commutative rings and semirings by normalizing expressions.

Coercions

When combining numbers form , , , and , we might want to cast from one type to another. Lean has a mechanism to automatically introduce coercions, represented by Coe.coe (syntactic sugar: ). Coe.coe can be set up to provide implicit coercions between arbitrary types.

Many coercions are already in place, including the following:

For example, this works, even though negation - n is not defined on natural numbers:

theorem neg_mul_neg_Nat (n : ℕ) (z : ℤ) :
  (- z) * (- n) = z * n :=
  by simp

Notice how Lean introduced a coercion:

#check neg_mul_neg_Nat

Type annotations can document our intentions:

theorem neg_Nat_mul_neg (n : ℕ) (z : ℤ) :
  (- n : ℤ) * (- z) = n * z :=
  by simp


#print neg_Nat_mul_neg

In proofs involving coercions, the tactic norm_cast can be convenient.

theorem Eq_coe_int_imp_Eq_Nat (m n : ℕ)
    (h : (m : ℤ) = (n : ℤ)) :
  m = n :=
  by norm_cast at h


theorem Nat_coe_Int_add_eq_add_Nat_coe_Int (m n : ℕ) :
  (m : ℤ) + (n : ℤ) = ((m + n : ℕ) : ℤ) :=
  by norm_cast

norm_cast moves coercions towards the inside of expressions, as a form of simplification. Like simp, it will often produce a subgoal.

norm_cast relies on theorems such as these:

#check Nat.cast_add
#check Int.cast_add
#check Rat.cast_add

Lists, Multisets, and Finite Sets

For finite collections of elements different structures are available:

theorem List_duplicates_example :
  [2, 3, 3, 4] ≠ [2, 3, 4] :=
  by decide

theorem List_order_example :
  [4, 3, 2] ≠ [2, 3, 4] :=
  by decide

theorem Multiset_duplicates_example :
  ({2, 3, 3, 4} : Multiset ℕ) ≠ {2, 3, 4} :=
  by decide

theorem Multiset_order_example :
  ({2, 3, 4} : Multiset ℕ) = {4, 3, 2} :=
  by decide

theorem Finset_duplicates_example :
  ({2, 3, 3, 4} : Finset ℕ) = {2, 3, 4} :=
  by decide

theorem Finset_order_example :
  ({2, 3, 4} : Finset ℕ) = {4, 3, 2} :=
  by decide

decide is a tactic that can be used on true decidable goals (e.g., a true executable expression).

def List.elems : BTree ℕ → List ℕ
  | BTree.empty      => []
  | BTree.node a l r => a :: List.elems l ++ List.elems r


def Multiset.elems : BTree ℕ → Multiset ℕ
  | BTree.empty      => ∅
  | BTree.node a l r =>
    {a} ∪ Multiset.elems l ∪ Multiset.elems r


def Finset.elems : BTree ℕ → Finset ℕ
  | BTree.empty      => ∅
  | BTree.node a l r => {a} ∪ Finset.elems l ∪ Finset.elems r


#eval List.sum [2, 3, 4]
#eval Multiset.sum ({2, 3, 4} : Multiset ℕ)
-- TODO: #eval Finset.sum ({2, 3, 4} : Finset ℕ) (fun n ↦ n)

#eval List.prod [2, 3, 4]
#eval Multiset.prod ({2, 3, 4} : Multiset ℕ)
-- TODO: #eval Finset.prod ({2, 3, 4} : Finset ℕ) (fun n ↦ n)

Order Type Classes

Many of the structures introduced above can be ordered. For example, the well-known order on the natural numbers can be defined as follows:

inductive Nat.le : ℕ → ℕ → Prop
  | refl : ∀a : ℕ, Nat.le a a
  | step : ∀a b : ℕ, Nat.le a b → Nat.le a (b + 1)


#print Preorder

This is an example of a linear order. A linear order (or total order) is a binary relation such that for all a, b, c, the following properties hold:

If a relation has the first three properties, it is a partial order. An example is on sets, finite sets, or multisets. If a relation has the first two properties, it is a preorder. An example is comparing lists by their length.

In Lean, there are type classes for these different kinds of orders: LinearOrdeer, PartialOrder, and Preorder.

#print Preorder
#print PartialOrder
#print LinearOrder

We can declare the preorder on lists that compares lists by their length as follows:

instance List.length.Preorder {α : Type} : Preorder (List α) :=
  { le :=
      fun xs ys ↦ List.length xs ≤ List.length ys
    lt :=
      fun xs ys ↦ List.length xs < List.length ys
    le_refl :=
      by
        intro xs
        apply Nat.le_refl
    le_trans :=
      by
        intro xs ys zs
        exact Nat.le_trans
    lt_iff_le_not_le :=
      by
        intro a B
        simp
        intro hlt
        linarith }

This instance introduces the infix syntax and the relations , <, and >:

theorem list.length.Preorder_example :
  [1] > [] :=
  by decide

Complete lattices (lecture 11) are formalized as another type class, CompleteLattice, which inherits from PartialOrder.

Type classes combining orders and algebraic structures are also available:

`OrderedCancelCommMonoid`
`OrderedCommGroup`
`OrderedSemiring`
`LinearOrderedSemiring`
`LinearOrderedCommRing`
`LinearOrderedField`

All these mathematical structures relate and < with 0, 1, +, and * by monotonicity rules (e.g., a ≤ b → c ≤ d → a + c ≤ b + d) and cancellation rules (e.g., c + a ≤ c + b → a ≤ b).

end LoVe