Alternate Int Hierarchy

Stream: lean4

[Mac]

I am not sure whether or not this belongs here or in a different channel. However, I am writing it in Lean 4 so I am sticking it here. If it should go elsewhere, feel free to move it.

I was exploring alternate definitions of Nat/Int and was curious if anyone saw any immediate flaws with this definition of numbers:

namespace AltInt

inductive PNat
| one
| succ : PNat -> PNat

def Nat := Option PNat

inductive Dipole (A : Type u)
| neg : A -> Dipole A
| pos : A -> Dipole A

def NzInt := Dipole PNat
def Int := Option NzInt

In particular, I am curious as to why Lean 4 proper doesn't go the Int := zero | pos PNat | neg PNat route for integers since that seems a lot simpler tan the Int := ofNat Nat | negSucc Nat that is currently used.

It also allows for the following definition of natural (truncating) division (which I think is correct -- haven't proven it yet though) that seems much simpler than what is currently used in core (for one, it uses structural rather than well-founded recursion):

-- using the defs above

namespace Nat

@[matchPattern] def zero : Nat := none
@[matchPattern] def nonzero : PNat -> Nat := some
@[matchPattern] def one : Nat := some PNat.one

@[matchPattern]
def succ : Nat -> Nat
| zero => one
| nonzero n => nonzero (PNat.succ n)

end Nat

namespace PNat

def succSubDivTrunc :  PNat -> PNat -> PNat -> Nat
| one, one, _ => Nat.one
| one, succ _, _ => Nat.zero
| succ m, one, n => Nat.succ (succSubDivTrunc m n n)
| succ m, succ r, n => succSubDivTrunc m r n

def divTrunc (m n : PNat) : Nat :=
  succSubDivTrunc m n n

end PNat

Any comments, insights, etc.? They would be much appreciated.

[Kevin Buzzard]

I'm surprised that you say a construction with three constructors is "a lot simpler" than a construction with two constructors. How are you going to prove associativity of addition using the three-constructor definition -- you have 27 cases to deal with I guess.

[Mac]

Kevin Buzzard said:

I'm surprised that you say a construction with three constructors is "a lot simpler" than a construction with two constructors. How are you going to prove associativity of addition using the three-constructor definition -- you have 27 cases to deal with I guess.

The constructors are nested though. So you prove associativity for the levels separately, greatly reducing the number of cases. You can then use the inner proofs in the proofs of the outer cases.

[Mac]

For example, for Nat, you can show that a + b + nonzero c = nonzero (a + b + c) and then use the associative property for PNat add to prove associativity for Nat.

[Yakov Pechersky]

Then why even define PNat (for the definition of Int), when it is clearly isomorphic to Nat?

[Mac]

Yakov Pechersky said:

Then why even define PNat (for the definition of Int), when it is clearly isomorphic to Nat?

Because it is in many cases semantically different? For example, the divTrunc definition wouldn't work for Nat. Sure I could pretend thatNat's zero meant one, but that conceptual disconnect seems undesirable. Mathlib (version 3 at least) also defines a pnat (though that definition is propositional), so a desire for the conceptual distinction seems reasonable.

[David Renshaw]

(deleted)

[Brandon Brown]

I was trying to do something similar ​as well as I found it more elegant

open Nat

inductive int : Type where
| zero : int
| pos_succ : Nat → int
| neg_succ : Nat → int

open int

/-
`pos_succ (Nat.zero)` is the representation of +1
`neg_succ (Nat.zero)` is the representation for -1
-/

def int.incr (a : int) :=
 ​match a with
 ​| int.zero => pos_succ (Nat.zero)
 ​| pos_succ a => pos_succ (a.succ)
 ​| neg_succ b =>
   ​match b with
   ​| Nat.zero => int.zero
   ​| succ b => neg_succ b

#reduce (neg_succ 2).incr.incr.incr.incr.incr

def int.decr (a : int) :=
 ​match a with
 ​| int.zero => neg_succ (Nat.zero)
 ​| neg_succ a => neg_succ (a.succ)
 ​| pos_succ b =>
   ​match b with
   ​| Nat.zero => int.zero
   ​| succ b => pos_succ b

#reduce (pos_succ 1).decr.decr.decr.decr

def add_int_Nat (a : int) (b : Nat)  : int :=
 ​match b with
 ​| Nat.zero => a
 ​| succ b => add_int_Nat a.incr b

def sub_int_Nat (a : int) (b : Nat)  : int :=
     ​match b with
     ​| Nat.zero => a
     ​| succ b => sub_int_Nat a.decr b

def add (a b : int) : int :=
 ​match a with
 ​| int.zero => b
 ​| pos_succ a => add_int_Nat b a.succ
 ​| neg_succ a => sub_int_Nat b a.succ

#reduce add (pos_succ 5) (neg_succ 2) -- pos_succ 2

And I am indeed struggling to prove associativity

[Reid Barton]

One approach is to, regardless of the specific definition of int, start by defining its eliminator based on an equiv, and prove it satisfies the correct equations. After that, there will be no more case analyses. Now you can define add and mul.

[Reid Barton]

You also need to prove int.incr and int.decr form an equiv first.

[Brandon Brown]

I'm still at a pretty basic level... I get that incr and decr can form an equiv, but can you unpack the part about defining an eliminator based on an equiv a bit more?

[François G. Dorais]

There is no need for a new type, you can do this type of matching on Int itself!

@[matchPattern] abbrev Int.posSucc (n : Nat) := ofNat n.succ

def Int.incr : Int → Int
| posSucc n => posSucc (n+1)
| 0 => posSucc 0
| negSucc 0 => 0
| negSucc (n+1) => negSucc n

And so on...

[Kevin Buzzard]

My guess is that Reid is suggesting that given a type X, a term z : X and an equiv X ~= X you can get a map from int to X -- and furthermore this classifies int up to unique isomorphism as an initial object.

[Reid Barton]

Yes that's right. Something like docs#nat.iterate but with an equiv as the input.
The key point is that if $e$ is an equiv, then $e(e^n(x)) = e^{n+1}(x)$ holds not just for positive $n$ (by definition) but also for negative $n$--this uses the equations of $e$--and likewise $e^{-1}(e^n(x)) = e^{n-1}(x)$ also for positive $n$.

[Reid Barton]

Then you can combine this with an induction principle like "if P(0) and P(n) => P(n+1) and P(n) => P(n-1) then P(n) holds for all n" and never worry again about whether numbers are positive or negative.

[Reid Barton]

The difficulty with giving a direct by-cases definition of add and running with it is that you will know by definition that (say) a + (b + 1) = (a + b) + 1 when b is positive, but not when it's negative. So you end up with cases everywhere, and you will have to use the fact that succ and pred cancel manually.

[Reid Barton]

I have to go for now but I can try to write up something later if it remains unclear.

[Kevin Buzzard]

If it helps, here's a little API for int.iterate which we wrote at Imperial as part of a group theory project: https://github.com/ImperialCollegeLondon/group-theory-game/blob/152ec4a92ad67b6174a3d240c63fa56a6df6017e/src/int/iterate.lean

[Reid Barton]

Right, this sort of thing is what I had in mind but you might need to organize some things a bit differently if you don't have int.add yet.

[Brandon Brown]

Is this similar to well founded recursion by ordering the integers like 0, -1, 1, -2, 2 etc ?

[François G. Dorais]

A similar trick to the one I mentioned above works for simulating the inductive definition of Int in terms of positive integers as @Mac originally intended. The additional cost is a weird definition of positive integers as follows.

def Pos := Nat

namespace Pos

protected def one : Pos := Nat.zero

instance : OfNat Pos (nat_lit 1) := ⟨Pos.one⟩

protected def succ : Pos → Pos := Nat.succ

protected def add : Pos → Pos → Pos :=
  λ (x y : Nat) => Nat.succ (Nat.add x y)

instance : Add Pos := ⟨Pos.add⟩

protected def mul : Pos → Pos → Pos :=
  λ (x y : Nat) => Nat.add (Nat.mul x y) (Nat.add x y)

instance : Mul Pos := ⟨Pos.mul⟩

end Pos

Then this works:

@[matchPattern] abbrev Int.ofPos : Pos → Int := λ (n : Nat) => Int.ofNat n.succ
@[matchPattern] abbrev Int.negOfPos : Pos → Int := λ (n : Nat) => Int.negSucc n

def Int.decr : Int → Int
| ofPos (n + 1) => ofPos n
| ofPos 1 => 0
| 0 => negOfPos 1
| negOfPos n => negOfPos (n+1)

In other words, we can always pretend Int is defined as @Mac wants

inductive Int : Type
| zero : Int
| ofPos : Pos → Int
| negOfPos : Pos → Int

or as @Brandon wants

inductive Int : Type
| zero : Int
| posSucc : Nat → Int
| negSucc : Nat → Int

even though the real definition of Int is actually

inductive Int : Type
| ofNat : Nat → Int
| negSucc : Nat → Int

[Brandon Brown]

That's an interesting trick, François

[Mac]

François G. Dorais said:

In other words, we can always pretend Int is defined as @Mac wants

inductive Int : Type
| zero : Int
| ofPos : Pos → Int
| negOfPos : Pos → Int

This is a neat trick! :)

However, it largely defeats the purpose of the original definition. The point of the original definition is to all for the conditions of nonzero/positive/negative to be defined structurally at type level rather than via an attendant proof.

That is, with my alternate definition, you would no longer need conditions like h : a /= 0 or h : a > 0 you could just pass a NzInt or PNat and be guaranteed that by the type. You can, of course, simulate this by creating a new bundle type that bundles a Nat/Int but that has annoying implications when in proofs and pattern matches as the type is now much more structurally complex and a lot of thing snow have to be proved rather than just holding structurally.

The use of the Option (or an equivalent Zeroid a := zero | nonzero a type) provides similar structural benefits to proofs/definitions and allows for easy generalization among multiple possibly zero types (i.e., Nat, Int, Rat, etc.). While a zero monoid also does the latter, Zeroid does it structurally, which is useful in many cases.