Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: filter_upwards
Heather Macbeth (Jan 23 2022 at 00:59):
The tactic docs#tactic.interactive.filter_upwards converts the goal to the form ∀ x, x ∈ t1 → ⋯ → x ∈ tn → x ∈ s. So it is followed 99% of the time (eg, every time at a random sample I took in mathlib) by intros.
Perhaps we could have syntax filter_upwards [...] with x h1 h2 which performs the intros step at the same time?
Mario Carneiro (Jan 23 2022 at 03:09):
sounds good to me. The filter_upwards [...] e syntax is also odd and could be replaced by filter_upwards [...] using e
Heather Macbeth (Jan 23 2022 at 03:15):
I've opened issue #11616 for this and will try it in a few weeks if someone else doesn't get there first!
Arthur Paulino (Jan 23 2022 at 13:01):
May I give it a try? This is what I'm trying to learn at the moment :pray:
Arthur Paulino (Jan 23 2022 at 13:34):
When combining both improvements, should it be said filter_upwards [...] with ... using ... or filter_upwards [...] using ... with ...?
Arthur Paulino (Jan 23 2022 at 14:07):
Ah, using ... tries to close the goal with exact ... so I'm guessing the former is more appropriate
Arthur Paulino (Jan 23 2022 at 14:08):
(deleted)
Arthur Paulino (Jan 23 2022 at 17:10):
I'm noticing that there are more occurrences of assume ... after filter_upwards [...] than intros ...
Arthur Paulino (Jan 23 2022 at 17:20):
Maybe not more, but I can't tell which one occurs more often
Yury G. Kudryashov (Jan 23 2022 at 17:24):
Please don't forget to update the docstring.
Heather Macbeth (Jan 23 2022 at 17:27):
assume is the same as intros though :)
Damiano Testa (Jan 23 2022 at 17:30):
You may also want to check for λ s after filter_upwards, since an intros can be replaced by refine λ ..., .... :shrug:
Mario Carneiro (Jan 23 2022 at 17:53):
@maintainers I've tried to keep track of these PRs but it's hard to know when they land. Can we have a rule that anything that adds a new interactive tactic or changes tactic syntax be tagged as modifies-tactic-syntax? That will make it easier to review these for mathport/mathlib4 updates
Johan Commelin (Jan 23 2022 at 17:55):
They should at least be tagged meta. I don't think there are that many PRs tagged with meta. Does that already help?
Mario Carneiro (Jan 23 2022 at 18:02):
It's only a small fraction of meta issues. I'm going through now and marking them
Arthur Paulino (Jan 23 2022 at 21:39):
The bulk of the PR is finished: #11624
I'm just fixing the errors that the CI tests find, but you can already check the changes.
Arthur Paulino (Jan 25 2022 at 10:52):
And it's merged :)
Last updated: Dec 20 2023 at 11:08 UTC