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.

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) 
    (byp : 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 
      intro (a,b) (c,d)p : UnorderedPair
a : ℕ
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); simp_all [equiv]p : UnorderedPair
a : ℕ
b : ℕ
c : ℕ
d : ℕ
⊢ a = c ∧ b = d ∨ a = d ∧ b = c → a + b = c + d; 
      intro hp : UnorderedPair
a : ℕ
b : ℕ
c : ℕ
d : ℕ
h : a = c ∧ b = d ∨ a = d ∧ b = c
⊢ a + b = c + d; cases hinl
p : UnorderedPair
a : ℕ
b : ℕ
c : ℕ
d : ℕ
h✝ : a = c ∧ b = d
⊢ a + b = c + d
inr
p : UnorderedPair
a : ℕ
b : ℕ
c : ℕ
d : ℕ
h✝ : a = d ∧ b = c
⊢ a + b = c + d 
      case inl h =>p : UnorderedPair
a : ℕ
b : ℕ
c : ℕ
d : ℕ
h : a = c ∧ b = d
⊢ a + b = c + d rw[h.left]p : UnorderedPair
a : ℕ
b : ℕ
c : ℕ
d : ℕ
h : a = c ∧ b = d
⊢ c + b = c + d; rw[h.right]All goals completed! 🐙
      case inr h =>p : UnorderedPair
a : ℕ
b : ℕ
c : ℕ
d : ℕ
h : a = d ∧ b = c
⊢ a + b = c + d rw[h.left]p : UnorderedPair
a : ℕ
b : ℕ
c : ℕ
d : ℕ
h : a = d ∧ b = c
⊢ d + b = c + d; rw[h.right]p : UnorderedPair
a : ℕ
b : ℕ
c : ℕ
d : ℕ
h : a = d ∧ b = c
⊢ d + c = c + d; simp[add_comm]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:

Quot.mk equiv (1, 2) : Quot equiv#check Quot.mk equiv (1, 2)

Add functions

UnorderedPair.toString
UnorderedPair.toStringRepr
UnorderedPair.normalizedRepr

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 identifier n,
mul x y, representing the multiplication of two expressions x and y.

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))):

