Zulip Chat Archive

Stream: new members

Topic: Odd/Even Kata


view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:08):

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?

view this post on Zulip Shing Tak Lam (Nov 13 2020 at 11:15):

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).

view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:17):

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!

view this post on Zulip Shing Tak Lam (Nov 13 2020 at 11:18):

Yeah that's pretty much the expected approach.

view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:20):

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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:20):

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

view this post on Zulip Shing Tak Lam (Nov 13 2020 at 11:23):

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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:24):

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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:25):

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)

view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:25):

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)

view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:26):

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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:26):

Rather than the inductive definition in the file.

view this post on Zulip Shing Tak Lam (Nov 13 2020 at 11:29):

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,

view this post on Zulip Wrenna Robson (Nov 13 2020 at 11:30):

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?

view this post on Zulip Shing Tak Lam (Nov 13 2020 at 11:34):

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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 12:16):

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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 12:32):

Done! Thanks for help.


Last updated: May 08 2021 at 04:14 UTC