# Zulip Chat Archive

## Stream: general

### Topic: automation

#### Scott Morrison (Jun 05 2018 at 00:26):

I was just having a look at @Chris Hughes's nice PR for quotient groups.

#### Scott Morrison (Jun 05 2018 at 00:26):

I golfed it a bit, using my "obviously" and "tidy" tactics, and would like to see how people feel about the result.

#### Scott Morrison (Jun 05 2018 at 00:27):

Chris's proof is at <https://github.com/leanprover/mathlib/pull/154/commits/b7edcbdd1f783da5f17dcd840057352157afdac0>.

#### Scott Morrison (Jun 05 2018 at 00:28):

I factored this into essentially three bits: 2 lemmas about elements in normal subgroups, a few "hints" for my automation, and then the following proof:

#### Scott Morrison (Jun 05 2018 at 00:28):

instance quotient_group' [group α] (s : set α) [normal_subgroup s] : group (left_cosets s) := by refine { one := ⟦1⟧, mul := λ a b, quotient.lift_on₂ a b (λ a b, ⟦a * b⟧) (by obviously), inv := λ a', quotient.lift_on a' (λ a, ⟦a⁻¹⟧) (by obviously), .. }; obviously

#### Scott Morrison (Jun 05 2018 at 00:28):

which is about as easy on the eye as I think one can hope for.

#### Scott Morrison (Jun 05 2018 at 00:28):

The lemmas are:

lemma quotient_group_aux [group α] (s : set α) [normal_subgroup s] (a b : α) (h : a⁻¹ * b ∈ s) : a * b⁻¹ ∈ s := begin rw [← inv_inv a, ← mul_inv_rev], exact is_subgroup.inv_mem (is_subgroup.mem_norm_comm h), end lemma quotient_group_aux' [group α] (s : set α) [normal_subgroup s] (a b c d : α) (h₁ : a * b ∈ s) (h₂ : c * d ∈ s) : c * (a * (b * d)) ∈ s := begin apply is_subgroup.mem_norm_comm, rw [← mul_assoc, mul_assoc], apply (is_subgroup.mul_mem_cancel_right s h₁).2, exact is_subgroup.mem_norm_comm h₂ end

#### Scott Morrison (Jun 05 2018 at 00:30):

which are dull variants on what Chris had done, just extracted out. I made no attempt to automate those, but I think it's not too much a stretch to hope that one could explain to a computer how to do these.

#### Scott Morrison (Jun 05 2018 at 00:30):

The ugly part of my "obviously-golfed" version is the "hints": before the nice instance proof I need to say:

-- Some 'hint' attributes for obviously. local attribute [reducible] setoid_has_equiv left_rel local attribute [applicable] is_submonoid.one_mem -- `applicable` means the lemma should be applied whenever relevant local attribute [semiapplicable] quotient_group_aux quotient_group_aux' -- `semiapplicable` means the lemma should be applied if all its hypotheses can be satisfied from the context local attribute [simp] mul_assoc

#### Scott Morrison (Jun 05 2018 at 00:31):

The whole thing is available at <https://github.com/semorrison/lean-tidy/blob/master/examples/quotient_group.lean>.

#### Scott Morrison (Jun 05 2018 at 00:34):

(Regarding the hints: `attribute [applicable] is_submonoid.one_mem`

would become a global attribute in my dream world --- whenever the goal is to prove `1 ∈ s`

, for `s`

a monoid, you should let the computer do that for you. :-) With another simple lemma about normal subgroups, one could do without the `attribute [simp] mul_assoc`

hint, which is pretty fragile.)

#### Scott Morrison (Jun 05 2018 at 01:34):

(On the subject of the two lemmas, once we have PIDs and Smith normal form, we can write a general purpose tactic which shows whether a given word lies in the normal subgroup generated by some collection of words, and hence prove goals of the form `w \mem s`

, given one or more hypotheses of the same form.)

#### Scott Morrison (Jun 05 2018 at 01:35):

(Such a tactic would remove the need for both the `semiapplicable`

and `simp`

hints above.)

#### Johan Commelin (Jun 05 2018 at 05:39):

Wow! That's some nice golfing. And golfing where you increase readability, instead of obfuscating!

#### Johan Commelin (Jun 05 2018 at 05:40):

@Kevin Buzzard Don't you think these tactics would help a lot with the perfectoid project?

#### Johan Commelin (Jun 05 2018 at 05:40):

If we want to produce code that is somewhat legible to mathematicians.

#### Kevin Buzzard (Jun 05 2018 at 06:53):

I am pretty sure that these tactics will make life much easier for mathematicians. Goodness knows if I will be able to use them. I have no idea of the problems I'll face with perfectoid spaces.

#### Patrick Massot (Jun 05 2018 at 07:27):

Automation is clearly the key. Proof assistants can become useful tools for mathematicians only if every stupid proof eventually gets automatic

Last updated: May 06 2021 at 22:13 UTC