WorkingWithQuotients.Expr.mul
  (WorkingWithQuotients.Expr.var 0)
  (WorkingWithQuotients.Expr.mul
    (WorkingWithQuotients.Expr.var 1)
    (WorkingWithQuotients.Expr.mul
      (WorkingWithQuotients.Expr.var 2)
      (WorkingWithQuotients.Expr.mul (WorkingWithQuotients.Expr.var 3) (WorkingWithQuotients.Expr.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 := by⊢ Equivalence fun x y => x.normalize = y.normalize 
    constructorrefl
⊢ ∀ (x : Expr), x.normalize = x.normalize
symm
⊢ ∀ {x y : Expr}, x.normalize = y.normalize → y.normalize = x.normalize
trans
⊢ ∀ {x y z : Expr}, x.normalize = y.normalize → y.normalize = z.normalize → x.normalize = z.normalize
    ·refl
⊢ ∀ (x : Expr), x.normalize = x.normalize introrefl
x✝ : Expr
⊢ x✝.normalize = x✝.normalize; rflAll goals completed! 🐙
    ·symm
⊢ ∀ {x y : Expr}, x.normalize = y.normalize → y.normalize = x.normalize intro _ _ hsymm
x✝ : Expr
y✝ : Expr
h : x✝.normalize = y✝.normalize
⊢ y✝.normalize = x✝.normalize; rw[h]All goals completed! 🐙
    ·trans
⊢ ∀ {x y z : Expr}, x.normalize = y.normalize → y.normalize = z.normalize → x.normalize = z.normalize intro _ _ _ h qtrans
x✝ : Expr
y✝ : Expr
z✝ : Expr
h : x✝.normalize = y✝.normalize
q : y✝.normalize = z✝.normalize
⊢ x✝.normalize = z✝.normalize; rw[h]trans
x✝ : Expr
y✝ : Expr
z✝ : Expr
h : x✝.normalize = y✝.normalize
q : y✝.normalize = z✝.normalize
⊢ y✝.normalize = z✝.normalize; rw[q]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 => byl✝ : 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 
    simp_all [ofList]l✝ : List ℕ
s✝ : List ℕ
h✝ : ofList l✝ = ofList s✝
l : ℕ
ls : List ℕ
s : ℕ
ss : List ℕ
h : l = s ∧ ofList ls = ofList ss
⊢ ls = ss
    induction hintro
l✝ : List ℕ
s✝ : List ℕ
h : ofList l✝ = ofList s✝
l : ℕ
ls : List ℕ
s : ℕ
ss : List ℕ
left✝ : l = s
right✝ : ofList ls = ofList ss
⊢ ls = ss
    rename_i hintro
l✝ : List ℕ
s✝ : List ℕ
h✝ : ofList l✝ = ofList s✝
l : ℕ
ls : List ℕ
s : ℕ
ss : List ℕ
left✝ : l = s
h : ofList ls = ofList ss
⊢ ls = ss
    apply ofList_injective hAll 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 := bye : Expr
⊢ e.normalize.normalize = e.normalize
  unfold Expr.normalizee : Expr
⊢ ofList (ofList e.toList).toList = ofList e.toList
  induction e.toListnil
e : Expr
⊢ ofList (ofList []).toList = ofList []
cons
e : Expr
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ofList (ofList tail✝).toList = ofList tail✝
⊢ ofList (ofList (head✝ :: tail✝)).toList = ofList (head✝ :: tail✝)
  ·nil
e : Expr
⊢ ofList (ofList []).toList = ofList [] simp[Expr.ofList, Expr.toList]All goals completed! 🐙
  ·cons
e : Expr
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ofList (ofList tail✝).toList = ofList tail✝
⊢ ofList (ofList (head✝ :: tail✝)).toList = ofList (head✝ :: tail✝) simp_all[Expr.ofList, Expr.toList]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.

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⟧) 
    (byx : ExprMonoid
y : 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₂ intro a b a' b' ha hbx : ExprMonoid
y : ExprMonoid
a : Expr
b : Expr
a' : Expr
b' : Expr
ha : a ≈ a'
hb : b ≈ b'
⊢ (fun x y => ⟦x.mul y⟧) a b = (fun x y => ⟦x.mul y⟧) a' b'; dsimpx : ExprMonoid
y : ExprMonoid
a : Expr
b : Expr
a' : Expr
b' : Expr
ha : a ≈ a'
hb : b ≈ b'
⊢ ⟦a.mul b⟧ = ⟦a'.mul b'⟧
        apply Quotient.sounda._@.Init.Core._hyg.15302
x : ExprMonoid
y : ExprMonoid
a : Expr
b : Expr
a' : Expr
b' : Expr
ha : a ≈ a'
hb : b ≈ b'
⊢ a.mul b ≈ a'.mul b'
        simp_all [HasEquiv.Equiv, Setoid.r, Expr.normalize, Expr.toList]a._@.Init.Core._hyg.15302
x : ExprMonoid
y : ExprMonoid
a : Expr
b : Expr
a' : Expr
b' : Expr
ha : Expr.ofList a.toList = Expr.ofList a'.toList
hb : Expr.ofList b.toList = Expr.ofList b'.toList
⊢ Expr.ofList (a.toList ++ b.toList) = Expr.ofList (a'.toList ++ b'.toList)
        have ha := Expr.ofList_injective haa._@.Init.Core._hyg.15302
x : ExprMonoid
y : ExprMonoid
a : Expr
b : Expr
a' : Expr
b' : Expr
ha✝ : Expr.ofList a.toList = Expr.ofList a'.toList
hb : Expr.ofList b.toList = Expr.ofList b'.toList
ha : a.toList = a'.toList
⊢ Expr.ofList (a.toList ++ b.toList) = Expr.ofList (a'.toList ++ b'.toList)
        have bh := Expr.ofList_injective hba._@.Init.Core._hyg.15302
x : ExprMonoid
y : ExprMonoid
a : Expr
b : Expr
a' : Expr
b' : Expr
ha✝ : Expr.ofList a.toList = Expr.ofList a'.toList
hb : Expr.ofList b.toList = Expr.ofList b'.toList
ha : a.toList = a'.toList
bh : b.toList = b'.toList
⊢ Expr.ofList (a.toList ++ b.toList) = Expr.ofList (a'.toList ++ b'.toList)
        congrAll goals completed! 🐙)
  one := ⟦.one⟧
  mul_assoc := by⊢ ∀ (a b c : ExprMonoid), a * b * c = a * (b * c)
    intro a b ca : ExprMonoid
b : ExprMonoid
c : ExprMonoid
⊢ a * b * c = a * (b * c)
    apply Quotient.ind (q:=c)a : ExprMonoid
b : ExprMonoid
c : ExprMonoid
⊢ ∀ (a_1 : Expr), a * b * ⟦a_1⟧ = a * (b * ⟦a_1⟧)
    apply Quotient.ind (q:=b)a : ExprMonoid
b : ExprMonoid
c : ExprMonoid
⊢ ∀ (a_1 a_2 : Expr), a * ⟦a_1⟧ * ⟦a_2⟧ = a * (⟦a_1⟧ * ⟦a_2⟧)
    apply Quotient.ind (q:=a)a : ExprMonoid
b : ExprMonoid
c : ExprMonoid
⊢ ∀ (a a_1 a_2 : Expr), ⟦a⟧ * ⟦a_1⟧ * ⟦a_2⟧ = ⟦a⟧ * (⟦a_1⟧ * ⟦a_2⟧)
    intro a b ca✝ : ExprMonoid
b✝ : ExprMonoid
c✝ : ExprMonoid
a : Expr
b : Expr
c : Expr
⊢ ⟦a⟧ * ⟦b⟧ * ⟦c⟧ = ⟦a⟧ * (⟦b⟧ * ⟦c⟧)
    apply Quotient.sounda._@.Init.Core._hyg.15302
a✝ : ExprMonoid
b✝ : ExprMonoid
c✝ : ExprMonoid
a : Expr
b : Expr
c : Expr
⊢ (a.mul b).mul c ≈ a.mul (b.mul c)
    simp_all only [HasEquiv.Equiv, Setoid.r, Expr.normalize, Expr.toList]a._@.Init.Core._hyg.15302
a✝ : ExprMonoid
b✝ : ExprMonoid
c✝ : ExprMonoid
a : Expr
b : Expr
c : Expr
⊢ Expr.ofList (a.toList ++ b.toList ++ c.toList) = Expr.ofList (a.toList ++ (b.toList ++ c.toList))
    apply congr_arga.h._@.Init.Core._hyg.15302
a✝ : ExprMonoid
b✝ : ExprMonoid
c✝ : ExprMonoid
a : Expr
b : Expr
c : Expr
⊢ a.toList ++ b.toList ++ c.toList = a.toList ++ (b.toList ++ c.toList)
    apply List.append_assocAll goals completed! 🐙
  one_mul := by⊢ ∀ (a : ExprMonoid), 1 * a = a
    intro aa : ExprMonoid
⊢ 1 * a = a
    apply Quotient.ind (q:=a)a : ExprMonoid
⊢ ∀ (a : Expr), 1 * ⟦a⟧ = ⟦a⟧
    intro aa✝ : ExprMonoid
a : Expr
⊢ 1 * ⟦a⟧ = ⟦a⟧
    apply Quotient.sounda._@.Init.Core._hyg.15302
a✝ : ExprMonoid
a : Expr
⊢ Expr.one.mul a ≈ a
    simp_all only [HasEquiv.Equiv, Setoid.r, Expr.normalize, Expr.toList]a._@.Init.Core._hyg.15302
a✝ : ExprMonoid
a : Expr
⊢ Expr.ofList ([] ++ a.toList) = Expr.ofList a.toList
    apply congr_arga.h._@.Init.Core._hyg.15302
a✝ : ExprMonoid
a : Expr
⊢ [] ++ a.toList = a.toList
    apply List.nil_appendAll goals completed! 🐙
  mul_one := by⊢ ∀ (a : ExprMonoid), a * 1 = a
    intro aa : ExprMonoid
⊢ a * 1 = a
    apply Quotient.ind (q:=a)a : ExprMonoid
⊢ ∀ (a : Expr), ⟦a⟧ * 1 = ⟦a⟧
    intro aa✝ : ExprMonoid
a : Expr
⊢ ⟦a⟧ * 1 = ⟦a⟧
    apply Quotient.sounda._@.Init.Core._hyg.15302
a✝ : ExprMonoid
a : Expr
⊢ a.mul Expr.one ≈ a
    simp_all only [HasEquiv.Equiv, Setoid.r, Expr.normalize, Expr.toList]a._@.Init.Core._hyg.15302
a✝ : ExprMonoid
a : Expr
⊢ Expr.ofList (a.toList ++ []) = Expr.ofList a.toList
    apply congr_arga.h._@.Init.Core._hyg.15302
a✝ : ExprMonoid
a : Expr
⊢ a.toList ++ [] = a.toList
    apply List.append_nilAll 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) 
    (bye : ExprMonoid
⊢ ∀ (a b : Expr), a ≈ b → (fun x => x.normalize.toString) a = (fun x => x.normalize.toString) b intro a b he : ExprMonoid
a : Expr
b : Expr
h : a ≈ b
⊢ (fun x => x.normalize.toString) a = (fun x => x.normalize.toString) b 
        have h := Expr.ofList_injective he : ExprMonoid
a : Expr
b : Expr
h✝ : a ≈ b
h : a.toList = b.toList
⊢ (fun x => x.normalize.toString) a = (fun x => x.normalize.toString) b
        simp[Expr.normalize]e : ExprMonoid
a : Expr
b : Expr
h✝ : a ≈ b
h : a.toList = b.toList
⊢ (Expr.ofList a.toList).toString = (Expr.ofList b.toList).toString
        congrAll 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⟧) 
    (bye : ExprMonoid
⊢ ∀ (a b : Expr), a ≈ b → (fun x => ⟦x.normalize⟧) a = (fun x => ⟦x.normalize⟧) b intro a b he : ExprMonoid
a : Expr
b : Expr
h : a ≈ b
⊢ (fun x => ⟦x.normalize⟧) a = (fun x => ⟦x.normalize⟧) b 
        have h := Expr.ofList_injective he : ExprMonoid
a : Expr
b : Expr
h✝ : a ≈ b
h : a.toList = b.toList
⊢ (fun x => ⟦x.normalize⟧) a = (fun x => ⟦x.normalize⟧) b
        simp[Expr.normalize]e : ExprMonoid
a : Expr
b : Expr
h✝ : a ≈ b
h : a.toList = b.toList
⊢ ⟦Expr.ofList a.toList⟧ = ⟦Expr.ofList b.toList⟧
        congrAll goals completed! 🐙)

We can show that normalization does not change the actual mathematical element:

theorem ExprMonoid.normalize_eq (e : ExprMonoid) : e.normalize = e := bye : ExprMonoid
⊢ e.normalize = e
  apply Quotient.ind (q:=e)e : ExprMonoid
⊢ ∀ (a : Expr), normalize ⟦a⟧ = ⟦a⟧
  intro xe : ExprMonoid
x : Expr
⊢ normalize ⟦x⟧ = ⟦x⟧
  apply Quotient.sounda._@.Init.Core._hyg.15302
e : ExprMonoid
x : Expr
⊢ x.normalize ≈ x
  simp only [HasEquiv.Equiv, Setoid.r]a._@.Init.Core._hyg.15302
e : ExprMonoid
x : Expr
⊢ x.normalize.normalize = x.normalize
  apply Expr.normalize_normalizeAll goals completed! 🐙

Example Usage

def var (n : Nat) : ExprMonoid := ⟦.var n⟧
def e := var 0 * var 1 * 1 * 1 * var 0

-- show the mathematical element
"(#0 * (#1 * (#0 * 1)))"
#eval e.toString

-- show the underlining representation
"((((#0 * #1) * 1) * 1) * #0)"
#eval e.toStringRepr

-- show the underlining representation after normalization
"(#0 * (#1 * (#0 * 1)))"
#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.

p	:	UnorderedPair
a	:	ℕ
b	:	ℕ
c	:	ℕ
d	:	ℕ
h	:	a = c ∧ b = d ∨ a = d ∧ b = c

x✝	:	Expr
y✝	:	Expr
z✝	:	Expr
h	:	x✝.normalize = y✝.normalize
q	:	y✝.normalize = z✝.normalize

l✝	:	List ℕ
s✝	:	List ℕ
h✝	:	ofList l✝ = ofList s✝
l	:	ℕ
ls	:	List ℕ
s	:	ℕ
ss	:	List ℕ
h	:	ofList (l :: ls) = ofList (s :: ss)

e	:	Expr
head✝	:	ℕ
tail✝	:	List ℕ
tail_ih✝	:	ofList (ofList tail✝).toList = ofList tail✝

x	:	ExprMonoid
y	:	ExprMonoid
a	:	Expr
b	:	Expr
a'	:	Expr
b'	:	Expr
ha	:	a ≈ a'
hb	:	b ≈ b'

a✝	:	ExprMonoid
b✝	:	ExprMonoid
c✝	:	ExprMonoid
a	:	Expr
b	:	Expr
c	:	Expr

Working with Quotients

Unordered Pair

Symbolic Expressions

Monoid Structure of ExprMonoid

Example Usage

Monoid Structure of `ExprMonoid`