Odd/Even Kata

Stream: new members

[Wrenna Robson]

Hi. I'm trying to do the following training kata.

https://www.codewars.com/kata/5e998b42dcf07b0001581def/train/lean

I've managed to do the basic and addition sections fine, but the multiplication section feels hard given that I don't actually have (I think) any of the regular natural number theorems: in particular I don't think I have the distributive law. So I can't see how to proceed. Can anyone assist?

[Shing Tak Lam]

This Kata was originally written a while ago, back when the nat stuff was still in Core Lean. Now it is in mathlib but the imports of the kata have not been changed to keep up.

If you import data.nat.basic at the top of the file it should work.

(I wrote the Kata but I haven't been active on Codewars in a while, but this does bring up a good point about katas which aren't 'broken', since the Preloaded/Solution files still check, but the expected lemmas are not there anymore).

[Wrenna Robson]

Thank you! I did wonder...

Incidentally my approach generally has been to do an induction tactic on the evenness hypothesis, like so:

lemma odd_add_one {n : ℕ} (hn : odd n) : even (n + 1) :=
begin
    induction hn with _ _ plus_one_even,
    exact even_ss even_zero,
    exact even_ss plus_one_even,
end

This has worked pretty well, but I wasn't sure if this was the intended approach!

[Shing Tak Lam]

Yeah that's pretty much the expected approach.

[Wrenna Robson]

Hmm - it seems inserting import data.nat.basic at the top has broken all my existing proofs...

[Wrenna Robson]

Possibly because it then does something different when I do the induction?

[Shing Tak Lam]

That's very strange, and I can't seem to reproduce that error. I don't think induction should do anything different.

[Wrenna Robson]

Here is I think a MWE:

import data.nat.basic

inductive even : ℕ → Prop
| even_zero : even 0
| even_ss : ∀ {n}, even n → even (n + 2)

inductive odd : ℕ → Prop
| odd_one : odd 1
| odd_ss : ∀ {n}, odd n → odd (n + 2)

open odd even

-- Getting Started

lemma even_add_one {n : ℕ} (hn : even n) : odd (n + 1) :=
begin
    induction hn with _ _ plus_one_odd,
    exact odd_one,
    exact odd_ss plus_one_odd,
end

[Wrenna Robson]

With the first line, the proof doesn't work: my tactic state is as follows after the induction line:

nhn_w: ℕ
hn_h: n = 2 * hn_w
⊢ odd (n + 1)

[Wrenna Robson]

Without it, it is like this:

case even.even_zero
n: ℕ
⊢ odd (0 + 1)
case even.even_ss
nhn_n: ℕ
hn_ᾰ: even hn_n
plus_one_odd: odd (hn_n + 1)
⊢ odd (hn_n + 2 + 1)

[Wrenna Robson]

I think it might be using some kind of odd and even definition from import data.nat.basic?

[Wrenna Robson]

Rather than the inductive definition in the file.

[Shing Tak Lam]

Yeah, there is a definition for odd and even now in the root namespace. I tested on Codewars, which is still on 3.20, which was why I didn't get any errors on there. I guess this is one of the cases where the Lean version mismatch between your local install of Lean and Codewars is kind of an issue... Not sure when/if Lean on Codewars will be updated anytime soon, since I haven't really kept up with what is happening on there,

[Wrenna Robson]

Yeah, I'm working in VSCode (because I don't think you get the same functionality on Codewars!) Hmm: I suppose a way of solving this would be just to rename odd and even to my_odd and my_even?

[Shing Tak Lam]

Yeah, that will become an issue the next time Codewars updates their version of Lean. In the meantime, I guess you can put the contents of that file in a namespace (but remember to not have the namespace when submitting) and it'd work.

import data.nat.basic

namespace hidden

inductive even : ℕ → Prop
| even_zero : even 0
| even_ss : ∀ {n}, even n → even (n + 2)

inductive odd : ℕ → Prop
| odd_one : odd 1
| odd_ss : ∀ {n}, odd n → odd (n + 2)

open odd even

-- Getting Started

lemma even_add_one {n : ℕ} (hn : even n) : odd (n + 1) :=
begin
    induction hn with _ _ plus_one_odd,
    exact odd_one,
    exact odd_ss plus_one_odd,
end

end hidden

[Wrenna Robson]

Grand, thanks (I don't really understand how namespaces work...)

[Wrenna Robson]

Done! Thanks for help.