reformulate

Stream: metaprogramming / tactics

[Patrick Massot]

@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.

[Jalex Stark]

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

[Reid Barton]

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

[Patrick Massot]

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

[Patrick Massot]

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".

[Rob Lewis]

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

[Rob Lewis]

And also working on hypotheses.

[Patrick Massot]

Yes, but it would return only relevant stuff.

[Jalex Stark]

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

[Rob Lewis]

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.

[Patrick Massot]

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.

[Rob Lewis]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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.

[Yury G. Kudryashov]

I meant that the tactic should show tfae.get too