Constructing the integers as equivalence classes

Stream: new members

[Peter Hansen]

I have tried solving some of the exercises in Terence Tao’s Analysis 1. In chapter 4, he constructs the integers as equivalence classes of pairs of natural numbers. To do the exercises, I would like construct them this way in Lean. Here is what I have done:

import Mathlib.Data.Equiv.Functor
import Mathlib.Tactic

def int_equiv (a b : ℕ × ℕ) : Prop :=
  a.1 + b.2 = b.1 + a.2

lemma int_equiv.refl : ∀ a : ℕ × ℕ, int_equiv a a := by
  intro a
  rfl

lemma int_equiv.symm : ∀ {a b : ℕ × ℕ}, int_equiv a b → int_equiv b a := by
  intros a b hab
  unfold int_equiv at *
  rw [hab]

lemma int_equiv.trans : ∀ {a b c : ℕ × ℕ}, int_equiv a b → int_equiv b c → int_equiv a c := by
  intros a b c hab hbc
  unfold int_equiv at *
  have : a.fst + b.snd + c.snd = c.fst + b.snd + a.snd := by
    rw [hab, ← hbc]
    ring
  rw [add_comm a.fst, add_comm c.fst, add_assoc, add_assoc] at this
  exact add_left_cancel this

def intEquiv : Equivalence int_equiv := {
  refl := .refl
  symm := .symm
  trans := .trans }

instance integer_setoid : Setoid (ℕ × ℕ) := {
  r := int_equiv
  iseqv := intEquiv }

def integer := Quotient integer_setoid

notation:65 lhs:65 " — " rhs:66 => (⟦(lhs, rhs)⟧ : integer)

example : 3 — 2 = 2 — 1 := by
  simp
  rfl

The main problem is that I can’t seem to project out the components of an integer, and so just defining addition is not doable. Is my approach fundamentally flawed?

[Yury G. Kudryashov]

You can use docs#Quotient.lift

[Eric Wieser]

For addition you probably want Quotient.map\_2

[Niels Voss]

The reason you can't project out the components of the integer is that whenever you use the data that the Quotient encapsulates you need to prove that the function respects the relation. If you had a function f which gets the first coordinate of ⟦(a,b)⟧ then you would have ⟦(1,2)⟧ = ⟦(3,4)⟧ but f ⟦(1,2)⟧ ≠ f ⟦(3,4)⟧, which is a contradiction. So to define a function g : integer -> X you need to both define a function h : ℕ × ℕ -> X and also prove that h respects int_equiv (then you use Quotient.lift, mentioned above). Defining a binary function is harder so you should use Quotient.map₂ as mentioned above.

[Peter Hansen]

Thanks for all the replies! Both for the tips and the explanation of why projections are not allowed. Concepts like quotient and setoids are very unfamiliar territory for me, but I think I managed to define both addition and multiplication using Quotient.map\_2

def add (a b : integer) : integer := by
  fapply @Quotient.map₂ (ℕ × ℕ) (ℕ × ℕ)
  · exact fun A B => (A.1 + B.1, A.2 + B.2)
  intro A B rAB C D rCD
  unfold instHasEquiv integer_setoid int_equiv
  dsimp
  rw [add_assoc, add_comm C.fst, add_assoc, add_comm D.snd]
  rw [add_assoc, add_comm D.fst, add_assoc, add_comm C.snd]
  rw [rCD, ← add_assoc, ← add_assoc, rAB, ← add_assoc, ← add_assoc]
  · exact a
  · exact b

def mul (a b : integer) : integer := by
  fapply @Quotient.map₂ (ℕ × ℕ) (ℕ × ℕ)
  · exact fun A B => (A.1 * B.1 + A.2 * B.2, A.1 * B.2 + A.2 * B.1)
  intro A B rAB C D rCD
  unfold instHasEquiv integer_setoid int_equiv
  dsimp
  rw [← @add_left_cancel_iff _ _ _  (B.fst * C.fst)]
  ring_nf

  rw [← mul_add, rCD, mul_add]
  rw [add_comm (B.fst * C.fst)]
  rw [add_assoc, add_assoc, add_assoc, add_assoc, add_assoc, add_assoc, add_left_cancel_iff]
  rw [← add_assoc, ← add_assoc, ← add_assoc, mul_comm _ C.fst, ← mul_add, ← rAB, mul_add]
  rw [add_comm (B.fst * C.snd)]
  rw [add_assoc, add_assoc, add_assoc, add_left_cancel_iff]
  rw [← add_assoc, mul_comm _ C.snd, mul_comm _ C.snd, ← mul_add, ← rAB, mul_add]
  rw [add_comm (C.fst * B.snd), mul_comm A.fst, add_assoc, add_assoc, add_left_cancel_iff]
  rw [mul_comm, ← mul_add, add_comm, ← rCD, mul_add, add_comm, mul_comm, mul_comm  C.fst]
  · exact a
  · exact b

