Defining ℤ in Lean

Stream: new members

[Isak Colboubrani]

For educational purposes, I aim to define the natural numbers, the integers, and addition in Lean.

I've defined the natural numbers as follows:

inductive nat where
  | zero : nat
  | succ (n : nat) : nat
open nat
instance : OfNat nat 0 where
  ofNat := zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where
  ofNat := succ (inferInstance : OfNat nat n).ofNat
def add : nat → nat → nat
  | a, 0 => a
  | a, succ b => succ (add a b)
example : add 1 2 = 3 := by rfl

I now wish to define the integers as the equivalence classes for the relation $(a, b) R(c, d) \Leftrightarrow a+d=b+c$. With say $-5$ representing the class with pairs such as $(1,6),(10,15)$, and similar.

What would be a succinct way to implement this in Lean?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

You could use docs4#Quotient. To do that, first construct an equivalence relation (docs4#Equivalence) over nat × nat. Then wrap that in a docs4#Setoid, and define int as the corresponding quotient.

[Gareth Ma]

I read somewhere that MLTT doesn't have quotient types? So what's happening here

[Jireh Loreaux]

Not without extra axioms it doesn't, but Lean has those. docs#Quot.sound

[Patrick Massot]

Jireh this is more than an extra axiom, in the sense that choice is an extra axiom: there is an extra reduction rule.

[Isak Colboubrani]

Thanks for the helpful hints!

This is my current attempt (#mwe):

inductive nat where
  | zero : nat
  | succ (n : nat) : nat
open nat
instance : OfNat nat 0 where
  ofNat := zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where
  ofNat := succ (inferInstance : OfNat nat n).ofNat
def add : nat → nat → nat
  | a, 0 => a
  | a, succ b => succ (add a b)
example : add 1 2 = 3 := by rfl

structure int_as_nat_pair where
  plus : nat
  minus : nat
def int_relation (x y : int_as_nat_pair) : Prop := add x.plus y.minus = add x.minus y.plus
theorem is_equivalence_relation : Equivalence int_relation := by sorry
instance int_setoid : Setoid int_as_nat_pair where
  r := int_relation
  iseqv := is_equivalence_relation
def int := Quotient int_setoid

Does this implementation look correct, aside from the unfinished proof?

[Kevin Buzzard]

Yes, although I would have used the [Add] notation typeclass and used the notation in the definition of the equivalence relation

[Isak Colboubrani]

Thanks! I'm now using Add.

This is my current #mwe:

inductive nat where
  | zero : nat
  | succ (n : nat) : nat
open nat
instance : OfNat nat 0 where
  ofNat := zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where
  ofNat := succ (inferInstance : OfNat nat n).ofNat
def nat.add : nat → nat → nat
  | a, 0 => a
  | a, succ b => succ (add a b)
instance : Add nat where
  add := nat.add
example : (1 : nat) + (2 : nat) = (3 : nat) := by rfl

structure int_as_nat_pair where
  plus : nat
  minus : nat
def int_relation (x y : int_as_nat_pair) := x.plus + y.minus = x.minus + y.plus
theorem is_equivalence_relation : Equivalence int_relation := by
  apply Equivalence.mk
  case refl => sorry
  case symm => sorry
  case trans => sorry
instance int_setoid : Setoid int_as_nat_pair where
  r := int_relation
  iseqv := is_equivalence_relation
def int := Quotient int_setoid

I'm not sure how to define int.add and create instances of int such as say int.zero ((0, 0)), int.one ((1, 0)) and int.minus_two ((0, 2)).

This is what I want to achieve:

def int.add : int → int → int := TODO
instance : Add int where
   add := int.add
def int.zero : int := TODO
def int.one : int := TODO
def int.minus_two : int := TODO
example : int.one + int.minus_two + int.one = int.zero := by sorry

Any hints?

[Eric Wieser]

You're looking for Quotient.mk _

[Isak Colboubrani]

Thank you for the hint!

I am now utilizing Quotient.mk _ to define int.zero, int.one, and others as follows:

def int.zero      : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 0 0)
def int.one       : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 1 0)
def int.two       : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 2 0)
def int.minus_one : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 0 1)
def int.minus_two : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 0 2)

