Announcement: new `push` tactic

Stream: mathlib4

[Jovan Gerbscheid]

The push and pull tactics were recently merged into Mathlib. They are a generalization of push_neg, so now push_neg is a macro for push Not. The push tactic is extensible, so we need to tag a bunch of lemmas with @[push] in order to start using it. This includes tags to extend push_neg. I made #29000 to add a bunch of these tags, but it got a bit large, so I'm splitting it into several PRs to make it easier to review. Would someone like to review them?

[Jovan Gerbscheid]

Annotations for Real.log: #30039

[Jovan Gerbscheid]

Annotations for fun: #30038

[Jovan Gerbscheid]

Annotations for membership in Set, Finset and Multiset: #30042

[Jovan Gerbscheid]

Annotations for push_neg for Empty/Subsingleton/Finite/Countable: #30051

[Jovan Gerbscheid]

When working on these PRs, I would have liked the following features:

• If the goal is IsEmpty A or Subsingleton A, it would be nice to be able to use by_contra! with an rintro pattern.
• absurd should have an absurd! version that calls push_neg
• by_cases should have a by_cases! version that calls push_neg on the second sub-goal
• by_contra and by_contra! behave differently when no argument is given. One of them introduces a hypothesis this, and the other gives an inaccessible name. Should it always be this?
• When the goal is X ⊆ Y, I would like a version of intro that automatically calls push _ ∈ _ on the new goal, so that if the goal is for example {x | P x} ⊆ {x | Q x}, I want it to give P x → Q x. Maybe it should be called mem_intro or intro_mem?

Do you agree with these suggestions?

[Yaël Dillies]

Jovan Gerbscheid said:

now push_neg is not a macro for push Not

Typo?

[Patrick Massot]

Did you made sure to keep everything that teachers use? Originally push_neg was a pure teaching tactic.

[Patrick Massot]

And verbose Lean currently has the awful https://github.com/PatrickMassot/verbose-lean4/blob/bd3b236511d9a8929791f20f775e98a9ef81697c/Verbose/Tactics/Common.lean#L563-L625

[Jovan Gerbscheid]

@Patrick Massot Yes, the option push_neg.use_distrib is still supported. The only behaviour that has changed is that it looks through reducible constants better:

import Mathlib

axiom Bar : Prop
abbrev Foo := ¬ Bar

#push_neg ¬ Foo -- Bar

[Robert Maxton]

@Jovan Gerbscheid
I would suggest that by_cases! just calls push_neg on both goals; sometimes it is convenient for one reason or another to put the negated version first. It would also be nice to turn ¬ Set.Nonempty into = ∅; bonus points if it also supposes rcases patterns so you can immediately case on the equality, but that might be beyond the scope of push

[Robert Maxton]

otherwise, yes, those all look good to me

[Jovan Gerbscheid]

If you want to get the negated version first, for example by_cases! h : ¬ p, then in the first goal we get h : ¬ p, and in the second goal h : p. The tactic doesn't actually need to push_neg in the first goal, only in the second goal. Also, I think it might be more readable to write by_cases h : p; swap.

Before my work, push_neg did already turn ¬ Set.Nonempty into = ∅. But I will add tags for e.g. the same rule for Finset.

I agree it would be nice to support rcases patterns in by_cases! (and by_cases), but I'm not sure what the syntax should be, given that the same variable name refers to two different introduced variables. Maybe we can have syntax by_cases! (rfl | h) : a = ∅.

[Jovan Gerbscheid]

Here's my PR for by_cases!: #30073

[Jovan Gerbscheid]

I've now split the tactic implementation of by_cases! into a separate PR: #30730