Is there a tactic that would have made the task a bit easier? Also: at the moment #check 3 — 2 = 2 — 1 is shown in infoview as Quotient.mk integer_setoid (3, 2) = Quotient.mk integer_setoid (2, 1) : Prop. Is there a way to force a nicer notation?

[Kevin Buzzard]

IIRC nlinarith is quite good at solving all the goals that show up in the construction of the ring structure on the integers

[Peter Hansen]

Constructing a ring structure of my integers is the next big step :) But right now I just want to making working with my integers a bit more pleasant. As mentioned, #check 3 — 2 = 2 — 1 is shown in the Infoview as Quotient.mk integer_setoid (3, 2) = Quotient.mk integer_setoid (2, 1) : Prop. This obscures what is going on. Any ideas of how to deal with this? Maybe build a type on top my integers?

[Yury G. Kudryashov]

#mwe

[Peter Hansen]

Yury G. Kudryashov said:

#mwe

import Mathlib.Data.Equiv.Functor
import Mathlib.Tactic


def int_equiv (a b : ℕ × ℕ) : Prop :=
  a.1 + b.2 = b.1 + a.2

lemma int_equiv.refl : ∀ a : ℕ × ℕ, int_equiv a a := by
  intro a
  rfl

lemma int_equiv.symm : ∀ {a b : ℕ × ℕ}, int_equiv a b → int_equiv b a := by
  intros a b hab
  unfold int_equiv
  rw [hab]

lemma int_equiv.trans : ∀ {a b c : ℕ × ℕ}, int_equiv a b → int_equiv b c → int_equiv a c := by
  intros a b c hab hbc
  unfold int_equiv
  have : a.fst + b.snd + c.snd = c.fst + b.snd + a.snd := by
    rw [hab, ← hbc]
    ring
  rw [add_comm a.fst, add_comm c.fst, add_assoc, add_assoc] at this
  exact add_left_cancel this

def intEquiv : Equivalence int_equiv := {
  refl := .refl
  symm := .symm
  trans := .trans }

instance integer_setoid : Setoid (ℕ × ℕ) := {
  r := int_equiv
  iseqv := intEquiv }

def integer := Quotient integer_setoid

notation:65 lhs:65 " — " rhs:66 => (⟦(lhs, rhs)⟧ : integer)

#check 3 — 2 = 2 — 1

[Yury G. Kudryashov]

You can def integer.mk (a b : Nat) : integer := ⟦(a, b)⟧, then use integer.mk in infix

[Yury G. Kudryashov]

(not tested)

[Peter Hansen]

Yury G. Kudryashov said:

You can def integer.mk (a b : Nat) : integer := ⟦(a, b)⟧, then use integer.mk in infix

Seems to work beautifully!. Thanks :)

[Peter Hansen]

As mentioned, I would like to show my integers form a ring, so why not start with showing addition is commutative. This problem is with how add unfolds.

import Mathlib.Data.Equiv.Functor
import Mathlib.Tactic

def int_equiv (a b : ℕ × ℕ) : Prop :=
  a.1 + b.2 = b.1 + a.2

lemma int_equiv.refl : ∀ a : ℕ × ℕ, int_equiv a a := by
  intro a
  rfl

lemma int_equiv.symm : ∀ {a b : ℕ × ℕ}, int_equiv a b → int_equiv b a := by
  intros a b hab
  unfold int_equiv
  rw [hab]

lemma int_equiv.trans : ∀ {a b c : ℕ × ℕ}, int_equiv a b → int_equiv b c → int_equiv a c := by
  intros a b c hab hbc
  unfold int_equiv
  have : a.fst + b.snd + c.snd = c.fst + b.snd + a.snd := by
    rw [hab, ← hbc]
    ring
  rw [add_comm a.fst, add_comm c.fst, add_assoc, add_assoc] at this
  exact add_left_cancel this

def intEquiv : Equivalence int_equiv := {
  refl := .refl
  symm := .symm
  trans := .trans }

