Structures and Classes

Defining structures

A structure is a bundle of things

              structure Card where
                suit : Fin 4
                value : Fin 13 
              

              structure Point where
                x : ℝ
                y : ℝ
                z : ℝ
              

                structure DirectedLineSegment where
                  src : Point
                  dst : Point
              

                def myPoint : Point where
                  x := 2
                  y := -1
                  z := 4
                

                def myPoint'' : Point :=
                  { x := 2, y := -1, z := 4 }
                

                def myPoint''' : Point :=
                  ⟨2, -1, 4⟩
                

                def myPoint'''' :=
                  Point.mk 2 (-1) 4
                

A trick: write def myPoint : Point := _ and click the 💡

Defining structures

A structure is a bundle of things

              structure Card where
                suit : Fin 4
                value : Fin 13 
              

              structure Point where
                x : ℝ
                y : ℝ
                z : ℝ
              

                structure DirectedLineSegment where
                  src : Point
                  dst : Point
              

                def mySegment : DirectedLineSegment where
                  src := {  -- `where` syntax doesn't work here
                    x := 0
                    y := 1
                    z := 2
                  }
                  dst := ⟨3, 4, 5⟩
                

                  def mySegment' : DirectedLineSegment :=
                    ⟨⟨0, 1, 2⟩, ⟨3, 4, 5⟩⟩
                

Defining structures

Structures can contain any type, including functions

              structure RealSeq where
                term : ℕ → ℝ
              

              structure BundledTuple where
                n : ℕ
                term : Fin n → ℝ
              

              structure NatRel where
                rel : ℕ → ℕ → Prop
              

                def squares : RealSeq where
                  term := fun n => n^2
                

                def adjacentRel : NatRel where
                  rel := fun m n => m = n + 1 ∨ m + 1 = n
                

                  def squares' : RealSequence where
                    term n := n^2
                  

                  def adjacentRel' : NatRel where
                    rel m n := m = n + 1 ∨ m + 1 = n
                  

                  def SumIsTwo : NatRel where
                    rel
                    | 0, 2 | 1, 1 | 2, 0 => True
                    | _, _ => False
                  

                    def myTuple : BundledTuple where
                      n := 3
                      term := ![1, 2, 3]
                  

