Zulip Chat Archive

Stream: new members

Topic: Multiplying by 2


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 14:27):

I guess you could prove it by induction

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 23 2020 at 14:37):

anyway, there is a theorem two_mul

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 23 2020 at 14:41):

there is the lean docs

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Apr 23 2020 at 14:41):

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

view this post on Zulip Emiel Lanckriet (Apr 23 2020 at 14:43):

Thanks, for now I am just using CoCalc.

view this post on Zulip Mario Carneiro (Apr 23 2020 at 14:43):

there is also grep on the sources

view this post on Zulip Mario Carneiro (Apr 23 2020 at 14:43):

or your favorite not-grep

view this post on Zulip Mario Carneiro (Apr 23 2020 at 14:44):

and library_search

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emiel Lanckriet (Apr 23 2020 at 16:00):

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


Last updated: May 10 2021 at 00:31 UTC