instance integer_setoid : Setoid (ℕ × ℕ) := {
  r := int_equiv
  iseqv := intEquiv }

def integer := Quotient integer_setoid

namespace integer

notation:65 lhs:65 " — " rhs:66 => Quot.mk Setoid.r (lhs, rhs)

def add (a b : integer) : integer := by
  fapply @Quotient.map₂ (ℕ × ℕ) (ℕ × ℕ)
  · exact fun A B => (A.1 + B.1, A.2 + B.2)
  intro A B rAB C D rCD
  unfold instHasEquiv integer_setoid int_equiv
  dsimp
  rw [add_assoc, add_comm C.fst, add_assoc, add_comm D.snd]
  rw [add_assoc, add_comm D.fst, add_assoc, add_comm C.snd]
  rw [rCD, ← add_assoc, ← add_assoc, rAB, ← add_assoc, ← add_assoc]
  · exact a
  · exact b

theorem add_comm (x y : integer) : add x y = add y x := by
  unfold add
  sorry

end integer

Is there any remediation for this or is this just (one of the reasons) why integers aren't defined as equivalence classes in Mathlib?

[Eric Wieser]

What's the problem?

[Peter Hansen]

Eric Wieser said:

What's the problem?

At the moment add unfold into Quotient.map₂ (fun A B => (A.fst + B.fst, A.snd + B.snd)) add.proof_1 x y = Quotient.map₂ (fun A B => (A.fst + B.fst, A.snd + B.snd)) add.proof_1 y x which doesn't seem very pleasant to work with. So unpleasant that I can't figure out to how to show commutativity (hence the sorry). How do i deal with this? Some sort of congruence argument?

[Kevin Buzzard]

Did you look at how I did this construction? I'm on mobile but I'm pretty sure I've formalised this in a few places

[Kevin Buzzard]

There are no problems doing it at all especially if you have access to the ring tactic to prove the auxiliary nat goals.

[Eric Wieser]

You'll need to induct on x and y, then dsimp should clean up the goal

[Peter Hansen]

Kevin Buzzard said:

Did you look at how I did this construction? I'm on mobile but I'm pretty sure I've formalised this in a few places

Are you referring to the version of the integers built into Lean? Or is there some alternative construction somewhere in Mathlib?

Eric Wieser said:

You'll need to induct on x and y, then dsimp should clean up the goal

How do I induct on x and y, when my integers are not an inductive type?

[Kevin Buzzard]

Are you referring to the version of the integers built into Lean?

No -- those integers are mathematically disgusting; they are optimised for computer scientists.

Or is there some alternative construction somewhere in Mathlib?

No! The whole point of mathlib is that you have one definition of everything, and we're using Lean so we're stuck with Lean's integers.

I'm referring to teaching materials such as https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/blob/master/src/section06quotients/sheet4Z.lean which work through the mathematical definition (unfortunately still in Lean 3 but before I teach the course again I'll translate everything into Lean 4).

[Eric Wieser]

How do I induct on x and y, when my integers are not an inductive type?

Induction also works on quotient types! Though you'll want to use induction x using Quotient.inductionOn to make sure it give you the spelling you want.

[Peter Hansen]

Kevin Buzzard said:

No! The whole point of mathlib is that you have one definition of everything, and we're using Lean so we're stuck with Lean's integers.

I'm referring to teaching materials such as https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/blob/master/src/section06quotients/sheet4Z.lean which work through the mathematical definition (unfortunately still in Lean 3 but before I teach the course again I'll translate everything into Lean 4).

That looks like exactly what I was trying to do. Thank you very much :)

Eric Wieser said:

How do I induct on x and y, when my integers are not an inductive type?

Induction also works on quotient types! Though you'll want to use induction x using Quotient.inductionOn to make sure it give you the spelling you want.

That worked!

theorem add_comm (x y : integer) : add x y = add y x := by
  induction x using Quotient.inductionOn
  induction y using Quotient.inductionOn
  apply Quotient.sound
  unfold instHasEquiv integer_setoid int_equiv
  ring_nf

Thanks for the tip.

[Peter Hansen]

So I have played around with my integers a bit further, and often run into a situation like this:

import Mathlib.Data.Equiv.Functor
import Mathlib.Tactic

def int_equiv (a b : ℕ × ℕ) : Prop :=
  a.1 + b.2 = b.1 + a.2

lemma int_equiv.refl : ∀ a : ℕ × ℕ, int_equiv a a := by
  intro a
  rfl