Defining structuresFunctions and operations

              def add (a b : Point) : Point where
                x := Point.x a + Point.x b
                y := a.y + b.y
                z := a.z + b.z
              

              def add (a b : Point) : Point :=
                ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
              

              def add'' : Point → Point → Point
              | ⟨x₁, y₁, z₁⟩, ⟨x₂, y₂, z₂⟩ =>
                  ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩
              

              def add''' (a b : Point) : Point :=
              match a, b with
              | ⟨x₁, y₁, z₁⟩, ⟨x₂, y₂, z₂⟩ =>
                  ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩
              

Defining structuresDot notation

If we have p : Point, then p.func means Point.func p

We should put the add function we just defined in the Point namespace

                namespace Point

                def add (a b : Point) : Point :=
                  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

                end Point
              

                def Point.add (a b : Point) : Point :=
                  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
              

Now we can write p1.add p2 instead of add p1 p2

Good style: definitions and theorems about Point
go in that namespace.

Defining structuresParameterized structures

Just like functions, structures can take parameters

            structure Point' (R : Type) where
              x : R
              y : R
              z : R
          

We can define points with different coefficient types:

              def myRealPoint : Point' ℝ where
                x := 2
                y := -1
                z := 4
              

                def myIntPoint : Point' ℤ :=
                  Point'.mk 2 (-1) 4
              

Defining structuresOperator notation

p1.add p2 is ok, but what about p1 + p2?

          instance : Add Point where
            add a b :=
              { x := a.x + b.x
                y := a.y + b.y
                z := a.z + b.z }

          example : Point := ⟨1, 0, 0⟩ + ⟨0, 1, 0⟩
          

Defining structuresClasses and instances

            instance : Add Point where
              add a b :=
                { x := a.x + b.x
                  y := a.y + b.y
                  z := a.z + b.z }
            

Defining structuresClasses and instances

                instance : Add Point where
                  add a b :=
                    { x := a.x + b.x
                      y := a.y + b.y
                      z := a.z + b.z }
              

                @[instance]
                def instAddPoint : Add Point where
                  add a b :=
                  { x := a.x + b.x
                    y := a.y + b.y
                    z := a.z + b.z }
              

What's Add? A (parameterized) class

                class Add (α : Type) where
                  add : α → α → α
              

                structure Add' (α : Type) where
                  add : α → α → α
              

How do class and structure differ?

                  #checkAdd.add {α : Type}
                    [self : Add α] (x y : α) : α
                   Add.add
                

                  #checkAdd'.add {α : Type}
                    (self : Add α) (x y : α) : α
                   Add'.add
                

Defining structuresClasses and instances

Square brackets are autofilled with instances

How exactly does this work for x y : Point?

1. x + y is notation for Add.add x y (ok, strictly it means HAdd.hAdd x y…)
2. Add.add x y elaborates to @Add.add Point _ x y
3. Lean needs _ : Add Point; it looks for instances that match this type
4. #synth Add Point demonstrates this:

   
                 [Meta.synthInstance] ✅ Add Point ▼
                   [] new goal Add Point ▼
                     [instances] #[@AddZeroClass.toAdd, @AddSemigroup.toAdd, @Distrib.toAdd, instAddPoint] 
                   [] ✅ apply instAddPoint to Add Point ▼
                     [tryResolve] ✅ Add Point ≟ Add Point 
                   [] result instAddPoint 
                 

Defining structuresclass or structure

Is there a canonical value for your definition?

Proofs with structures

Proofs with structurestrivial lemmas

Make sure to teach the simplifier the
trivial lemmas about your operation

            @[simp] theorem add_x (a b : Point) : (a + b).x = a.x + b.x :=
              rfl
            @[simp] theorem add_y (a b : Point) : (a + b).y = a.y + b.y :=
              rfl
            @[simp] theorem add_z (a b : Point) : (a + b).z = a.z + b.z :=
              rfl
          

              example : ((⟨1, 2, 3⟩ : Point) + (⟨10, 20, 30⟩ : Point)).x = 11 := by
                dsimp -- goal is now `1 + 10 = 11`
                norm_num
            

Proofs with structuresExtensionality

How do we prove two points are equal?

              
@[ext]
              theorem Point.ext {a b : Point}
                  (hx : a.x = b.x)
                  (hy : a.y = b.y)
                  (hz : a.z = b.z) : a = b := by
  cases a
                cases b
  dsimp only at *
                /-
  hx : x✝¹ = x✝
                hy : y✝¹ = y✝
                hz : z✝¹ = z✝
                ⊢ { x := x✝¹, y := y✝¹, z := z✝¹ }
                  = { x := x✝, y := y✝, z := z✝ }
  -/
                rw [hx, hy, hz]
              

Proofs with structuresExtensionality

How do we prove two points are equal?

              
@[ext]
              theorem Point.ext {a b : Point}
                  (hx : a.x = b.x)
                  (hy : a.y = b.y)
                  (hz : a.z = b.z) : a = b := by
  obtain ⟨a_x, a_y, a_z⟩ := a
                obtain ⟨a_b, b_y, b_z⟩ := b
  dsimp only at *
                /-
  hx : a_x = a_b
                hy : a_y = b_y
                hz : a_z = b_z
                ⊢ { x := a_x, y := a_y, z := a_z }
                  = { x := a_b, y := b_y, z := b_z }
  -/
                rw [hx, hy, hz]
              

Proofs with structuresExtensionality

How do we prove two points are equal?

              @[ext]
              structure Point where
                x : ℝ
                y : ℝ
                z : ℝ
              

              example {a b : Point}
                  (hx : a.x = b.x)
                  (hy : a.y = b.y)
                  (hz : a.z = b.z) : a = b := by
                ext
                repeat' assumption
              

                protected
                theorem add_comm (a b : Point) :
                    a + b = b + a := by
                  ext <;> dsimp <;> apply add_comm
              

Proofs with structuresProofs within structures

Structures can contain proof fields too:

              structure OpenDisc2D (r : ℝ) where
                x : ℝ
                y : ℝ
                mem_disc : x^2 + y^2 < r^2
              

              def unitDiscZero : OpenDisc2D 1 where
                x := 0
                y := 0
                mem_disc := by
                  -- goal is 0 ^ 2 + 0 ^ 2 < 1 ^ 2
                  norm_num
              

              example (p : OpenDisc2D 1) : p.x ≠ 2 := by
                intro hx            -- hx : p.x = 2
                have := p.mem_disc  -- this : p.x ^ 2 + p.y ^ 2 < 1 ^ 2
                nlinarith
            

Proofs with structuresProofs within structures

More examples

                structure EvenNat
                    where
                  n : ℕ
                  is_even : Even n
              

                structure PythagoreanTriple
                    where
                  a : ℕ
                  b : ℕ
                  c : ℕ
                  sq_add_sq : a^2 + b^2 = c^2
              

                structure RootOf (f : ℝ → ℝ)
                    where
                  x : ℝ
                  is_root : f x = 0
              

              -- based on a silly software interview question
              structure IsFizzBuzz (n : ℕ) : Prop where
                three_dvd : 3 ∣ n
                five_dvd : 5 ∣ n
            

Built-in structures

          /-- `α × β` is notation for `Prod α β` -/
          structure Prod (α : Type u) (β : Type v) where
            fst : α
            snd : β
          

          /-- `{x : α // p x}` is notation for `Subtype p` -/
          structure Subtype {α : Sort u} (p : α → Prop) where
            val : α
            property : p val
          

            def Point' : Type := ℝ × ℝ × ℝ -- syntax for `Prod ℝ (Prod ℝ ℝ)`
            def OpenDisc2D' (r : ℝ) : Type := {x : ℝ × ℝ // x.1^2 + x.2^2 < r ^ 2}
            

Exercises: show these types are equivalent!

Algebraic structures

Don't want to repeat the same lemma for every type:

                example (a b : Point) :
                  a + b = b + a :=
                Point.add_comm a b
              

                example (a b : ℚ) :
                  a + b = b + a :=
                rat.add_comm a b
              

                example (a b : ℝ) :
                  a + b = b + a :=
                real.add_comm a b
              

We already saw typeclasses for notation;
what about typeclasses for proofs as well?

            example {A : Type*} [AddCommGroup A] (a b : A) :
              a + b = b + a :=
            AddCommGroup.add_comm a b
          

                instance :
                    AddCommGroup Point :=
                  sorry

                example (a b : Point) :
                  a + b = b + a :=
                AddCommGroup.add_comm a b
              

                instance :
                    AddCommGroup ℚ :=
                  sorry

                example (a b : ℚ) :
                  a + b = b + a :=
                AddCommGroup.add_comm a b
              

                instance :
                    AddCommGroup ℝ :=
                  sorry

                example (a b : ℝ) :
                  a + b = b + a :=
                AddCommGroup.add_comm a b
              

Algebraic structuresMathematical background

This isn't just a Lean trick; mathematical examples:

partially ordered set

a set $P$ and a binary relation $\le$ on $P$ that is transitive and antisymmetric.

group

a set $G$ with an associative binary operation, an identity element $1$, and a function $g \mapsto g^{-1}$ that returns an inverse for each $g$ in $G$. A group is abelian or commutative if the operation is commutative.

lattice

a partially ordered set with meets and joins.

ring

an (additively written) abelian group $(R, +, 0, x \mapsto -x)$ together with an associative multiplication operation $\cdot$ and an identity $1$, such that multiplication distributes over addition. A ring is commutative if the multiplication is commutative.

ordered ring

a ring together with a partial order on its elements $(R, +, 0, -, \cdot, 1, \le)$, such that $a \le b$ implies $a + c \le b + c$ for every $a$, $b$, and $c$ in $R$, and $0 \le a$ and $0 \le b$ implies $0 \le a b$ for every $a$ and $b$ in $R$.

metric space

a set $X$ and a function $d : X \times X \to \mathbb{R}$ such that the following hold:

• $d(x, y) \ge 0$ for every $x$ and $y$ in $X$.
• $d(x, y) = 0$ if and only if $x = y$.
• $d(x, y) = d(y, x)$ for every $x$ and $y$ in $X$.
• $d(x, z) \le d(x, y) + d(y, z)$ for every $x$, $y$, and $z$ in $X$.

Algebraic structuresMathematical background

A fairly direct lean translation:

partially ordered set

              class PartialOrder (P : Type) :=  -- a set $P$ and
                le : P → P → Prop               -- a binary relation $\le$ on $P$
                le_trans : Transitive le        -- that is transitive
                le_antirefl : AntiSymmetric le  -- and antisymmetric
              

group

              class Group (G : Type) :=     -- a set $G$ with
                mul : G → G → G             -- an associative binary operation,
                mul_assoc : Associative mul
                one : G                     -- an identity element $1$, and
                one_mul : LeftIdentity mul one
                mul_one : RightIdentity mul one
                inv : G → G                 -- a function $g \mapsto g^{-1}$ that
                mul_right_inv :
                  RightInverse mul inv one  -- returns an inverse for each $g$ in $G$.
              

These are not quite the definitions in mathlib,
but they're close enough to not matter

Algebraic structuresA Group class

The group definition in mathlib avoids Associative
and instead writes things out directly:

          class Group (G : Type) where
            mul : G → G → G
            one : G
            inv : G → G
            mul_assoc : ∀ x y z : G, mul (mul x y) z = mul x (mul y z)
            mul_one : ∀ x : G, mul x one = x
            one_mul : ∀ x : G, mul one x = x
            mul_left_inv : ∀ x : G, mul (inv x) x = one
          

            instance Group.toMul (G) [Group G] : Mul G where
              mul := Group.mul
            instance Group.toOne (G) [Group G] : One G where
              one := Group.one
            instance Group.toInv (G) [Group G] : Inv G where
              inv := Group.inv
            

Algebraic structuresA more readable Group class

We can do a little better by directly putting these in Group; now we can use the notation in the definition!

          class Group (G : Type) where
            toMul : Mul G
            toOne : One G
            toInv : Inv G
          
  mul_assoc : ∀ x y z : G, (x * y) * z = x * (y * z)
            mul_one : ∀ x : G, x * 1 = x
            one_mul : ∀ x : G, 1 * x = x
            mul_left_inv : ∀ x : G, x⁻¹ * x = 1
          attribute [instance] Group.toMul Group.toOne Group.toInv
          

            variables (G) [Group G]
            #synth Mul G  -- displays `Group.toMul`
            example : Mul G := inferInstance
            

Algebraic structuresAn even more readable Group class

This pattern is so common that Lean has
special notation for it, extends:

          class Group (G : Type) extends Mul G, One G, Inv G where    
          
  mul_assoc : ∀ x y z : G, (x * y) * z = x * (y * z)
            mul_one : ∀ x : G, x * 1 = x
            one_mul : ∀ x : G, 1 * x = x
            mul_left_inv : ∀ x : G, x⁻¹ * x = 1
          

Algebraic structuresExample: the permutation group

            instance : One (Equiv.Perm α) where
              one := Equiv.refl _
            instance : Mul (Equiv.Perm α) where
              mul x y := x.trans y
            instance : Inv (Equiv.Perm α) where
              inv x := x.symm
            

            instance : Group (Equiv.perm α) where
              -- one, mul, and inv are filled automatically
              mul_assoc x y z := by
                sorry
              mul_one x := by
                sorry
              one_mul x := by
                sorry
              mul_left_inv x := by
                sorry
            

Algebraic structuresExample: product of groups

Classes can be chained transitively:

          instance [One α] [One β] : One (α × β) where
            one := (1, 1)
          instance [Mul α] [Mul β] : Mul (α × β) where
            mul x y := (x.1 * y.1, x.2 * x.2)
          instance [Inv α] [Inv β] : Inv (α × β) where
            inv x := (x.1⁻¹, x.2⁻¹)
          

          instance [Group α] [Group β]  : Group (α × β) where
            mul_assoc x y z := by
              sorry
            mul_one x := by
              sorry
            one_mul x := by
              sorry
            mul_left_inv x := by
              sorry
          

Exercise: do this for AddGroup Point

Algebraic structuresAdvanced: forgetful inheritance

              example {α : Type} :
                  Group (Equiv.Perm α) where
                mul := _
                mul_assoc := _
                one := _
                one_mul := _
                mul_one := _
                npow := _
                npow_zero := _
                npow_succ := _
                inv := _
                div := _
                div_eq_mul_inv := _
                zpow := _
                zpow_zero' := _
                zpow_succ' := _
                zpow_neg' := _
                mul_left_inv := _
              

Algebraic structuresAdvanced: type synonyms

What if our algebraic structure is non-canonical?

                @[ext]
                structure MulOpposite (α : Type) where op ::
                  unop : α
              

                variable {α} [Mul α]
                instance : Mul (MulOpposite α) where
                  mul x y := op (unop y * unop x)
              
                @[simp] theorem op_mul (a b : α) :
                  op (a * b) = op b * op a := rfl
                @[simp] theorem unop_mul
                  (a b : MulOpposite α) :
                  unop (a * b) = unop b * unop a := rfl