How to lift a binary function to a quotient?

Question

Kia ora :)

I am trying to use Quot. in Lean4 to define the integers as the quotient of the Cartesian product of two copies of the natural numbers (type Peano) under the relation:

def rel (x y : Peano × Peano) : Prop :=
  (fst x) + (snd y) = (fst y) + (snd x)

I have proved that this is an equivalence relation. Furthermore I have shown that the following binary operation on pairs of natural numbers:

def sum (x y : Peano × Peano) : Peano × Peano :=
  ((fst x) + (fst y), (snd x) + (snd y))

instance : Add (Peano × Peano) where
  add := sum

lifts to the quotient by proving the following theorem:

theorem sum_lifts (a b c d : Peano × Peano) : (rel a b) ∧ (rel c d) →  rel (a+c) (b+d) :=
  by << PROOF OMITTED >>>

I then make the following definition of the integers. But Lean is unhappy with the way I define sum_int on the integers.

def ℤ := Quot rel

def sum_int (a b : ℤ) : ℤ := Quot.lift sum sum_lifts

instance : Add ℤ where
  add := Quot.lift sum sum_lifts

I see the code in TPIL4 only describes how to lift unary functions to the quotient. How can it be altered for binary functions?

Thanks for the help!

Side question: is it usual to say something lifts to the quotient? I normally hear people saying this-or-that descends to the quotient. Am I upside down?

Answer 1

You are encountering two challenges related to the fact that the interface for Quot in base Lean is rather weak:

• Quot.lift is not intended to directly create a function f : Quot r -> Quot r. It is intended to create a function f : Quot r -> A for some type A where A need not be a quotient type. So your congruence lemma sum_lifts is not of the right form to use Quot.lift. It needs to end in an equality, not an equivalence.
• Quot.lift is for functions of one argument. Expanding it to two arguments requires a bit of type-theoretic gymnastics.

There are four ways to do this depending if you are want to use Mathlib and if you want to use Quot or Quotient.

But all of them follow the following approach:

• Find the library function which gives you what you need.
• Work backwards, providing the inputs you need of the correct types.

Boilerplate

All my examples will use this variation of your code.

import Mathlib.Data.Quot  -- only need for methods 2 and 4

def Peano := Nat
instance : Add Peano where
  add := fun x y => Nat.add (x : Nat) (y : Nat)

-- Instead of Peano × Peano, we will use a custom structure, but it doesn't matter
structure PreInt where
  fst : Nat
  snd : Nat

def PreInt.rel (x y : PreInt) : Prop :=
  x.fst + y.snd = x.fst + y.snd

def PreInt.sum (x y : PreInt) : PreInt :=
  PreInt.mk (x.fst + y.snd) (x.snd + y.fst)

theorem PreInt.sum_congr (a b c d : PreInt) : rel a b → rel c d → rel (sum a c) (sum b d) :=
  by sorry

Method 1. Use Quot.lift in base Lean

If you just want to use base Lean, you can use Quot to define the space:

def Int₁ := Quot PreInt.rel

and then use Quot.lift to make the function.

Before getting to a function of two arguments, let's do a function of one argument (negation) as an example. Most importantly, our lift lemma needs an equality at the end, not an equivalence, so we need to work with an intermediate function which goes from PreInt to Int₁.

def PreInt.neg (a : PreInt) : PreInt := PreInt.mk a.snd a.fst
theorem PreInt.neg_congr (a b : PreInt) : rel a b → rel (neg a) (neg b) :=
  by sorry

-- as an intermediate need function from `PreInt` to `Int₁`
def Int₁.negAux (a : PreInt) : Int₁ := Quot.mk PreInt.rel (PreInt.neg a)

-- lift lemma uses equality, not the relation `PreInt.rel`
theorem Int₁.negAux_lifts (a b: PreInt) : PreInt.rel a b → negAux a = negAux b := by
   intro h
   -- use Quot.sound to reduce to congruence property
   apply Quot.sound
   apply PreInt.neg_congr
   apply h

def Int₁.neg (a : Int₁) : Int₁ := Quot.lift negAux negAux_lifts a

For two arguments, it is the same idea, but we need two intermediate functions, one of type PreInt -> PreInt -> Int₁, and the other of type PreInt -> Int₁ -> Int₁:

