RFC: contrapose for `a ↔ b`

Stream: mathlib4

[Jovan Gerbscheid]

Would it be a reasonable feature for contrapose/contrapose!, when applied to a goal a ↔ b, to turn it into ¬ a ↔ ¬ b? This doesn't interfere with the current behaviour, since contrapose without arguments only works when the goal is of the form a → b, turning it into ¬ b → ¬ a.

[Weiyi Wang]

The current magic spell for this is rw [← not_iff_not] but it always takes me some time to remember it / find it

[Jovan Gerbscheid]

And usually, you want to push the negation as well, so contrapose! would do this conveniently.

[Jireh Loreaux]

I like this.

[Jovan Gerbscheid]

A somewhat orthogonal idea I had is that it might be nice for contrapose (without the !) to cancel out a negation that is already present. So it would e.g. replace a → ¬ b with b → ¬ a. This way, it is not "pushing" the negation, but just "cancelling" it. Note that the by_contra and absurd tactics already have this feature.

I can imagine that one might not want to run the full power of push_neg (i.e. not use contrapose!), but I cannot imagine why one wouldn't want to cancel out a double negation. (And doing this with a single lemma would create smaller proof terms, and avoid classical logic sometimes)

[Patrick Massot]

About contrapose for equivalences, I think it would be nice to include an option to turn it off, for people who directly use contrapose for teaching.

[Michael Rothgang]

Jovan just made #31510 which does this (including a teaching option). I'm reviewing it, and have a specification question: do we prefer contrapose on a ↔ b to yield ¬ a ↔ ¬ b or ¬ b ↔ ¬ a?

[Michael Rothgang]

I would have expected the latter (and that matches the behaviour for implications). What do others think? Let's have a poll:

[Michael Rothgang]

/poll What should contrapose do to a bi-implication a ↔ b?
¬ a ↔ ¬ b
¬ b ↔ ¬ a
nothing, i.e. this thread is a bad idea