Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: reformulate


view this post on Zulip Patrick Massot (Aug 24 2020 at 08:46):

@Scott Morrison so you think you could offer us a variation on library_search that would search only for lemmas asserting the goal or the targeted assumption is equivalent to something else? For instance, if my goal is uniform continuity of a function between metric spaces, then I want to type reformulate and see a list of suggestions including docs#metric.uniform_continuous_iff (ideally suggestions would be clickable and include the reformulated goal), and the same with reformulate at h.

view this post on Zulip Jalex Stark (Aug 24 2020 at 12:22):

I heard someone talk about a work-in-progress rw_hint that seemed like the same idea

view this post on Zulip Reid Barton (Aug 24 2020 at 12:28):

This also sounds like the core part of rewrite_search, but with a human doing the search part

view this post on Zulip Patrick Massot (Aug 24 2020 at 12:39):

No, I'm asking for a much stupider thing, no recursion into subterm involved.

view this post on Zulip Patrick Massot (Aug 24 2020 at 12:40):

In principle I'm mostly targeting the case of "here are ten definitions of the same thing, I don't want to know which one is the definition".

view this post on Zulip Rob Lewis (Aug 24 2020 at 12:41):

This sounds like suggest but filtered to only iff.mp/mpr applications, right?

view this post on Zulip Rob Lewis (Aug 24 2020 at 12:41):

And also working on hypotheses.

view this post on Zulip Patrick Massot (Aug 24 2020 at 12:42):

Yes, but it would return only relevant stuff.

view this post on Zulip Jalex Stark (Aug 24 2020 at 13:45):

I guess "return only relevant stuff" is something one can make incremental progress on by improving the heuristic for ranking by relevance

view this post on Zulip Rob Lewis (Aug 24 2020 at 13:47):

Ranking by the number of new goals generated seems like a good metric. An application of iff.mp that results in no extra goals seems like a reformulation, by definition.

view this post on Zulip Patrick Massot (Aug 25 2020 at 12:15):

There is no ranking involved in my proposal. If the tactic only matches exactly the goal (or assumption), relevance is automatic (modulo side condition), that's the point.

view this post on Zulip Rob Lewis (Aug 25 2020 at 12:32):

Then I don't understand your comment here:
Patrick Massot said:

Yes, but it would return only relevant stuff.

It sounds like you're exactly describing suggest filtered to only iff.mp/mpr applications, also working on hypotheses.

view this post on Zulip Patrick Massot (Aug 25 2020 at 12:38):

Yes, that's why I hope it would be a trivial exercise for Scott (or anyone understand how suggest works).

view this post on Zulip Patrick Massot (Aug 25 2020 at 12:39):

Well, there is extra credit if the tactic displays what the new goal/assumption would be, and I don't think suggest does that.

view this post on Zulip Yury G. Kudryashov (Sep 16 2020 at 16:36):

If we have 10 equivalent definitions, then probably we have a tfae, not many iffs.

view this post on Zulip Patrick Massot (Sep 16 2020 at 17:02):

The tactic would be useful even if we have a couple of iff. And, more importantly, they can have different assumptions. For instance uniform continuity can be reformulated differently for general uniform spaces, metric spaces, normed spaces.

view this post on Zulip Yury G. Kudryashov (Sep 16 2020 at 17:06):

I meant that the tactic should show tfae.get too


Last updated: May 09 2021 at 23:10 UTC