## Stream: general

### Topic: tidy is wicked strong

#### Johan Commelin (Aug 03 2018 at 07:07):

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 (Aug 03 2018 at 07:07):

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 (Aug 03 2018 at 07:08):

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 (Aug 03 2018 at 07:09):

Long live @Scott Morrison! Blacksmith of hammer tactics!

#### Johan Commelin (Aug 03 2018 at 07:52):

Ooh, and obviously also does the job.

#### Kevin Buzzard (Aug 03 2018 at 08:13):

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 (Aug 03 2018 at 08:17):

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 (Aug 03 2018 at 08:18):

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

#### Scott Morrison (Aug 03 2018 at 08:18):

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

#### Scott Morrison (Aug 03 2018 at 08:18):

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 (Aug 03 2018 at 08:19):

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 (Aug 03 2018 at 08:20):

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

#### Minchao Wu (Aug 03 2018 at 08:24):

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

#### Kenny Lau (Aug 03 2018 at 08:24):

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

#### Johan Commelin (Aug 03 2018 at 08:27):

It seems that Mohan Ganesalingam completely left the field.

#### Scott Morrison (Aug 03 2018 at 08:28):

@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 (Aug 03 2018 at 08:29):

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

#### Minchao Wu (Aug 03 2018 at 08:30):

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

#### Johan Commelin (Aug 03 2018 at 08:32):

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

#### Scott Morrison (Aug 03 2018 at 08:33):

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

#### Minchao Wu (Aug 03 2018 at 08:33):

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

#### Scott Morrison (Aug 03 2018 at 08:34):

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 (Aug 03 2018 at 08:34):

(Typical mathematicians! :-)

#### Rob Lewis (Aug 03 2018 at 11:14):

@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 (Aug 03 2018 at 11:16):

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

Last updated: May 18 2021 at 17:44 UTC