## Stream: Codewars

### Topic: Group Is Not Union Of Two Proper Subgroups

#### Kenny Lau (May 13 2020 at 20:28):

https://www.codewars.com/kata/5ea8056e449f540001a2dab2/discuss/lean

Unless the intent of this kata was explicitly to make the trainee (me in this case) discover things like decidable/classical/etc on their own, I would suggest adding a hint in this direction to the description. This could be as simple as pointing out the existence of the classical tactic.

#### Jalex Stark (May 13 2020 at 20:30):

my preferred solution is to put

noncomputable theory
open_locale classical


as part of the "initial solution"

#### Jalex Stark (May 13 2020 at 20:31):

I guess sflicht thinks that the Lean codewars exercises should teach you everything about doing math in Lean

which, no

#### Jalex Stark (May 13 2020 at 20:37):

I left this as a comment:

A good patch is to have

noncomputable theory
open_locale classical


in the header of any Lean kata which is meant to be about "everyday mathematics".

I don't think "learn Lean entirely through exercises on Codewars" is a particularly good life strategy, anymore than it would be for learning other languages. Come ask questions here
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members

or use this website to find reference material
https://leanprover-community.github.io/

#### Kevin Buzzard (May 13 2020 at 20:41):

I've not been doing codewars because I've had to cut down on my "recreational Lean" since hundreds of undergrad scripts landed on my desk. I'll be back by the end of May. I think the fact that a group isn't a union of two proper subgroups is a cool lemma. One could even make it harder by proving that 2 is tight :-)

#### Kenny Lau (May 13 2020 at 20:42):

that can be your next kata!

#### Jalex Stark (May 13 2020 at 20:42):