Here is my definition for int.add:

def int.add (x y : int) : int :=
  Quotient.liftOn₂ x y (fun x y => Quotient.mk int_setoid (int_as_nat_pair.mk (x.plus + y.plus) (x.minus + y.minus))) sorry

Does it appear correct?

The following test cases behave as expected:

example : int.zero = int.zero := by rfl
example : int.zero + (int.zero + int.zero) = int.zero := by rfl
example : int.one + int.zero = int.one := by rfl
example : int.zero + int.minus_two = int.minus_two := by rfl
example : int.minus_two + int.zero = int.minus_two := by rfl
example : int.one + int.one = int.two + int.zero := by rfl
example : (int.zero + int.zero) + int.one = int.one := by rfl
example : (int.one + int.zero) + int.one = int.two := by rfl
example : (int.zero + int.minus_two) + int.zero = int.minus_two := by rfl
example : int.minus_one + int.minus_one = int.minus_two := by rfl
example : (int.zero + int.zero) + int.minus_two = int.minus_two := by rfl

However, these two do not:

example : (int.one + int.one) + int.minus_two = int.zero := by rfl
example : (int.one + int.minus_two) + int.one = int.zero := by rfl

I am unsure why: these two cases do not seem structurally different from the previous ones. What could be the issue?

This is a #mwe:

inductive nat where
  | zero : nat
  | succ (n : nat) : nat
open nat
instance : OfNat nat 0 where
  ofNat := zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where
  ofNat := succ (inferInstance : OfNat nat n).ofNat
def nat.add : nat → nat → nat
  | a, 0 => a
  | a, succ b => succ (add a b)
instance : Add nat where
  add := nat.add
example : (1 : nat) + (2 : nat) = (3 : nat) := by rfl
example : (1 : nat) + ((2 : nat) + (1 : nat)) = (3 : nat) + (1 : nat) := by rfl

structure int_as_nat_pair where
  plus : nat
  minus : nat
def int_relation (x y : int_as_nat_pair) := x.plus + y.minus = x.minus + y.plus
theorem int_relation_is_equivalence_relation : Equivalence int_relation := by
  apply Equivalence.mk
  case refl => sorry
  case symm => sorry
  case trans => sorry

instance int_setoid : Setoid int_as_nat_pair where
  r := int_relation
  iseqv := int_relation_is_equivalence_relation
def int := Quotient int_setoid

def int.zero      : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 0 0)
def int.one       : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 1 0)
def int.two       : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 2 0)
def int.minus_one : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 0 1)
def int.minus_two : int := (@Quotient.mk _) int_setoid (int_as_nat_pair.mk 0 2)

def int.add (x y : int) : int :=
  Quotient.liftOn₂ x y (fun x y => Quotient.mk int_setoid (int_as_nat_pair.mk (x.plus + y.plus) (x.minus + y.minus))) sorry

instance : Add int where
  add := int.add

example : int.zero = int.zero := by rfl
example : int.zero + (int.zero + int.zero) = int.zero := by rfl
example : int.one + int.zero = int.one := by rfl
example : int.zero + int.minus_two = int.minus_two := by rfl
example : int.minus_two + int.zero = int.minus_two := by rfl
example : int.one + int.one = int.two + int.zero := by rfl
example : (int.zero + int.zero) + int.one = int.one := by rfl
example : (int.one + int.zero) + int.one = int.two := by rfl
example : (int.zero + int.minus_two) + int.zero = int.minus_two := by rfl
example : int.minus_one + int.minus_one = int.minus_two := by rfl
example : (int.zero + int.zero) + int.minus_two = int.minus_two := by rfl
example : (int.one + int.one) + int.minus_two = int.zero := by sorry

[Isak Colboubrani]

I've revisited my implementation of $\mathbb{N}$ and $\mathbb{Z}$ (as $\mathbb{N} \times \mathbb{N}$), and now I'm obtaining the expected outcomes.

