Defining algebraic structures

Stream: lean4

[Tomáš Pecl]

Hello. I am trying to define Linear algebra. I have several problems and questions about it. Currently I got this:

class Inv (F : Type u) where
  inv : F -> F
postfix:max "⁻¹" => Inv.inv

class Zero (F : Type u) where
  zero : F
instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

class One (F : Type u) where
  one : F
instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1



class Monoid (F : Type u) (op : F -> F -> F) (ide : F) where
  --I would like to use a custom notation here so instead "op ide a = a"
  --I would like to use 1 * a = a but only inside here
  --so that it would not interfere with the Field definition
  --which instanciates two Group structures each with a different operator (+ and *)
  id_op: ∀ a : F, op ide a = a
  assoc: ∀ a b c : F, op a (op b c) = op (op a b) c

--why can I not put class here?
--what is the difference between class and structure?
structure CommutMonoid (F : Type u) (op : F -> F -> F) (ide : F) extends Monoid F op ide where
  comm: ∀ a b : F, op a b = op b a

theorem op_id (m : CommutMonoid F op ide) : ∀ a : F, op a ide = a := by {
  intro a
  rw [m.comm,m.id_op]
}

class Group (F : Type u) (op : F -> F -> F) (ide : F) (inv : F -> F) extends CommutMonoid F op ide where
  a_op_inv_a: ∀ a : F, op a (inv a) = ide

--I can use the proof from the CommutMonoid in here
theorem op_id2 (g : Group F op ide inv) : ∀ a : F, op a ide = a := op_id g.toCommutMonoid

--I use this for saying that multiplication is "ConditionalGroup f (.*.) 1 (.⁻¹) (. ≠ 0)"
class ConditionalGroup (F : Type u) (op : F -> F -> F) (ide : F) (inv : F -> F) (inv_cond : F -> Prop) extends CommutMonoid F op ide where
  a_op_inv_a: ∀ a : F, inv_cond a -> op a (inv a) = ide

class Field (F : Type u) extends Zero F, Add F, Neg F, One F, Mul F, Inv F where
  plus: Group F (.+.) 0 (-.)  --the Group structure of +
  mult: ConditionalGroup F (.*.) 1 (.⁻¹) (. ≠ 0) --the Group structure of *
  ldistr: ∀ a b c : F, a * (b + c) = a*b + a*c  --left distrubutivity

--I can use the more general proof for CommutMonoid here for both + and * to define these "shortcuts"
theorem plus_zero (f : Field F) : ∀ a : F, a + 0 = a := op_id f.plus.toCommutMonoid
theorem mult_one (f : Field F) : ∀ a : F, a * 1 = a := op_id f.mult.toCommutMonoid

--proof of right distributivity
theorem rdistr (f : Field F) : ∀ a b c : F, (b + c)*a = b*a + c*a := by {
  intro a b c
  rw [f.mult.comm,f.ldistr,f.mult.comm b a,f.mult.comm a c]
}

--I can use multiple Fields here and prove things about them, not sure if I ever need this
--(this example is quite stupid)
theorem x (f1 : Field F1) (f2 : Field F2) : (∀ a : F1, a + 0 = a) ∧ (∀ a : F2, a + 0 = a) := by {
  exact And.intro (op_id f1.plus.toCommutMonoid) (op_id f2.plus.toCommutMonoid)
}

--why can I not use class here?
structure LinearSpace (f: Field F) (L : Type u) extends Zero L, Add L, Neg L, HMul F L L where
  plus: Group L (.+.) 0 (-.)
  --scalar multiplication axioms -> maybe I could replace these by something like a Monoid?
  --mult: Monoid ???
  one_mult: ∀ a : L, (1 : F) * a = a
  mult_assoc: ∀ a b : F, ∀ x : L, a * (b * x) = (a * b) * x
  --distrubutivity axioms
  ldistr: ∀ a : F, ∀ x y : L, a * (x + y) = a*x + a*y
  rdistr: ∀ a b : F, ∀ x : L, (a + b) * x = a*x + b*x

--this does not work if LinearSpace is not class -> + and 0 are unknown
theorem unique_zero_vector (f : Field F) (l : LinearSpace f L) : ∀ zero : L, ((∀ a : L, zero + a = a) -> zero = 0) := by {
  intro zero2
  intro is_zero
  have zero2_plus_zero := is_zero 0
  rw [l.plus.comm zero2 0] at zero2_plus_zero
  rw [l.plus.id_op] at zero2_plus_zero
  exact zero2_plus_zero
}

