# Zulip Chat Archive

## Stream: new members

### Topic: happy function, restricting function inputs

#### Angela Li (Jun 26 2020 at 15:42):

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 (Jun 26 2020 at 15:43):

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

#### Kevin Buzzard (Jun 26 2020 at 15:45):

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 (Jun 26 2020 at 15:45):

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 (Jun 26 2020 at 15:48):

```
import tactic
def B := set.Ioi 1
example : B := ⟨2, show 1 < 2, by linarith⟩
```

#### Kevin Buzzard (Jun 26 2020 at 15:49):

`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 (Jun 26 2020 at 15:51):

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 (Jun 26 2020 at 15:52):

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 (Jun 26 2020 at 15:52):

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 (Jun 26 2020 at 15:52):

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

#### Angela Li (Jun 26 2020 at 15:53):

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 (Jun 26 2020 at 15:54):

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.

Last updated: May 11 2021 at 22:14 UTC