However, for some of my straightforward $\mathbb{Z}$ proofs that I assumed could be resolved using rfl, I find that I need to use apply Quotient.sound before rfl. I'm puzzled about what distinguishes the cases where only rfl is needed from those where apply Quotient.sound followed by rfl is required. Any suggestions? Am I overlooking any setup step that would enable me to bypass calling apply Quotient.sound even for these scenarios?

-- solvable by rfl only
example : (3 : int) * (-2 : int) = (-6 : int) := by rfl
example : ((1 : int) + (0 : int)) + (1 : int) = (2 : int) := by rfl
example : ((0 : int) + (-2 : int)) + (0 : int) = (-2 : int) := by rfl
example : ((1 : int) * (-1 : int)) + (-2 : int) = (-3 : int) := by rfl

-- solvable by Quotient.sound + rfl
example : (2 : int) + (-1 : int) = (1 : int) := by apply Quotient.sound; rfl
example : ((1 : int) + (1 : int)) + (-2 : int) = (0 : int) := by apply Quotient.sound; rfl
example : ((1 : int) + (-2 : int)) + (1 : int) = (0 : int) := by apply Quotient.sound; rfl
example : ((3 : int) * (-2 : int)) + (3 : int) = (-3 : int) := by apply Quotient.sound; rfl

Full #mwe:

-- define nat
inductive nat where
  | zero : nat
  | succ (n : nat) : nat

-- support nat literals
instance : OfNat nat 0 where ofNat := nat.zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where ofNat := nat.succ (inferInstance : OfNat nat n).ofNat

-- support nat add & mul
def nat.add (n1 n2 : nat) : nat := match n1, n2 with
  | n1, 0 => n1
  | n1, succ n2 => succ (add n1 n2)
instance : Add nat where add := nat.add
def nat.mul (n1 n2 : nat) : nat := match n1, n2 with
  | _, 0 => 0
  | n1, succ n2 => n1 + mul n1 n2
instance : Mul nat where mul := nat.mul

-- define int (nat x nat) as a quotient type
def int_pair : Type := nat × nat
def int_pair_relation (ab cd : int_pair) : Prop := ab.1 + cd.2 = cd.1 + ab.2
theorem int_pair_rel_is_equiv_rel : Equivalence int_pair_relation := by sorry
def int_pair_setoid : Setoid int_pair := Setoid.mk int_pair_relation int_pair_rel_is_equiv_rel
instance int_pair_setoid_instance : Setoid int_pair := int_pair_setoid
def int : Type := Quotient int_pair_setoid

-- support int add, mul & neg
def int.add (z1 z2 : int) : int := Quotient.liftOn₂ z1 z2 (fun x y => Quotient.mk int_pair_setoid (x.1 + y.1, x.2 + y.2)) sorry
instance : Add int where add := int.add
def int.mul (z1 z2 : int) : int := Quotient.liftOn₂ z1 z2 (fun x y => Quotient.mk int_pair_setoid (x.1 * y.1 + x.2 * y.2, x.1 * y.2 + x.2 * y.1)) sorry
instance : Mul int where mul := int.mul
def int.neg (z : int) : int := Quotient.liftOn z (fun x => Quotient.mk int_pair_setoid (x.2, x.1)) sorry
instance : Neg int where neg := int.neg

-- support int literals
def int.zero : int := Quotient.mk int_pair_setoid (0, 0)
def int.one : int := Quotient.mk int_pair_setoid (1, 0)
instance : OfNat int 0 where ofNat := int.zero
instance {n : Nat} [OfNat int n] : OfNat int (n + 1) where ofNat := (inferInstance : OfNat int n).ofNat + int.one

-- solvable by rfl only
example : (3 : int) * (-2 : int) = (-6 : int) := by rfl
example : ((1 : int) + (0 : int)) + (1 : int) = (2 : int) := by rfl
example : ((0 : int) + (-2 : int)) + (0 : int) = (-2 : int) := by rfl
example : ((1 : int) * (-1 : int)) + (-2 : int) = (-3 : int) := by rfl

