happy function, restricting function inputs

Stream: new members

[Angela Li]

Hello! I'm trying to define a function that takes 3 natural numbers so that p > 0 and b > 1.

def happyfunction (p : ℕ+) (b : ℕ) : ℕ → ℕ
| n := ((digits b n).map (λ d, d^p)).sum

Would it be better to have (p : ℕ+) like I have right now or have {p : ℕ} (hp : p > 0)? Currently, I have to add

def pow (n : ℕ) (p : ℕ+) : ℕ := nat.pow n p
instance : has_pow ℕ ℕ+ := ⟨pow⟩

This is my first time using instance and I was also trying to restrict b using a set def B := set.Ioi (1 : ℕ) then (b : B) but it gave me the following errors when I tried #eval happyfunction 2 10 8:

111:23: failed to synthesize type class instance for
⊢ has_one ↥B

111:23: failed to synthesize type class instance for
⊢ has_add ↥B

I'm not sure how to solve this since B does not include one. Would it be better to just have (hb : b > 1)?
I would like to just be able to pass numbers in since I will mostly be working with p=2 and b=2,4,6,10, so if I have the hypotheses instead of using the sets, would Lean know automatically that 10 > 1 by norm_num?

Also, slightly random, but what is the difference between (b : B) and (b ∈ B)? And what does ↥ mean?
Anyways, thank you so much and I hope this was not too many questions.

[Kevin Buzzard]

There's not much of an API for N+, it might be easier using N

[Kevin Buzzard]

The problem you're running into is that if Lean sees 10 : B then it tries to figure out a map from the naturals to B and then evaluates it at 10, and we're failing at the first hurdle here.

[Kevin Buzzard]

A term of type B is a pair consisting of a natural, and a proof that the natural is in the required range, so you will have to give that to Lean directly to avoid this problem

[Kevin Buzzard]

import tactic

def B := set.Ioi 1

example : B := ⟨2, show 1 < 2, by linarith⟩

[Kevin Buzzard]

set nat is a type. B : set nat is a term. So b : B doesn't make sense. But Lean figures that if you want to talk about b : B i.e. if you want to make B into a type, you probably mean the subtype corresponding to B, and that little funny arrow indicates the transformation of B from a set to a subtype.

[Kevin Buzzard]

The idiomatic way to do all this in type theory is just to define stuff anyway, not worry about edge cases like b=1, and make a mental note that if you attempt to evaluate your function at a junk input, expect a junk output.

import tactic

import data.nat.digits

def happyfunction (p : ℕ) (b : ℕ) : ℕ → ℕ
| n := ((digits b n).map (λ d, d^p)).sum

[Kevin Buzzard]

things like digits will just give junk answers for small b, but you promise not to evaluate this function at small b, right?

[Kevin Buzzard]

Lean will happily accept 1/0, and for all I know it gives the answer 37, but I'm a mathematician so I never divide by 0.

[Angela Li]

Ohh okay that makes more sense. Thank you so much! Yes I'm only going to evaluate for b > 1

[Angela Li]

Also, would it be worth expanding the N+ API? I'm not too sure what I'm doing right now since I don't have that much math background haha.

[Kevin Buzzard]

You're the second person to ask this recently. The argument against is that if 0 can just tag along and give junk values most of the time, then maybe that's fine. The API for nat is huuge.