Ring instance

Stream: mathlib4

[Martin Dvořák]

This is my first time playing with algebraic structures in Lean 4.
I decided to define a custom Ring instance over rational numbers.
I thought it would be an easy exercise (it probably is -- and I seem to be n00b).

import Mathlib.Data.Rat.Defs

def weirdAdd (a b : ℚ) : ℚ := a + b - 1/2
def weirdMul (a b : ℚ) : ℚ := a + b + 2*a*b

instance : Ring ℚ where
  add := weirdAdd
  mul := weirdMul
  zero := 1/2
  neg := fun x => 1 - x
  one := 0
  zero_add := sorry
  add_zero := sorry
  add_left_neg := sorry
  one_mul := sorry
  mul_one := sorry
  zero_mul := sorry
  mul_zero := sorry
  add_comm := sorry
  add_assoc := sorry
  mul_assoc := sorry
  left_distrib := sorry
  right_distrib := sorry

I already have an error:

type mismatch
  HEq.rfl
has type
  HEq ?m.1052 ?m.1052 : Prop
but is expected to have type
  NatCast.natCast 0 = 0 : Prop

What is the cause? Do I need to provide the natCast function, prove natCast_zero and so on?

[Eric Wieser]

You would do better to do this exercise on a (wrapped) copy of the rational numbers

[Eric Wieser]

structure MyRat where
  val : Rat


def weirdAdd (a b : MyRat) : MyRat := .mk (a.val + b.val - 1/2)
def weirdMul (a b : MyRat) : MyRat := .mk (a.val + b.val + 2*a.val*b.val)

instance : Ring MyRat where

[Eric Wieser]

Otherwise Lean will try to use the existing instance, which is what is going wrong here

[Martin Dvořák]

Would def Q' : Type := ℚ be enough? Or does it have to be a structure with a rational field?

[Eric Wieser]

That would be enough, but it's much easier to make a mess

[Eric Wieser]

If you use that approach, you will want to to define Q'.mk and Q.val manually, and write your code as if you were using a structure

[Martin Dvořák]

How can I unfold the zero now?

import Mathlib.Data.Rat.Defs

structure ℚ' where
  v : ℚ

def weirdAdd (a b : ℚ') : ℚ' := .mk$ a.v + b.v - (1/2 : ℚ)
def weirdMul (a b : ℚ') : ℚ' := .mk$ a.v + b.v + (2 : ℚ) * a.v * b.v

instance weirdRing : Ring ℚ' where
  add := weirdAdd
  mul := weirdMul
  zero := .mk (1/2 : ℚ)
  neg := (fun (x : ℚ') => .mk (1 - x.v))
  one := .mk 0
  zero_add (x : ℚ') := by
    --unfold HAdd.hAdd
    --unfold instHAdd
    --unfold weirdAdd
    --unfold Add.add
    simp only [HAdd.hAdd, instHAdd, weirdAdd, Add.add]
    -- `0.v` is `@OfNat.ofNat ℚ' 0 Zero.toOfNat0 : ℚ'`
    sorry
  add_zero := sorry
  add_left_neg := sorry
  one_mul := sorry
  mul_one := sorry
  zero_mul := sorry
  mul_zero := sorry
  add_comm := sorry
  add_assoc := sorry
  mul_assoc := sorry
  left_distrib := sorry
  right_distrib := sorry

Is there a better way how to get from the generic goal 0 + x = x to working with my definitions?

[Eric Wieser]

Put @[simps] on your defs?

[Eric Wieser]

(and ext on the structure)

[Martin Dvořák]

Did I understand your recommendation right?

import Mathlib.Data.Rat.Defs

@[ext]
structure ℚ' where
  v : ℚ

@[simps]
def weirdAdd (a b : ℚ') : ℚ' := .mk$ a.v + b.v - (1/2 : ℚ)

@[simps]
def weirdMul (a b : ℚ') : ℚ' := .mk$ a.v + b.v + (2 : ℚ) * a.v * b.v

instance weirdRing : Ring ℚ' where
  add := weirdAdd
  mul := weirdMul
  zero := .mk (1/2 : ℚ)
  neg := fun x => .mk (1 - x.v)
  one := .mk 0
  zero_add (x : ℚ') := by
    --simp only [HAdd.hAdd, instHAdd, weirdAdd, Add.add]
    simp -- has no effect
    sorry
  add_zero := sorry
  add_left_neg := sorry
  one_mul := sorry
  mul_one := sorry
  zero_mul := sorry
  mul_zero := sorry
  add_comm := sorry
  add_assoc := sorry
  mul_assoc := sorry
  left_distrib := sorry
  right_distrib := sorry

It has no effect.

[Eric Wieser]

The ext attribute won't do anything until you use the corresponding tactic

[Eric Wieser]

Defining neg and zero separately with simps will help too

[Martin Dvořák]

Still no unfolding.

import Mathlib.Data.Rat.Defs

@[ext]
structure ℚ' where
  v : ℚ

@[simps]
def weirdAdd (a b : ℚ') : ℚ' := .mk$ a.v + b.v - (1/2 : ℚ)

@[simps]
def weirdMul (a b : ℚ') : ℚ' := .mk$ a.v + b.v + (2 : ℚ) * a.v * b.v

@[simps]
def weirdZero : ℚ' := .mk$ 1 / 2

@[simps]
def weirdOne : ℚ' := .mk 0

@[simps]
def weirdNeg (a : ℚ') : ℚ' := .mk$ 1 - a.v

instance weirdRing : Ring ℚ' where
  add := weirdAdd
  mul := weirdMul
  zero := weirdZero
  neg := weirdNeg
  one := weirdOne
  zero_add (x : ℚ') := by
    --ext -- goes too far
    simp -- has no effect
    sorry
  add_zero := sorry
  add_left_neg := sorry
  one_mul := sorry
  mul_one := sorry
  zero_mul := sorry
  mul_zero := sorry
  add_comm := sorry
  add_assoc := sorry
  mul_assoc := sorry
  left_distrib := sorry
  right_distrib := sorry

Is there any tutorial that I could follow?
I cannot be the first one who struggles with these instances.

[Eric Wieser]

ext : 1 will go exactly as far as you need

[Eric Wieser]

here is an exercise that has you build this type of type alias

[Martin Dvořák]

Very nice tutorial, thank you!

[Martin Dvořák]

I finished my exercise:
https://github.com/madvorak/lean4-exercises/blob/main/Rings.lean

• It took me longer than I expected. However, this is indicative of me being a n00b, not of Lean 4 not being user-friendly.
• I didn't manage to do the proofs inside the instance declaration; I might possibly define a notation before declaring the instance and use it in all lemmas, but it is not what I hoped for.
• On the positive side, Lean proved to be a proof assistant. I made a mathematical mistake originally. In Lean, it was easy to find the mistake and very fast to correct it.

[Martin Dvořák]

I would really like to know how to write it so that I will be able open the tactic mode inside the instance declaration and unfold my definitions there. Repeating each condition in a separate lemma statement was annoying.