-- solvable by Quotient.sound + rfl
example : (2 : int) + (-1 : int) = (1 : int) := by apply Quotient.sound; rfl
example : ((1 : int) + (1 : int)) + (-2 : int) = (0 : int) := by apply Quotient.sound; rfl
example : ((1 : int) + (-2 : int)) + (1 : int) = (0 : int) := by apply Quotient.sound; rfl
example : ((3 : int) * (-2 : int)) + (3 : int) = (-3 : int) := by apply Quotient.sound; rfl

[Eric Wieser]

rfl works when x.plus = y.plus and x.minus = y.minus. Quotient.sound rfl works when x.plus + y.minus = x.minus + y.plus.

[Isak Colboubrani]

Ah, now the pattern becomes clear to me. Thank you for pointing it out!

I'm currently pondering why my custom construction of int necessitates the use of apply Quotient.sound, whereas Lean's native Int construction does not require it:

-- My custom "int"
example : (2 : int) + (-1 : int) = (1 : int) := by apply Quotient.sound; rfl
-- Lean's Int
example : (2 : Int) + (-1 : Int) = (1 : Int) := by rfl

Considering the chosen Quotient construction I've employed here, is the use of apply Quotient.sound inevitable, or is there a method to enable Lean to penetrate through the quotient construction and permit rfl to function without the prerequisite of apply Quotient.sound?

[Kyle Miller]

I just want to mention a followup exercise you could do, once you've explored this one. The Quotient is there when you don't have a good choice for a quotient type, but quotients are defined using universal properties. If it's possible to choose a type, like for example taking a representative element per equivalence class, then you can use that as the quotient.

For example, you could use this for your quotient:

structure int where
  p : int_pair
  normalized : p.1 = 0 ∨ p.2 = 0

You would define int.mk : int_pair -> int as a replacement for Quotient.mk by subtracting one from both p.1 and p.2 so long as normalized is not true. The goal would be to replace each Quotient lemma with one specialized for this int.

[Kyle Miller]

Regarding your question, if you use the reduce tactic from Mathlib.Tactic.Common, you can see the issue. Put into Quotient syntax, the problem is that the goal is the same as Quotient.mk int_pair_setoid (2, 1) = Quotient.mk int_pair_setoid (1, 0).

example : (2 : int) + (-1 : int) = (1 : int) := by
  change Quotient.mk int_pair_setoid (2, 1) = Quotient.mk int_pair_setoid (1, 0)
  apply Quotient.sound
  change _ = _; dsimp only
  -- ⊢ 2 + 0 = 1 + 1
  rfl

That is, rfl doesn't succeed without Quotient.sound since (2, 1) is not equal to (1, 0).

[Kyle Miller]

This lack of normalization by the way is an issue for computations, since the numbers hidden inside the integers might keep growing without bound.

[Kyle Miller]

For fun, note that you can use metaprogramming to create a new tactic for doing rfl for int.

