automation

Stream: general

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

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]

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]

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

[Scott Morrison]

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

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

(Such a tactic would remove the need for both the semiapplicable and simp hints above.)

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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