[Eric Wieser]

Here's an answer to the local * notation:

section
variable (F : Type u) (op : F -> F -> F) (ide : F)
local infix:65 "*" => op
local notation "𝟙" => ide
class Monoid where
  id_op: ∀ a : F, 𝟙 * a = a
  assoc: ∀ a b c : F, a * (b * c) = (a * b) * c

end

[Tomáš Pecl]

But wouldnt that mean that Monoid would be private in the section? Like then I would have to open that section if I wanted to use that Monoid somewhere else, or am I wrong?

[Tomáš Pecl]

But I am gonna try it

[Eric Wieser]

The only thing that is "private" in the section are the local commands

[Eric Wieser]

The Monoid type is not private

[Tomáš Pecl]

Ok so I made it work:

section MonoidsDefs
variable (F : Type u) (op : F -> F -> F) (id : F)
local infix:65 "*" => op
local notation "𝟙" => id

class Monoid where
  id_op: ∀ a : F, 𝟙 * a = a
  assoc: ∀ a b c : F, a * (b * c) = (a * b) * c

structure CommutMonoid extends Monoid F op id where
  comm: ∀ a b : F, a*b = b*a
end MonoidsDefs

section MonoidsProofs
variable {F : Type u} {op : F -> F -> F} {id : F}
local infix:65 "*" => op
local notation "𝟙" => id

theorem op_id (m : CommutMonoid F op id) : ∀ a : F, a*id = a := by {
  intro a
  rw [m.comm,m.id_op]
}
end MonoidsProofs

[Eric Wieser]

structure CommutMonoid extends Monoid should be class CommutMonoid extends Monoid

[Tomáš Pecl]

I used curly braces {} in the section MonoidsProofs for the variables to make sure that I do not have to supply the F, op and id whenever I use the theorems

[Eric Wieser]

That choice will come to bite you when you have an expression like a*1 + 0, and need to pick between the two different op_ids with +0 vs *1

[Tomáš Pecl]

Eric Wieser said:

structure CommutMonoid extends Monoid should be class CommutMonoid extends Monoid

But then my code for Group breaks because:

cannot find synthesization order for instance @Group.toCommutMonoid with type
  {F : Type u} → {op : F → F → F} → {ide : F} → (inv : F → F) → [self : Group F op ide inv] → CommutMonoid F op ide
all remaining arguments have metavariables:
  Group F op ide ?invLean 4
T5.Group.a_op_inv_a.{u} {F : Type u} {op : F → F → F} {ide : F} {inv : F → F} [self : Group F op ide inv] (a : F) :
  op a (inv a) = ide

[Eric Wieser]

You should use

class Group (F : Type u) (op : F -> F -> F) (ide : F) (inv : outParam <| F -> F) extends CommutMonoid F op ide where
  a_op_inv_a: ∀ a : F, op a (inv a) = ide

[Eric Wieser]

Which tells Lean "if you know op and ide already, then there is only one possible inv"

[Tomáš Pecl]

Eric Wieser said:

That choice will come to bite you when you have an expression like a*1 + 0, and need to pick between the two different op_ids with +0 vs *1

hey it works:

theorem identities (f : Field F) : ∀ a : F, a*1 + 0 = a := by {
  intro a
  rw [f.plus.comm,f.plus.id_op,f.mult.comm,f.mult.id_op]
}

[Ruben Van de Velde]

Please use #backticks

[Tomáš Pecl]

yea, sorry, I fixed it

[Eric Wieser]

Just to check, I assume you're aware that mathlib already has docs#Field and docs#Module etc, and you're doing this as an exercise?

[Tomáš Pecl]

Yes. I am trying to write it from scratch

[Tomáš Pecl]

Eric Wieser said:

You should use

class Group (F : Type u) (op : F -> F -> F) (ide : F) (inv : outParam <| F -> F) extends CommutMonoid F op ide where
  a_op_inv_a: ∀ a : F, op a (inv a) = ide

why should it mean that "once you know op and ide, you know inv"?

[Tomáš Pecl]

can you explain why it makes it work?

[Eric Wieser]

docs#outParam has some explanation, but perhaps not enough