Defining a function on the non-zero positive integers

Stream: lean4

[Subhajit Bandyopadhyay]

Hi all. I am new to LEAN. So please bear with me if this question is too basic. I have been able to define functions on the natural numbers. But I need to define an arithmetic function, that is, a function that acts on the non-zero positive integers and inherit all the properties of the natural numbers (addition, multiplication etc) naturally. Is there a type for positive integers? If not, how do I approach the arithmetic functions in lean?

[Eric Wieser]

Are you aware of docs#ArithmeticFunction ?

[Yury G. Kudryashov]

About positive integers: docs#PNat

[Subhajit Bandyopadhyay]

Eric Wieser said:

Are you aware of docs#ArithmeticFunction ?

I was not aware of this library. Thank you for pointing this out.

[Subhajit Bandyopadhyay]

Yury G. Kudryashov said:

About positive integers: docs#PNat

I tried to use this. But I got a "failed to synthesize instance" error in the following definition of a function.

def pow_of_two_factor (n : ℕ+) : ℕ :=
  if n%2 = 1 then
    0
  else
    1 + pow_of_two_factor (n/2)

[Yury G. Kudryashov]

You should try if (n : Nat) % 2 = 1, otherwise it tries to find an instance for Mod on PNat and fails.

[Eric Wieser]

Note this function exists already, I think it's docs#Nat.log

[Richard Copley]

docs#Nat.maxPowDiv 2

[Eric Wieser]

I guess we should link that to docs#Nat.floorRoot in the docs somehow, cc @Yaël Dillies

[Yaël Dillies]

This is not the same?

[Yaël Dillies]

maxPowDiv corresponds to padicValNat, not floorRoot

[Eric Wieser]

Aren't they related as log is to nthRoot? Or alternatively, by flipping the arguments to ^? I guess I'm surprised to use floor used in one name but max in the other.

[Eric Wieser]

(I'm not suggesting we merge them, only make the names more similar)

[Yaël Dillies]

Eric Wieser said:

Aren't they related as log is to nthRoot?

Yes, that's correct

[Eric Wieser]

What I'm suggesting then is to unify the floor/max parts of the name