Zulip Chat Archive

Stream: new members

Topic: Multiplying by 2


Emiel Lanckriet (Apr 23 2020 at 14:25):

I'm making a Odd + Even = Odd? Even * Anything = Even? Prove it!-kata on Codewars, but I'm stuck even_mul_even, I know that n is even and I know that sums of even numbers are even, now I want to show that that n * 2 is even, but I can't find a way to convert n * 2 to n + n. Any advice?

Kevin Buzzard (Apr 23 2020 at 14:27):

I guess you could prove it by induction

Kevin Buzzard (Apr 23 2020 at 14:27):

When I did that kata I proved a couple of things which weren't asked for, to make my life easier.

Emiel Lanckriet (Apr 23 2020 at 14:29):

Ok, thanks I'll try to prove n*2=n+n by induction in a separate function.

Kevin Buzzard (Apr 23 2020 at 14:31):

I guess we're hoping to keep codewars spoiler questions off this site in general, although most Lean questions are welcomed :-)

Mario Carneiro (Apr 23 2020 at 14:33):

I'm not sure I like this, we've never had to censor solutions before, despite several lean classes being taught

Mario Carneiro (Apr 23 2020 at 14:35):

It means that the more people make katas the less we can talk about, and the censorship has no end date

Mario Carneiro (Apr 23 2020 at 14:37):

anyway, there is a theorem two_mul

Emiel Lanckriet (Apr 23 2020 at 14:40):

Is there a place where I can easily look up these theorems, because for the moment I look at the sidelines of the natural numbers game, but some of it doesn't translate to Lean in general.

Mario Carneiro (Apr 23 2020 at 14:41):

there is the lean docs

Shing Tak Lam (Apr 23 2020 at 14:41):

Are you using VSCode? if so, press Ctrl-P and then # if you know what the name should be (approximately).

Mario Carneiro (Apr 23 2020 at 14:41):

https://leanprover-community.github.io/mathlib_docs/

Emiel Lanckriet (Apr 23 2020 at 14:43):

Thanks, for now I am just using CoCalc.

Mario Carneiro (Apr 23 2020 at 14:43):

there is also grep on the sources

Mario Carneiro (Apr 23 2020 at 14:43):

or your favorite not-grep

Mario Carneiro (Apr 23 2020 at 14:44):

and library_search

Donald Sebastian Leung (Apr 23 2020 at 15:07):

IMO general hints and tips for solving Codewars kata is okay, but don't e.g. post your Codewars solutions publicly on GitHub (because then others could just copy and paste full solutions to get free points)

Emiel Lanckriet (Apr 23 2020 at 15:40):

I have been looking for the inverse of succ_inj in the docs, but I can't find it does someone know where to find this? In the natural number game it is called succ_eq_succ_of_eq, but in the mathlib_docs I can't find anything similar.

Mario Carneiro (Apr 23 2020 at 15:58):

congr_arg is a theorem that proves x = y -> f x = f y once and for all. The tactic is congr

Emiel Lanckriet (Apr 23 2020 at 16:00):

Wow, thanks, that's much more powerfull than what I needed.


Last updated: Dec 20 2023 at 11:08 UTC