macro "zrfl" : tactic => `(tactic| (apply Quotient.sound; rfl))

example : (2 : int) + (-1 : int) = (1 : int) := by zrfl
example : ((1 : int) + (1 : int)) + (-2 : int) = (0 : int) := by zrfl
example : ((1 : int) + (-2 : int)) + (1 : int) = (0 : int) := by zrfl
example : ((3 : int) * (-2 : int)) + (3 : int) = (-3 : int) := by zrfl

[Kyle Miller]

With your OfNat instance, note that you can write it like

instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where
  ofNat := nat.succ (OfNat.ofNat n)

without need to to refer to fields of an instance obtained via inferInstance. (This is how it's intended to be written.)

[Kyle Miller]

If you insert an int normalization function in your arithmetic operations you can get the arithmetic to be by rfl.

def int_pair.normalize : int_pair → int_pair
  | (a, 0) => (a, 0)
  | (0, b) => (0, b)
  | (a + 1, b + 1) => int_pair.normalize (a, b)
  termination_by x => x.1

def int.normalize (z : int) : int :=
  Quotient.liftOn z (fun x => int.mk x.normalize) sorry

def int.add (z1 z2 : int) : int := int.normalize <|
  Quotient.liftOn₂ z1 z2 (fun x y => Quotient.mk int_pair_setoid (x.1 + y.1, x.2 + y.2)) sorry

You'll want this for proofs:

theorem int.normalize_eq (z : int) : z.normalize = z := sorry

[Kevin Buzzard]

The answer to "why doesn't Lean's Int need to use Quotient.sound is "Lean's Int was written by computer scientists not mathematicians, and hence is not defined as a quotient". This makes the API harder to develop but it makes computation more efficient or something

[Mario Carneiro]

You don't want to see what Int as written by computer scientists looks like

[Kevin Buzzard]

I meant a different kind of computer scientist

[Ruben Van de Velde]

Applied computer scientist

[Kyle Miller]

@Kevin Buzzard There's no harm in defining Int as a Quotient even for computation since you can make your Int.add/Int.mul/etc. evaluate to normal forms, where you're sure that the representative inside the Quotient.mk is such that one of the two numbers is zero.

Plus, since when have mathematicians insisted on a particular construction for a quotient? Aren't we happy with universal properties and choosing some set that can serve as "the" quotient? (I might even argue that Quotient is not the construction mathematicians have in mind when they think about the generic construction of a quotient-by-a-relation. There are no equivalence classes in sight. You could say that what's really going on is that Quotient is what happens if you replace Eq for one type with a coarser relation. That's to say, it's a mechanism to make it so that you can't tell the difference between certain elements anymore, and somehow the original elements are still there. Isak's questions about rfl vs Quotient.sound rfl point toward the fact that the underlying representatives still matter a whole lot.)

[Kevin Buzzard]

I'm totally happy with Lean's model of a quotient. I think the model in core is horrible because you end up with this pathological constructor which has no good properties. Making the API for Int like that is like going on a quest starting with a crappy sword. With the quotient definition everything instantly reduces to something which omega can solve and is often just an easy NNG level where you have access to all the Nat API. Whereas checking addition is associative in core involves numerous case splits, some of which use the theory of subNatNat : N -> N -> Z which needs to be developed first, including the fabulous theorem docs#Int.subNatNat_add_negSucc . In the quotient approach subNatNat is uncurried into quotient.mk and everything is so much easier.

[Kyle Miller]

Arguably core is forgetting to prove the universal property first. The definition in core "is" the quotient, but there's no API that lets you work with it as the quotient. Edit: I see, I missed subNatNat, which is the quotient map from N x N to Z.

[Kyle Miller]

Oh right, I just remembered that we've had this discussion before :smile:

[Isak Colboubrani]

Thank you @Kyle Miller for your valuable insights and code review. I learned a lot thanks to your feedback!

After introducing the suggested normalisation to one representative per equivalence class I'm able to solve the trivial theorems using only rfl (without apply Quotient.sound) which is great.

I think I've now implemented your suggestions with one exception: I'm unable to add the suggested constraint normalized : p.1 = 0 ∨ p.2 = 0 on int.

Here is my current setup:

structure int_pair where
  plus : nat
  minus : nat
def int_pair_setoid : Setoid int_pair := Setoid.mk int_pair_relation int_pair_rel_is_equiv_rel
def int : Type := Quotient int_pair_setoid

More specifically, I am unsure about the appropriate location for this constraint within the quotient structure. My understanding is that applying the constraint directly to int_pair would preclude the representation of non-normalized pairs. Would the solution involve creating an additional type int_pair_constrained that encompasses both an int_pair and the imposed constraint? What would be the best way to approach this?

Current #mwe:

-- define nat
inductive nat
  | zero : nat
  | succ (n : nat) : nat

-- support nat literals
instance : OfNat nat 0 where ofNat := nat.zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where ofNat := nat.succ (OfNat.ofNat n)

-- support nat add & mul
def nat.add (n1 n2 : nat) : nat := match n1, n2 with
  | n1, 0 => n1
  | n1, succ n2 => succ (add n1 n2)
instance : Add nat where add := nat.add
def nat.mul (n1 n2 : nat) : nat := match n1, n2 with
  | _, 0 => 0
  | n1, succ n2 => n1 + mul n1 n2
instance : Mul nat where mul := nat.mul

-- define int (nat x nat) as a quotient type
structure int_pair where
  plus : nat
  minus : nat
def int_pair.normalize : int_pair → int_pair
  | { plus := a, minus := 0 } => { plus := a, minus := 0 }
  | { plus := 0, minus := b } => { plus := 0, minus := b }
  | { plus := a + 1, minus := b + 1 } => int_pair.normalize { plus := a, minus := b }
  termination_by x => x.plus
def int_pair_relation (ab cd : int_pair) : Prop := ab.plus + cd.minus = cd.plus + ab.minus
theorem int_pair_rel_is_equiv_rel : Equivalence int_pair_relation := by sorry
def int_pair_setoid : Setoid int_pair := Setoid.mk int_pair_relation int_pair_rel_is_equiv_rel
instance int_pair_setoid_instance : Setoid int_pair := int_pair_setoid
def int : Type := Quotient int_pair_setoid
def int.normalize (z : int) : int :=
  Quotient.liftOn z (fun x => Quotient.mk int_pair_setoid x.normalize) sorry
def int.mk (z : int_pair) : int := int.normalize <| Quotient.mk int_pair_setoid z

-- support int add, mul & neg
def int.add (z1 z2 : int) : int := int.normalize <| Quotient.liftOn₂ z1 z2 (fun x y => Quotient.mk int_pair_setoid { plus := x.plus + y.plus, minus := x.minus + y.minus }) sorry
instance : Add int where add := int.add
def int.mul (z1 z2 : int) : int := int.normalize <| Quotient.liftOn₂ z1 z2 (fun x y => Quotient.mk int_pair_setoid { plus := x.plus * y.plus + x.minus * y.minus, minus := x.plus * y.minus + x.minus * y.plus }) sorry
instance : Mul int where mul := int.mul
def int.neg (z : int) : int := int.normalize <| Quotient.liftOn z (fun x => Quotient.mk int_pair_setoid { plus := x.minus, minus := x.plus }) sorry
instance : Neg int where neg := int.neg
@[simp] theorem int.normalize_eq (z : int) : z.normalize = z := sorry

-- support int literals
def int.zero : int := int.mk { plus := 0, minus := 0 }
def int.one : int := int.mk { plus := 1, minus := 0 }
instance : OfNat int 0 where ofNat := int.zero
instance {n : Nat} [OfNat int n] : OfNat int (n + 1) where ofNat := (OfNat.ofNat n) + int.one

-- now solvable by rfl only (previous solvable by Quotient.sound + rfl)
example : (2 : int) + (-1 : int) = (1 : int) := by rfl
example : ((1 : int) + (1 : int)) + (-2 : int) = (0 : int) := by rfl
example : ((1 : int) + (-2 : int)) + (1 : int) = (0 : int) := by rfl
example : ((3 : int) * (-2 : int)) + (3 : int) = (-3 : int) := by rfl

[Kyle Miller]

The idea is that once you add that normalization field, you can use that type as "the" quotient ("the" is in quotes because, taking an idea from category theory, a quotient Q of a type A is an type with a map A -> Q that satisfies the universal property of quotients).

Here's a start. What you'd do is create all the Quotient functions you had been using for the int type. I have int.mk' being the former Quotient.mk, and int.liftOn is the former Quotient.liftOn. Once you have all the basic Quotient functions and theorems defined, this int is a quotient type. (The Quotient type is necessary when you can't choose a normal form. In this version, you do not need to normalize after each operation because normalization occurs within int.mk'.)

structure int_pair where
  plus : nat
  minus : nat
structure int where
  pair : int_pair
  normalized : pair.plus = 0 ∨ pair.minus = 0
def int_pair.normalize (pair : int_pair) : int_pair :=
  match pair with
  | { plus := _, minus := 0 } | { plus := 0, minus := _ } => pair
  | { plus := a + 1, minus := b + 1 } => int_pair.normalize { plus := a, minus := b }
def int_pair_relation (ab cd : int_pair) : Prop := ab.plus + cd.minus = cd.plus + ab.minus
theorem int_rel_is_equiv_rel : Equivalence int_pair_relation := by sorry

theorem int_pair.normalize_normalized (p : int_pair) :
    p.normalize.plus = 0 ∨ p.normalize.minus = 0 := by
  induction p using int_pair.normalize.induct
  · simp [normalize]; exact Or.inr rfl
  · simp [normalize]; exact Or.inl rfl
  next ih => obtain ih | ih := ih <;> simp [normalize, ih]

def int.mk' (p : int_pair) : int := { pair := p.normalize, normalized := p.normalize_normalized }

def int.liftOn {α : Sort*} (z : int) (f : int_pair → α)
    (_ : ∀ p1 p2, int_pair_relation p1 p2 → f p1 = f p2) : α :=
  f z.pair

theorem int.liftOn_mk' {α : Sort*} (f : int_pair → α) (h) (p : int_pair) :
    int.liftOn (int.mk' p) f h = f p := by
  sorry

[Isak Colboubrani]

To implement rat.normalize, I need nat.gcd. Since I prefer to make everything self-contained for learning purposes, I want to avoid using Nat.gcd if possible.

Given the following #mwe, what would be a suitable minimal implementation of nat.gcd?

inductive nat
  | zero : nat
  | succ (n : nat) : nat
instance : OfNat nat 0 where ofNat := nat.zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where ofNat := nat.succ (OfNat.ofNat n)

-- def nat.gcd (n1 n2 : nat) : nat := ...

example : nat.gcd (100 : nat) (75 : nat) = (25 : nat) := by sorry

[Isak Colboubrani]

I found the following nat.gcd definition in the LeanDojo paper (page 5), and it appears to be taken from data/nat/gcd.leanin Lean 3. I've updated it to what I believe is the corresponding Lean 4 syntax:

def nat.gcd : nat → nat → nat
  | nat.zero, y => y
  | nat.succ x, y => nat.gcd (y % (nat.succ x)) (nat.succ x)

However, it seems like I'm missing the code necessary to convince Lean that this recursion will terminate. What am I missing? Did something change between Lean 3 and Lean 4 regarding recursion termination, or is my Lean 3 to Lean 4 port incorrect?

This is a #mwe:

-- define nat
inductive nat
  | zero : nat
  | succ (n : nat) : nat

-- support nat literals
instance : OfNat nat 0 where ofNat := nat.zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where ofNat := nat.succ (OfNat.ofNat n)

-- Temporarily implement nat.mod by using Nat.mod (to be fixed!).
-- Assume nat.mod exists for now.
def custom_nat_to_nat : nat → Nat
  | nat.zero => 0
  | nat.succ n => (custom_nat_to_nat n) + 1
def nat_to_custom_nat : Nat → nat
  | 0 => nat.zero
  | n + 1 => nat.succ (nat_to_custom_nat n)
def nat.mod (n1 n2 : nat) : nat :=
  let n1_nat : Nat := custom_nat_to_nat n1
  let n2_nat : Nat := custom_nat_to_nat n2
  n1_nat % n2_nat |> nat_to_custom_nat
instance : Mod nat where mod := nat.mod

def nat.gcd : nat → nat → nat
  | nat.zero, y => y
  | nat.succ x, y => nat.gcd (y % (nat.succ x)) (nat.succ x)

example : nat.gcd (100 : nat) (75 : nat) = (25 : nat) := by rfl

[Isak Colboubrani]

I successfully delayed the need to address this by directing Lean to assume, without verification, that the recursion will terminate (using decreasing_by sorry):

def nat.gcd : nat → nat → nat
  | nat.zero, y => y
  | nat.succ x, y => nat.gcd (y % (nat.succ x)) (nat.succ x)
decreasing_by sorry

I'm still curious about what changes, if any, occurred between Lean 3 and Lean 4 regarding the requirement to prove recursion termination.