Zulip Chat Archive

Stream: general

Topic: tidy is wicked strong


view this post on Zulip 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
} }

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 03 2018 at 07:09):

Long live @Scott Morrison! Blacksmith of hammer tactics!

view this post on Zulip Johan Commelin (Aug 03 2018 at 07:52):

Ooh, and obviously also does the job.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Aug 03 2018 at 08:18):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Minchao Wu (Aug 03 2018 at 08:24):

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

view this post on Zulip Kenny Lau (Aug 03 2018 at 08:24):

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

view this post on Zulip Johan Commelin (Aug 03 2018 at 08:27):

It seems that Mohan Ganesalingam completely left the field.

view this post on Zulip 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.)

view this post on Zulip Scott Morrison (Aug 03 2018 at 08:29):

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

view this post on Zulip Minchao Wu (Aug 03 2018 at 08:30):

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

view this post on Zulip 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...

view this post on Zulip Scott Morrison (Aug 03 2018 at 08:33):

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

view this post on Zulip Minchao Wu (Aug 03 2018 at 08:33):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 03 2018 at 08:34):

(Typical mathematicians! :-)

view this post on Zulip 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.

view this post on Zulip 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