tidy is wicked strong

Stream: general

[Johan Commelin]

Kudos to Scott!

instance LeftMod__has_ZeroObject : @universal.has_ZeroObject (R-Mod) LeftMod_.foo :=
{ zero_object :=
{ zero_object := zero_module R,
  is_initial  := ⟨λ M : R-Mod, ⟨λ _, 0, is_linear_map.map_zero⟩,
  begin
    intros M f g,
    tidy,
    rw [← zero_is_star, is_linear_map.zero f_property, is_linear_map.zero g_property]
  end ⟩,
  is_terminal := by tidy
} }

[Johan Commelin]

I just told Lean the definition of the zero-module. And it figured out on its own that it is the terminal object in the category of left modules!
Mind you: I wrote only 1 rfl-lemma to help it:

lemma zero_is_star : (0 : (zero_module R)) = star := rfl

[Johan Commelin]

It needs a bit of hand-holding for the initial object, but I guess this is only because is_linear_map is not a class.

[Johan Commelin]

Long live @Scott Morrison! Blacksmith of hammer tactics!

[Johan Commelin]

Ooh, and obviously also does the job.

[Kevin Buzzard]

It's slowly dawning on me that my initial impression ("tidy is something Scott wrote to help with his category theory stuff, and it does category theory stuff") is completely wrong, and that tidy and obviously are really all-purpose tools which will help us all. But they are not even part of a PR, right? Is there some kind of plan to get them PR'ed somehow, and what are the obstructions to getting them into mathlib?

[Scott Morrison]

Hi Kevin, tidy doesn't do all that much, but I agree it's helpful. Really we need to carefully read <https://arxiv.org/abs/1309.4501> and translate it all into Lean, and then we'll really have the start of a hammer that mathematicians appreciate.

[Scott Morrison]

tidy is relatively easy to PR to mathlib, and hopefully I will have time soon to start doing this

[Scott Morrison]

many of the gross aspects of it have become cleaner in the last month

[Scott Morrison]

obviously is just tidy equipped with an extra tactic, called rewrite_search, which uses edit-distance based heuristics to search for chains of rewrites to prove equational results.

[Scott Morrison]

it is harder to PR, both because the implementation is really awful, and a student is actively working on cleverer (i.e. using machine learning in the heuristics) versions, so it's a moving target

[Scott Morrison]

(actually, secretly I'm hoping that he will rewrite rewrite_search from scratch for me, when he realises how awful it is)

[Minchao Wu]

@Scott Morrison who is the student? I'm also interested in applying machine learning to heuristics

[Kenny Lau]

@Kevin Buzzard did one of your students mention machine learning?

[Johan Commelin]

It seems that Mohan Ganesalingam completely left the field.

[Scott Morrison]

@Minchao Wu , it's Keeley Hoek, who is sometimes around here. (Also, as we're all in the same building, we should really meet up --- my apologies that I screwed up our last attempt to do so.)

[Scott Morrison]

@Kevin Buzzard, have you ever read that Ganesalingam-Gowers paper? If not, you really should. :-)

[Minchao Wu]

No worries :) Is the student also from the math department?

[Johan Commelin]

It's really a pity that the "future work" never materialised. I think Gowers also changed subject...

[Scott Morrison]

Well... Gowers was only ever a visitor... :-)

[Minchao Wu]

If he's coming next week we can just schedule a group meeting maybe

[Scott Morrison]

It is such a pity that they did their work in their own private interactive theorem prover, so it's not usable by the rest of us.

[Scott Morrison]

(Typical mathematicians! :-)

[Rob Lewis]

@Scott Morrison Are you/your student familiar with the work on TacticToe? http://cl-informatik.uibk.ac.at/users/cek/docs/17/tgckju-lpar17.pdf They've been relatively successful with ML-guided tactic proofs in HOL4. One of the more impressive results at AITP this year, in my opinion.

[Scott Morrison]

Thanks @Rob Lewis for the reference. This is very different than what we're trying.