(I think kenny's question was about the linked comment from the kata discussion thread?)

#### Kevin Buzzard (May 13 2020 at 20:45):

Oh! Are you asking whether I think learning Lean entirely through exercises on codewars is a good idea? I guess not, some kata are far too hard for a beginner, some are simple, one needs access to material which is "just right" to learn stuff well. I guess that if we make it 100 kata then there will be a whole lot of choice though -- there already is a nice variety of kata in fact.

#### Jalex Stark (May 13 2020 at 20:47):

I guess if one wants to make this kind of learning easier, one should put together more "collections"

#### Jalex Stark (May 13 2020 at 20:47):

e.g. donald has a "real analysis" and "incidence geometry" collections

#### Jalex Stark (May 13 2020 at 20:48):

these happen to have problems entirely written by him, but I think that is not a necessary feature of collections

#### Jalex Stark (May 13 2020 at 20:48):

@Rocky Kamen-Rubio was trying to make some sort of beginner's collection based on his experience being very new and solving kata?

#### Kevin Buzzard (May 13 2020 at 20:49):

When I have time I might make a Diophantine equation collection; I asked two hard questions so far but I know 100 easier ones.

#### Sam Lichtenstein (May 13 2020 at 23:48):

Jalex Stark said:

I guess sflicht thinks that the Lean codewars exercises should teach you everything about doing math in Lean

FTR, I am sflicht on codewars. I certainly did not mean to imply what you say. Only that if the purpose of the kata is to be pedagogical, I didn't think this one was optimized (unless the author was intending to teach students how to discover "open_locale classical" for themselves, in which case the kata was a success, at least in my case!)

#### Jalex Stark (May 13 2020 at 23:51):

hi sam! my point is just that "use classical reasoning" should be useful in like, ~all kata

#### Jalex Stark (May 13 2020 at 23:52):

so it would be weird to put the burden of explicitly teaching that here

#### Jalex Stark (May 13 2020 at 23:53):

anyway, it sounds like we agree that "add stuff to the header to indicate that classical reasoning is encouraged" is a good course of action

#### Sam Lichtenstein (May 14 2020 at 00:04):

while it's obvious that classical reasoning is useful for any normal math, I had not encountered references to the fact that one sometimes needs to explicitly engage this mode in any of the other beginner resources (#TPIL, #NNG, etc). of course it's possible I just missed it.

#### Sam Lichtenstein (May 14 2020 at 00:15):

while I have your attention, another beginner point raised by the linked kata was that I stumbled towards a solution that opened with

by_cases (∀ x, x ∈ S),
simp *,
simp *,
have sproper := not_forall.mp h,
have tproper := not_forall.mp g,


I was vaguely aware from reading other resources that "using simp before the end" is bad, so I assumed my solution was suboptimal. From perusing the other solutions, I learned that it could be replaced with what I guess is a more idiomatically correct opening sequence:

by_contra h,
push_neg at h,
cases h with sproper tproper,


At the end of the day, I was left wondering if there are any tutorials oriented towards teaching this type of idiom -- basically how to use tactics with flair, the way Serre would do. (Even if in other contexts -- such as mathlib? -- it might be considered better style to write proofs in the style of Soviet mathematician about to run out of typewriter ink.) I suppose the book-in-progress Mathematics In Lean might fill the gap eventually. But if there is some obvious resource that I should be aware of, I'd certainly love to know about it!

#### Mario Carneiro (May 14 2020 at 00:15):

what's the statement?

#### Sam Lichtenstein (May 14 2020 at 00:17):

it's theorem of_forall_mem_or_mem {G : Type u} [group G] (S T : set G) [is_subgroup S] [is_subgroup T] (HST : ∀ x, x ∈ S ∨ x ∈ T) : (∀ x, x ∈ S) ∨ (∀ x, x ∈ T) := sorry from https://www.codewars.com/kata/5c85201e20f73f08df4216b1/train/lean

#### Bhavik Mehta (May 14 2020 at 00:18):

I love the phrase "proofs in the style of Soviet mathematician about to run out of typewriter ink"

#### Sam Lichtenstein (May 14 2020 at 00:18):

I didn't intentionally drop the article, actually, but I wish it had been intentional

#### Mario Carneiro (May 14 2020 at 00:19):

This is a difficult question to answer, as there are many many ways to prove things, even discounting the obviously bad ones

#### Bhavik Mehta (May 14 2020 at 00:22):

I don't think there's many idioms of this form - for me there's a (small) list of tactics which I would use, and not the phrase "by_contra -- push_neg -- cases" or something (although in this particular case I think there should be something called by_contra! which does by_contra, push_neg)

#### Mario Carneiro (May 14 2020 at 00:23):

I try to put each "conceptual unit" on one line. Usually this entails applying a theorem and getting some new variables

#### Mario Carneiro (May 14 2020 at 00:26):

In this case I would have liked to say

theorem of_forall_mem_or_mem {G : Type} [group G] (S T : set G) [is_subgroup S] [is_subgroup T]
(HST : ∀ x, x ∈ S ∨ x ∈ T) : (∀ x, x ∈ S) ∨ (∀ x, x ∈ T) :=
begin
refine or_iff_not_and_not.2 (λ ⟨h₁, h₂⟩, _),
end


but this doesn't quite work, both because or_iff_not_and_not requires decidability and because the pattern match turns the refine into an exact

#### Mario Carneiro (May 14 2020 at 00:26):

a reasonable alternative is

theorem of_forall_mem_or_mem {G : Type} [group G] (S T : set G) [is_subgroup S] [is_subgroup T]
(HST : ∀ x, x ∈ S ∨ x ∈ T) : (∀ x, x ∈ S) ∨ (∀ x, x ∈ T) :=
begin
classical,
apply or_iff_not_and_not.2, rintro ⟨h₁, h₂⟩,
end


#### Sam Lichtenstein (May 14 2020 at 00:28):

is it fair to say that "have" is considered inelegant? I find myself using it a lot to break the problem down into digestible bits, but I rarely see it in @Kenny Lau's kata solutions, for example. Or is this a bit like "point free" in Haskell (https://wiki.haskell.org/Pointfree) -- not that I really know anything about Haskell -- in that it can be simultaneously more elegant and more obscure...

#### Mario Carneiro (May 14 2020 at 00:29):

I would say that if you are going for compact proofs, have is useful only if you want to rewrite the result. Otherwise you can usually inline the have into the next line

#### Jalex Stark (May 14 2020 at 00:53):

whenever you have a nonterminal simp, use squeeze_simp, which will produce a list of lemmas so that simp only [list, of, lemmas], will do what you want and run fast

#### Jalex Stark (May 14 2020 at 00:54):

the problem with nonterminal simps (and terminal ones, even!) is that it has to do a search through the very long list of simp lemmas for the appropriate ones

#### Jalex Stark (May 14 2020 at 00:54):

the problem that gets worse with nonterminal simps is that if you add more simp lemmas, you might change the result of the simp

#### Jalex Stark (May 14 2020 at 00:55):

so "simp gets smarter" breaks your proof if you used simp the wrong way

#### Donald Sebastian Leung (May 14 2020 at 03:55):

Jalex Stark said:

these happen to have problems entirely written by him, but I think that is not a necessary feature of collections

Speaking of collections, I would recommend adding a link to the collection in the description for each kata so solvers stumbling on any kata in the collection would be able to follow the link and find related exercises; otherwise, it could get lost in the sea of collections pretty quickly.

Last updated: May 08 2021 at 23:10 UTC