## Stream: new members

### Topic: recursive function from \N

#### Li Xuanji (Jun 03 2020 at 05:49):

Hi, I've defined this function aspos_num \to \Z, but can't figure out how to define it from \N to \Z without going through pos_num

def J_joseph : pos_num → ℤ
| 1 := 1
| (pos_num.bit0 n) := 2*(J_joseph n) - 1     -- J(2*n)   = 2*J(n) - 1
| (pos_num.bit1 n) := 2*(J_joseph n) + 1     -- J(2*n+1) = 2*J(n) + 1


#### Johan Commelin (Jun 03 2020 at 05:58):

@Li Xuanji What is pos_num?

#### Mario Carneiro (Jun 03 2020 at 05:58):

binary positive natural numbers

#### Johan Commelin (Jun 03 2020 at 05:59):

I can guess... that it's positive numbers :wink: But I've never seen that type before

Aah... :bulb:

it's in mathlib

#### Johan Commelin (Jun 03 2020 at 06:00):

@Li Xuanji I don't think it's easy to define that as function on \N using recursion. But you can use if .. then .. else ..

#### Mario Carneiro (Jun 03 2020 at 06:00):

You can use nat.binary_rec_on to do binary definitions on nat directly

#### Johan Commelin (Jun 03 2020 at 06:01):

I guess I can go back to bed... I've already learned enough new stuff for a day, and I haven't even had breakfast yet.

thanks!

#### Li Xuanji (Jun 03 2020 at 06:03):

wait where's binary_rec_on defined?

#### Li Xuanji (Jun 03 2020 at 06:04):

ah I guess it got renamed to binary_rec

#### Mario Carneiro (Jun 03 2020 at 06:10):

Alternatively:

import data.num.lemmas

def J_joseph : pos_num → ℤ
| 1 := 1
| (pos_num.bit0 n) := 2*(J_joseph n) - 1     -- J(2*n)   = 2*J(n) - 1
| (pos_num.bit1 n) := 2*(J_joseph n) + 1     -- J(2*n+1) = 2*J(n) + 1

def J_joseph₁ : ℕ → ℤ
| 0 := 0
| (n+1) := J_joseph (n:num).succ'

#eval (list.range 20).map J_joseph₁
-- [0, 1, 1, 3, 1, 3, 5, 7, 1, 3, 5, 7, 9, 11, 13, 15, 1, 3, 5, 7]

def J_joseph₂ (n : ℕ) : ℤ := (2 * n + 1) - (2 ^ nat.size n : ℕ)

#eval (list.range 20).map J_joseph₂
-- [0, 1, 1, 3, 1, 3, 5, 7, 1, 3, 5, 7, 9, 11, 13, 15, 1, 3, 5, 7]

example : J_joseph₁ = J_joseph₂ := sorry


can you prove it?

#### Li Xuanji (Jun 03 2020 at 06:15):

yeah, I'm trying to prove the same closed form of J_joseph

#### Li Xuanji (Jun 03 2020 at 06:15):

but I found that some of the tactics I learned for nat doesn't work for pos_num

#### Mario Carneiro (Jun 03 2020 at 06:15):

You can also use nat.binary_rec for doing induction in binary

#### Mario Carneiro (Jun 03 2020 at 06:16):

induction on pos_num should work fine

#### Li Xuanji (Jun 03 2020 at 06:16):

yeap induction worked

#### Li Xuanji (Jun 03 2020 at 06:16):

let me look up what failed

#### Li Xuanji (Jun 03 2020 at 06:30):

sry that took a while; I wanted to do cases n to prove the goal

n : pos_num,
l : ℕ,
h1 : n = pos_num.of_nat_succ l,
h2 : pos_num.of_nat 2 > n
⊢ l = 0


#### Li Xuanji (Jun 03 2020 at 06:36):

with your definition of J_joseph₁  it works much better

#### Kevin Buzzard (Jun 03 2020 at 07:01):

@Johan Commelin I learnt about pos_num at Lean Together 2019 during the dinner. I sat next to Seul Baek and my initial reaction was "oh no, a computer scientist, whatever do we have in common to talk about?" but then we got talking about easy automation and then about proofs involving naturals, and then I went back to my hotel room and spent some time looking at this part of mathlib. At some point in the dinner I realised that it was a theorem that "column addition" (as taught to an 9 year old) agreed with natural number game addition, and after the dinner I went back to my hotel room and proved that the canonical map from posnum to nat was a morphism of additive semigroups.

#### Kevin Buzzard (Jun 03 2020 at 07:01):

It's a proof that the addition beloved of computer scientists is actually the correct addition!

#### Li Xuanji (Jun 03 2020 at 07:37):

don't think I'll get to it anytime soon, but the next recurrence to formalize is like J_joseph except using other bases

#### Mario Carneiro (Jun 03 2020 at 07:49):

Unfortunately I don't think mathlib can help you that much for other bases. I think there is a definition of digits somewhere? But mostly you can just do strong recursion on nat using that n / b < n.

#### Johan Commelin (Jun 03 2020 at 07:50):

Yup digits was added recently.

#### Scott Morrison (Jun 03 2020 at 08:33):

Actually, I think digits is still languishing in a PR I apparently abandoned: #2686

#### Johan Commelin (Jun 03 2020 at 08:42):

@Scott Morrison Are you planning on unabandoning it in the near future?

#### Scott Morrison (Jun 03 2020 at 08:43):

I have to admit it doesn't feel very high priority. But I think the suggestions were all easy to implement so the guilt will get to me at some point.

#### Johan Commelin (Jun 03 2020 at 08:44):

Otherwise, just label it with please-adopt. (You can adopt it yourself, when the guilt catches up.)

#### Reid Barton (Jun 03 2020 at 11:48):

Do we already have a version of https://en.wikipedia.org/wiki/Lucas%27s_theorem? That would make this PR more compelling (not that it should be included in this PR, but as possible future work).

#### Johan Commelin (Jun 03 2020 at 12:05):

I don't think we have that

#### Kevin Buzzard (Jun 03 2020 at 16:17):

I had something about digits too which i don't think I ever finished. Maybe @Calle Sönne was also involved?

#### Kevin Buzzard (Jun 03 2020 at 16:18):

https://en.wikipedia.org/wiki/Kummer%27s_theorem is what you want for recreational purposes