recursive function from \N

Stream: new members

[Li Xuanji]

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]

@Li Xuanji What is pos_num?

[Mario Carneiro]

binary positive natural numbers

[Johan Commelin]

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

[Johan Commelin]

Aah... :bulb:

[Mario Carneiro]

it's in mathlib

[Johan Commelin]

@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]

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

[Johan Commelin]

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.

[Li Xuanji]

thanks!

[Li Xuanji]

wait where's binary_rec_on defined?

[Li Xuanji]

ah I guess it got renamed to binary_rec

[Mario Carneiro]

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]

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

[Li Xuanji]

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

[Mario Carneiro]

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

[Mario Carneiro]

induction on pos_num should work fine

[Li Xuanji]

yeap induction worked

[Li Xuanji]

let me look up what failed

[Li Xuanji]

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]

with your definition of J_joseph₁ it works much better

[Kevin Buzzard]

@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]

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

[Li Xuanji]

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]

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]

Yup digits was added recently.

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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]

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

[Reid Barton]

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]

I don't think we have that

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(olympiads etc)