Zulip Chat Archive

Stream: new members

Topic: happy function, restricting function inputs


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:43):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 15:48):

import tactic

def B := set.Ioi 1

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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