Zulip Chat Archive

Stream: triage

Topic: issue #2725: `push_hom` and `pull_hom` tactics


view this post on Zulip Random Issue Bot (Feb 14 2021 at 14:19):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: feature-request, help wanted, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Scott Morrison (Feb 14 2021 at 22:47):

I haven't thought about this in a while. But I'd certainly like to have something like this.

view this post on Zulip Scott Morrison (Feb 14 2021 at 22:48):

Indeed, in category theory proofs I can think of lots of related tools: push/pull for _functor, _eq_to_hom, ... I think all of them would just be named simp sets, and possibly rather light wrappers around them.

view this post on Zulip Eric Wieser (Feb 15 2021 at 05:30):

Is there a mechanism to say "use this simp set with every lemma reversed"?

view this post on Zulip Johan Commelin (Feb 15 2021 at 06:09):

On the other hand, since mathlib moved to bundled functions, I've had a lot less need for this type of tactics, because simp is now just a lot better at this.

view this post on Zulip Yury G. Kudryashov (Feb 15 2021 at 18:58):

simp is good as push_hom but sometimes (not often) I want pull_hom.

view this post on Zulip Random Issue Bot (Mar 17 2021 at 14:26):

Today I chose issue 2725 for discussion!

push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: feature-request, help wanted, meta

Is this issue still relevant? Any recent updates? Anyone making progress?


Last updated: May 09 2021 at 16:20 UTC