def Int₁.sumAux (a b : PreInt) : Int₁ := Quot.mk PreInt.rel (PreInt.sum a b)

theorem Int₁.sumAux_lifts (a b₁ b₂: PreInt) : PreInt.rel b₁ b₂ → sumAux a b₁ = sumAux a b₂ := by
   intro h
   apply Quot.sound
   apply PreInt.sum_congr
   . rfl
   . apply h

def Int₁.sumAux' (a : PreInt) : Int₁ -> Int₁ := Quot.lift (sumAux a) (Int₁.sumAux_lifts a)

theorem Int₁.sumAux'_lifts (a₁ a₂ : PreInt) : PreInt.rel a₁ a₂ → sumAux' a₁ = sumAux' a₂ := by
  intro h
  -- function extensionality to make it sumAux' a₁ b = sumAux' a₂ b
  apply funext
  intro b
  -- Quot.ind is like cases/induction where we replace a quotient with its inner parts
  apply Quot.ind _ b
  intro b'
  apply Quot.sound
  apply PreInt.sum_congr
  . apply h
  . rfl

def Int₁.sum (a : Int₁) : Int₁ → Int₁ := Quot.lift Int₁.sumAux' Int₁.sumAux'_lifts a

Method 2: Use Quot.map₂ in Mathlib

The above gymnastics are just boilerplate, and it is easy to replace Quot.lift it with a custom operator designed specifically for building a function which maps two quotient spaces into a third quotient space. This is what Quot.map₂ does.

theorem PreInt.sum_congr_right (a : PreInt) (b₁ b₂: PreInt) : rel b₁ b₂ → rel (sum a b₁) (sum a b₂) := by
  apply PreInt.sum_congr
  rfl

theorem PreInt.sum_congr_left (a₁ a₂: PreInt) (b : PreInt) : rel a₁ a₂ → rel (sum a₁ b) (sum a₂ b) := by
  intro h
  apply PreInt.sum_congr
  . apply h
  . rfl
  
def Int₁.sum' (a b : Int₁ ) : Int₁ :=
  Quot.map₂ PreInt.sum PreInt.sum_congr_right PreInt.sum_congr_left a b

Method 3: Use Quotient.lift₂ in base Lean

Quotient is like Quot except it requires that the relation is an equivalence relation. Also, it works on Setoid types, which is just a fancy name for a type with an equivalence relation.

theorem PreInt.rel_is_equiv : Equivalence rel :=
  by sorry  -- supply proof here

instance PreInt.preIntSetoid : Setoid (PreInt) where
  r     := rel
  iseqv := rel_is_equiv

def Int₂ := Quotient (PreInt.preIntSetoid)

Then Quotient has lift₂ for functions of two arguments so that helps with some of the boilerplate (but since this is still lift, we have to still make an auxiliary function).

def Int₂.sumAux (a b : PreInt) : Int₂ := Quotient.mk' (PreInt.sum a b)

theorem Int₂.sumAux_lifts (a b c d : PreInt) : a ≈ c -> b ≈ d -> Int₂.sumAux a b = Int₂.sumAux c d := by
  intro h1 h2
  apply Quotient.sound
  apply PreInt.sum_congr
  . apply h1
  . apply h2

def Int₂.sum (a b : Int₂) : Int₂ := Quotient.lift₂ Int₂.sumAux Int₂.sumAux_lifts a b

Method 4. Use Quotient.map₂' in Mathlib

This is similar to Quot.map₂ but with a slightly different interface. The theorem you need to prove looks complicated, but it is just using fancy symbols for simple concepts.

theorem PreInt.sum_congr' : (Setoid.r ⇒ Setoid.r ⇒ Setoid.r) PreInt.sum PreInt.sum := by
  -- remove the fancy LiftFun notation and then follow your nose
  rw [Relator.LiftFun]
  intro a b h1
  rw [Relator.LiftFun]
  intro a1 b1 h2
  apply PreInt.sum_congr
  . apply h1
  . apply h2

def Int₂.sum' (a b : Int₂) : Int₂ := Quotient.map₂' PreInt.sum PreInt.sum_congr' a b