Group Is Not Union Of Two Proper Subgroups

Stream: Codewars

[Kenny Lau]

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.

[Kenny Lau]

what do you guys think about this?

[Jalex Stark]

my preferred solution is to put

noncomputable theory
open_locale classical

as part of the "initial solution"

[Jalex Stark]

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

[Jalex Stark]

which, no

[Kenny Lau]

what does @Kevin Buzzard think about this?

[Jalex Stark]

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]

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]

that can be your next kata!

[Jalex Stark]

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

[Kevin Buzzard]

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]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

@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]

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]

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]

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

[Jalex Stark]

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

[Jalex Stark]

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]

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]

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 *,
by_contradiction g,
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]

what's the statement?

[Sam Lichtenstein]

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]

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

[Sam Lichtenstein]

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

[Mario Carneiro]

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

[Bhavik Mehta]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

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

[Donald Sebastian Leung]

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.

[Way Yan]

Sorry for reviving this thread, but I'm completely stuck at a really basic point: how do I unfold the hypotheses hS : S < ⊤ and hK : K < ⊤ into a more usable form (like a statement with quantifiers and ∈)? I'm guessing this is a bit of stupid question, but I'm still very unfamiliar with Lean :sweat_smile:

[Mario Carneiro]

I'm not sure if it definitionally works out to something useful, but S <= T should definitionally be the same as subset so you can use S < T -> \not (\forall x \in T, x \in S) and then work with that

[Mario Carneiro]

example {G : Type} [group G] (S : subgroup G) (HST : S < ⊤) : ∃ x, x ∉ S :=
by simpa [set.subset_def] using HST.2

[Way Yan]

Thanks!