lemma int_equiv.symm : ∀ {a b : ℕ × ℕ}, int_equiv a b → int_equiv b a := by
  intros a b hab
  unfold int_equiv
  rw [hab]

lemma int_equiv.trans : ∀ {a b c : ℕ × ℕ}, int_equiv a b → int_equiv b c → int_equiv a c := by
  intros a b c hab hbc
  unfold int_equiv
  have : a.fst + b.snd + c.snd = c.fst + b.snd + a.snd := by
    rw [hab, ← hbc]
    ring
  rw [add_comm a.fst, add_comm c.fst, add_assoc, add_assoc] at this
  exact add_left_cancel this

def intEquiv : Equivalence int_equiv := {
  refl := .refl
  symm := .symm
  trans := .trans }

instance integer_setoid : Setoid (ℕ × ℕ) := {
  r := int_equiv
  iseqv := intEquiv }

def integer := Quotient integer_setoid

notation:65 lhs:65 " — " rhs:66 => Quot.mk Setoid.r (lhs, rhs)

theorem int_prod_pair (A : integer) : ∃ (a : (ℕ × ℕ)), A = (a.1 — a.2) := by
  induction A using Quotient.inductionOn
  simp
      -- CONTEXT
      -- case h
      -- a✝: ℕ × ℕ
      -- ⊢ ∃ a b, Quotient.mk integer_setoid a✝ = a — b
  sorry

-- EDIT solved it as

theorem int_prod_pair' (A : integer) : ∃ (a : (ℕ × ℕ)), A = (a.1 — a.2) := by
  fapply Quot.recOn A
  intro a
  use a
  intro B D P
  rfl

What is the meaning of the ✝- symbol? I have noticed that it also shows up when I accidentally use a variable name twice.

[Mauricio Collares]

That's the symbol for inaccessible names. An inacessible name like a✝ is "dead" in the sense that typing a in the current context does not resolve to the variable in the a✝ line, either because of shadowing or because of macro hygiene.

[Peter Hansen]

Mauricio Collares said:

That's the symbol for inaccessible names. An inacessible name like a✝ is "dead" in the sense that typing a in the current context does not resolve to the variable in the a✝ line, either because of shadowing or because of macro hygiene.

Thank you for the answer. I'm still a bit unsure of what exactly causes a variable to become inaccessible. Could you please elaborate just a bit on 'shadowing' and ' macro hygiene'?

[Kevin Buzzard]

You can't have two variables both called x. That's shadowing. If a tactic creates a variable and the user doesn't name it there and then, then the computer ensures that the user will never be able to talk about it explicitly. That's macro hygiene.

[Peter Hansen]

Kevin Buzzard said:

You can't have two variables both called x. That's shadowing. If a tactic creates a variable and the user doesn't name it there and then, then the computer ensures that the user will never be able to talk about it explicitly. That's macro hygiene.

Then how can I name it (from a dead state)?

[Kevin Buzzard]

First, you shouldn't be in the situation of having a dead variable which you want to use at all. If it's coming from macro hygiene then you should have named it when you ran the tactic. If it's coming from two variables having the same name you should have called them different names.

[Kevin Buzzard]

But there is a tactic called rename_i which you can use to name these dead variables. It's a code smell though.

[Mauricio Collares]

With the induction' tactic you can say induction' A using Quotient.inductionOn with my_name to choose a name yourself (which will be accessible)

[Peter Hansen]

Kevin Buzzard said:

First, you shouldn't be in the situation of having a dead variable which you want to use at all. If it's coming from macro hygiene then you should have named it when you ran the tactic. If it's coming from two variables having the same name you should have called them different names.

That explains very well. Thank you. Sometimes the correct tactics syntax can be a bit difficult to get right, I guess. At least I think it was easier to read the Lean3 documentation.

Mauricio Collares said:

With the induction' tactic you can say induction' A using Quotient.inductionOn with my_name to choose a name yourself (which will be accessible)

Thank you! I thought I had tried exactly just that, but turns out I had used induction and not induction'.

[Kevin Buzzard]

Sometimes the correct tactics syntax can be a bit difficult to get right, I guess. At least I think it was easier to read the Lean3 documentation.

You can see documentation for a tactic in Lean 4 by hovering over it, and in my experience Lean 4 tactics are documented better than Lean 3 ones. If you have a specific example of where something is unclear then please point it out -- or even better make a PR to fix it. Lean and mathlib are open source projects and the community genuinely wants to make the software better.