3.2. Working with Quotients
A common programming task is working with sets, which are collections of objects without any particular order. In practice, a simple way to handle small sets is to store the elements in a list (or array) and ensure no duplicates, while also making sure that functions on these lists do not rely on the order of the elements. However, typical programming languages do not enforce these invariants, and programmers must take extra care. One common trick is to keep the list sorted, which can reduce the likelihood of accidentally relying on element order. This approach, however, is limited, especially when working with elements that have no natural ordering, or when sorting is too costly.
In mathematics, one possible definition of a multiset is that it is a list of elements, but we impose an equivalence relation: two lists are equivalent if one is a permutation of the other. For example, [1, 2, 3]
is equivalent to [3, 2, 1]
but not to [1, 2, 2]
. In this context, a multiset is the set of all lists that are permutations of each other—i.e., an equivalence class. In Lean, we can work with such equivalence classes directly using quotients.
3.2.1. Unordered Pair
Let’s start with a simpler example: unordered pairs of two natural numbers. Suppose we begin with an ordered pair (a, b)
and define an equivalence relation such that (a, b) ~ (c, d)
if either a = c ∧ b = d
or a = d ∧ b = c
.
We define the equivalence relation as follows:
def equiv : ℕ × ℕ → ℕ × ℕ → Prop :=
fun (a, b) (c, d) => (a = c ∧ b = d) ∨ (a = d ∧ b = c)
Now we define an unordered pair as the quotient of ℕ × ℕ
by this equivalence:
def UnorderedPair := Quot equiv
The Quot
type constructor in Lean takes an equivalence relation r : X → X → Prop
and creates a new type that represents the equivalence classes of X
under this relation. Essentially, Quot r
is a way to work with sets of equivalent values without dealing directly with the specific elements of these sets.
When working with quotients in Lean, it’s useful to understand how Lean manages equivalence classes. Internally, Lean treats each quotient type as if it stores just one representative from each equivalence class. However, unlike in some other programming languages, Lean enforces that any functions defined on these quotient types must be proven to be independent of the choice of representative. This means you must ensure that your functions produce consistent results regardless of which specific element of the equivalence class is used.
Let’s define a function that sums the elements of an unordered pair. In Lean, defining functions on quotients requires using Quot.lift
, which lets you work with representatives while ensuring that the result is independent of which representative is chosen:
def UnorderedPair.sum (p : UnorderedPair) : Nat :=
Quot.lift
(fun (a, b) => a + b)
(p:UnorderedPair⊢ ∀ (a b : ℕ × ℕ),
equiv a b →
(fun x =>
match x with
| (a, b) => a + b)
a =
(fun x =>
match x with
| (a, b) => a + b)
b
p:UnorderedPaira:ℕb:ℕc:ℕd:ℕ⊢ equiv (a, b) (c, d) →
(fun x =>
match x with
| (a, b) => a + b)
(a, b) =
(fun x =>
match x with
| (a, b) => a + b)
(c, d); p:UnorderedPaira:ℕb:ℕc:ℕd:ℕ⊢ a = c ∧ b = d ∨ a = d ∧ b = c → a + b = c + d;
p:UnorderedPaira:ℕb:ℕc:ℕd:ℕh:a = c ∧ b = d ∨ a = d ∧ b = c⊢ a + b = c + d; p:UnorderedPaira:ℕb:ℕc:ℕd:ℕh✝:a = c ∧ b = d⊢ a + b = c + dp:UnorderedPaira:ℕb:ℕc:ℕd:ℕh✝:a = d ∧ b = c⊢ a + b = c + d
case inl h p:UnorderedPaira:ℕb:ℕc:ℕd:ℕh:a = c ∧ b = d⊢ a + b = c + d p:UnorderedPaira:ℕb:ℕc:ℕd:ℕh:a = c ∧ b = d⊢ c + b = c + d; All goals completed! 🐙
case inr h p:UnorderedPaira:ℕb:ℕc:ℕd:ℕh:a = d ∧ b = c⊢ a + b = c + d p:UnorderedPaira:ℕb:ℕc:ℕd:ℕh:a = d ∧ b = c⊢ d + b = c + d; p:UnorderedPaira:ℕb:ℕc:ℕd:ℕh:a = d ∧ b = c⊢ d + c = c + d; All goals completed! 🐙)
p
Here, Quot.lift
takes three arguments: a function that works on representatives, fun (a, b) => a + b
, a proof that the function respects the equivalence relation and an element of the quotient type p
.
To create an element of a quotient, we use Quot.mk
. For example, to construct an unordered pair:
#check Quot.mk equiv (1, 2)
3.2.2. Symbolic Expressions
Let's explore a more intricate example involving symbolic expressions with free variables and a single binary operation. Our goal is to handle expressions in a way that respects mathematical properties such as associativity and the existence of a unit element.
We start by defining an inductive type Expr
to represent these symbolic expressions:
inductive Expr where
| one
| var (n : Nat)
| mul (x y : Expr)
deriving Repr
Here, Expr
consists of three constructors:
-
one
, representing the multiplicative identity, -
var n
, representing a variable with identifiern
, -
mul x y
, representing the multiplication of two expressionsx
andy
.
We would like the multiplication to to be associative and one
as multiplicative unit. Therefore we need to define equivalence relation on Expr
that expresses this and then take an quotient of Expr
.
One way of defining this equivalence relation is to defined normalization function that takes and expression and normalizes it to an unique element. In this particular case, we remove all multiplications by one
and right associate all multiplication. We achieve this by mapping Expr
to List Nat
and back:
def Expr.toList (e : Expr) : List Nat :=
match e with
| one => []
| var n => [n]
| mul x y => x.toList ++ y.toList
def Expr.ofList (l : List Nat) : Expr :=
match l with
| [] => .one
| n :: ns => mul (.var n) (ofList ns)
def Expr.normalize (e : Expr) : Expr :=
.ofList e.toList
For instance, the expression mul (mul (var 0) (mul one (var 1))) (mul (var 2) (var 3))
normalizes to mul (var 0) (mul (var 1) (mul (var 2) (mul (var 3) one)))
:
#eval Expr.mul (.mul (.var 0) (.mul .one (.var 1))) (.mul (.var 2) (.var 3))
|>.normalize
Instead of using Quot
we will use Quotient
which provides a better user experience. To use Quotient
we have to provide an instance of Setoid Expr
which attaches relation to Expr
and proves that it is an equivalence:
instance ExprSetoid : Setoid Expr where
r := fun x y => x.normalize = y.normalize
iseqv := ⊢ Equivalence fun x y => x.normalize = y.normalize
⊢ ∀ (x : Expr), x.normalize = x.normalize⊢ ∀ {x y : Expr}, x.normalize = y.normalize → y.normalize = x.normalize⊢ ∀ {x y z : Expr}, x.normalize = y.normalize → y.normalize = z.normalize → x.normalize = z.normalize
⊢ ∀ (x : Expr), x.normalize = x.normalize x✝:Expr⊢ x✝.normalize = x✝.normalize; All goals completed! 🐙
⊢ ∀ {x y : Expr}, x.normalize = y.normalize → y.normalize = x.normalize x✝:Expry✝:Exprh:x✝.normalize = y✝.normalize⊢ y✝.normalize = x✝.normalize; All goals completed! 🐙
⊢ ∀ {x y z : Expr}, x.normalize = y.normalize → y.normalize = z.normalize → x.normalize = z.normalize x✝:Expry✝:Exprz✝:Exprh:x✝.normalize = y✝.normalizeq:y✝.normalize = z✝.normalize⊢ x✝.normalize = z✝.normalize; x✝:Expry✝:Exprz✝:Exprh:x✝.normalize = y✝.normalizeq:y✝.normalize = z✝.normalize⊢ y✝.normalize = z✝.normalize; All goals completed! 🐙
Now we can define the quotinet of Expr
:
def ExprMonoid := Quotient ExprSetoid
Based on the name, ExprMonoid
forms mathematical monoid. To prove all the necessary monoid theorems we will need the that Expr.ofList
is injective function:
theorem Expr.ofList_injective {l s : List ℕ}
(h : Expr.ofList l = Expr.ofList s) : l = s :=
match l, s, h with
| [], [], _ => rfl
| l::ls, s::ss, h => l✝:List ℕs✝:List ℕh✝:ofList l✝ = ofList s✝l:ℕls:List ℕs:ℕss:List ℕh:ofList (l :: ls) = ofList (s :: ss)⊢ l :: ls = s :: ss
l✝:List ℕs✝:List ℕh✝:ofList l✝ = ofList s✝l:ℕls:List ℕs:ℕss:List ℕh:l = s ∧ ofList ls = ofList ss⊢ ls = ss
l✝:List ℕs✝:List ℕh:ofList l✝ = ofList s✝l:ℕls:List ℕs:ℕss:List ℕleft✝:l = sright✝:ofList ls = ofList ss⊢ ls = ss
l✝:List ℕs✝:List ℕh✝:ofList l✝ = ofList s✝l:ℕls:List ℕs:ℕss:List ℕleft✝:l = sh:ofList ls = ofList ss⊢ ls = ss
All goals completed! 🐙
This lemma shows that if two lists l
and s
produce the same expression via Expr.ofList
, then the lists themselves must be equal.
We can also prove that normalization of already normalized element does nothing:
theorem Expr.normalize_normalize (e : Expr) :
e.normalize.normalize = e.normalize := e:Expr⊢ e.normalize.normalize = e.normalize
e:Expr⊢ ofList (ofList e.toList).toList = ofList e.toList
e:Expr⊢ ofList (ofList []).toList = ofList []e:Exprhead✝:ℕtail✝:List ℕtail_ih✝:ofList (ofList tail✝).toList = ofList tail✝⊢ ofList (ofList (head✝ :: tail✝)).toList = ofList (head✝ :: tail✝)
e:Expr⊢ ofList (ofList []).toList = ofList [] All goals completed! 🐙
e:Exprhead✝:ℕtail✝:List ℕtail_ih✝:ofList (ofList tail✝).toList = ofList tail✝⊢ ofList (ofList (head✝ :: tail✝)).toList = ofList (head✝ :: tail✝) All goals completed! 🐙
For ease of debugging and display, we define a function to convert expressions into strings:
def Expr.toString (e : Expr) : String :=
match e with
| .one => "1"
| .mul x y => s!"({x.toString} * {y.toString})"
| .var n => s!"#{n}"
This function provides a human-readable representation of an Expr
.
3.2.2.1. Monoid Structure of ExprMonoid
Using the quotient type ExprMonoid
, we can show that it forms a monoid where multiplication is associative and has a unit element:
instance : Monoid ExprMonoid where
mul x y := x.liftOn₂ y (fun x y => ⟦.mul x y⟧)
(x:ExprMonoidy:ExprMonoid⊢ ∀ (a₁ b₁ a₂ b₂ : Expr), a₁ ≈ a₂ → b₁ ≈ b₂ → (fun x y => ⟦x.mul y⟧) a₁ b₁ = (fun x y => ⟦x.mul y⟧) a₂ b₂ x:ExprMonoidy:ExprMonoida:Exprb:Expra':Exprb':Exprha:a ≈ a'hb:b ≈ b'⊢ (fun x y => ⟦x.mul y⟧) a b = (fun x y => ⟦x.mul y⟧) a' b'; x:ExprMonoidy:ExprMonoida:Exprb:Expra':Exprb':Exprha:a ≈ a'hb:b ≈ b'⊢ ⟦a.mul b⟧ = ⟦a'.mul b'⟧
x:ExprMonoidy:ExprMonoida:Exprb:Expra':Exprb':Exprha:a ≈ a'hb:b ≈ b'⊢ a.mul b ≈ a'.mul b'
x:ExprMonoidy:ExprMonoida:Exprb:Expra':Exprb':Exprha:Expr.ofList a.toList = Expr.ofList a'.toListhb:Expr.ofList b.toList = Expr.ofList b'.toList⊢ Expr.ofList (a.toList ++ b.toList) = Expr.ofList (a'.toList ++ b'.toList)
x:ExprMonoidy:ExprMonoida:Exprb:Expra':Exprb':Exprha✝:Expr.ofList a.toList = Expr.ofList a'.toListhb:Expr.ofList b.toList = Expr.ofList b'.toListha:a.toList = a'.toList⊢ Expr.ofList (a.toList ++ b.toList) = Expr.ofList (a'.toList ++ b'.toList)
x:ExprMonoidy:ExprMonoida:Exprb:Expra':Exprb':Exprha✝:Expr.ofList a.toList = Expr.ofList a'.toListhb:Expr.ofList b.toList = Expr.ofList b'.toListha:a.toList = a'.toListbh:b.toList = b'.toList⊢ Expr.ofList (a.toList ++ b.toList) = Expr.ofList (a'.toList ++ b'.toList)
All goals completed! 🐙)
one := ⟦.one⟧
mul_assoc := ⊢ ∀ (a b c : ExprMonoid), a * b * c = a * (b * c)
a:ExprMonoidb:ExprMonoidc:ExprMonoid⊢ a * b * c = a * (b * c)
a:ExprMonoidb:ExprMonoidc:ExprMonoid⊢ ∀ (a_1 : Expr), a * b * ⟦a_1⟧ = a * (b * ⟦a_1⟧)
a:ExprMonoidb:ExprMonoidc:ExprMonoid⊢ ∀ (a_1 a_2 : Expr), a * ⟦a_1⟧ * ⟦a_2⟧ = a * (⟦a_1⟧ * ⟦a_2⟧)
a:ExprMonoidb:ExprMonoidc:ExprMonoid⊢ ∀ (a a_1 a_2 : Expr), ⟦a⟧ * ⟦a_1⟧ * ⟦a_2⟧ = ⟦a⟧ * (⟦a_1⟧ * ⟦a_2⟧)
a✝:ExprMonoidb✝:ExprMonoidc✝:ExprMonoida:Exprb:Exprc:Expr⊢ ⟦a⟧ * ⟦b⟧ * ⟦c⟧ = ⟦a⟧ * (⟦b⟧ * ⟦c⟧)
a✝:ExprMonoidb✝:ExprMonoidc✝:ExprMonoida:Exprb:Exprc:Expr⊢ (a.mul b).mul c ≈ a.mul (b.mul c)
a✝:ExprMonoidb✝:ExprMonoidc✝:ExprMonoida:Exprb:Exprc:Expr⊢ Expr.ofList (a.toList ++ b.toList ++ c.toList) = Expr.ofList (a.toList ++ (b.toList ++ c.toList))
a✝:ExprMonoidb✝:ExprMonoidc✝:ExprMonoida:Exprb:Exprc:Expr⊢ a.toList ++ b.toList ++ c.toList = a.toList ++ (b.toList ++ c.toList)
All goals completed! 🐙
one_mul := ⊢ ∀ (a : ExprMonoid), 1 * a = a
a:ExprMonoid⊢ 1 * a = a
a:ExprMonoid⊢ ∀ (a : Expr), 1 * ⟦a⟧ = ⟦a⟧
a✝:ExprMonoida:Expr⊢ 1 * ⟦a⟧ = ⟦a⟧
a✝:ExprMonoida:Expr⊢ Expr.one.mul a ≈ a
a✝:ExprMonoida:Expr⊢ Expr.ofList ([] ++ a.toList) = Expr.ofList a.toList
a✝:ExprMonoida:Expr⊢ [] ++ a.toList = a.toList
All goals completed! 🐙
mul_one := ⊢ ∀ (a : ExprMonoid), a * 1 = a
a:ExprMonoid⊢ a * 1 = a
a:ExprMonoid⊢ ∀ (a : Expr), ⟦a⟧ * 1 = ⟦a⟧
a✝:ExprMonoida:Expr⊢ ⟦a⟧ * 1 = ⟦a⟧
a✝:ExprMonoida:Expr⊢ a.mul Expr.one ≈ a
a✝:ExprMonoida:Expr⊢ Expr.ofList (a.toList ++ []) = Expr.ofList a.toList
a✝:ExprMonoida:Expr⊢ a.toList ++ [] = a.toList
All goals completed! 🐙
To define multiplication we used Quotient.liftOn₂
insteald of Quot.lift
. Also instead of Quot.mk
to create an element of quotient we used the notation ⟦·⟧
. The proofs are rather verbose on purpose so you can step through them step by step and get an idea what does it takes to prove properties when using quotients.
For debuging purposes we might want to print out an element of ExprMonoid
. To maintain consistency of the system we have to print out the string representation of the normalized element:
def ExprMonoid.toString (e : ExprMonoid) : String :=
e.liftOn (fun x => x.normalize.toString)
(e:ExprMonoid⊢ ∀ (a b : Expr), a ≈ b → (fun x => x.normalize.toString) a = (fun x => x.normalize.toString) b e:ExprMonoida:Exprb:Exprh:a ≈ b⊢ (fun x => x.normalize.toString) a = (fun x => x.normalize.toString) b
e:ExprMonoida:Exprb:Exprh✝:a ≈ bh:a.toList = b.toList⊢ (fun x => x.normalize.toString) a = (fun x => x.normalize.toString) b
e:ExprMonoida:Exprb:Exprh✝:a ≈ bh:a.toList = b.toList⊢ (Expr.ofList a.toList).toString = (Expr.ofList b.toList).toString
All goals completed! 🐙)
Sometime we might also want to see the actual representant of (e : ExprMonoid)
. We can accesse it with Quotient.unquot
but this function is unsafe as it might produce different results for propositionally equal arguments i.e. an unsafe function f
might for arguments x
and y
that are equail, x = y
, produce different results f x ≠ f y
.
unsafe def ExprMonoid.toStringRepr (e : ExprMonoid) : String :=
e.unquot.toString
This function is very usefull for debuging but any function using it must be marked as unsafe.
Another useful function is one that normalizes the underlining representation:
def ExprMonoid.normalize (e : ExprMonoid) : ExprMonoid :=
e.liftOn (fun x => ⟦x.normalize⟧)
(e:ExprMonoid⊢ ∀ (a b : Expr), a ≈ b → (fun x => ⟦x.normalize⟧) a = (fun x => ⟦x.normalize⟧) b e:ExprMonoida:Exprb:Exprh:a ≈ b⊢ (fun x => ⟦x.normalize⟧) a = (fun x => ⟦x.normalize⟧) b
e:ExprMonoida:Exprb:Exprh✝:a ≈ bh:a.toList = b.toList⊢ (fun x => ⟦x.normalize⟧) a = (fun x => ⟦x.normalize⟧) b
e:ExprMonoida:Exprb:Exprh✝:a ≈ bh:a.toList = b.toList⊢ ⟦Expr.ofList a.toList⟧ = ⟦Expr.ofList b.toList⟧
All goals completed! 🐙)
We can show that normalization does not change the actual mathematical element:
theorem ExprMonoid.normalize_eq (e : ExprMonoid) : e.normalize = e := e:ExprMonoid⊢ e.normalize = e
e:ExprMonoid⊢ ∀ (a : Expr), normalize ⟦a⟧ = ⟦a⟧
e:ExprMonoidx:Expr⊢ normalize ⟦x⟧ = ⟦x⟧
e:ExprMonoidx:Expr⊢ x.normalize ≈ x
e:ExprMonoidx:Expr⊢ x.normalize.normalize = x.normalize
All goals completed! 🐙
3.2.2.1.1. Example Usage
def var (n : Nat) : ExprMonoid := ⟦.var n⟧
def e := var 0 * var 1 * 1 * 1 * var 0
-- show the mathematical element
#eval e.toString
-- show the underlining representation
#eval e.toStringRepr
-- show the underlining representation after normalization
#eval e.normalize.toStringRepr
This example demonstrates converting and normalizing symbolic expressions into their string representations, showcasing the power of quotients in Lean for maintaining mathematical invariants while managing complex symbolic data.