contrapose

Stream: general

[Johan Commelin]

@Patrick Massot I have a feature request.
I would like to do contrapose foo with bar. Because now the hypothesis name just gets reused, but this can create severe semantic dissonance.

[Johan Commelin]

H_nonzero : y ≠ 0
⊢ ⇑l q ≠ 0

[Johan Commelin]

contrapose! H_nonzero

[Johan Commelin]

H_nonzero : ⇑l q = 0
⊢ y = 0

[Kevin Buzzard]

I just do intro bar, apply foo which I think is shorter! I didn't know about contrapose

[Kevin Buzzard]

But it sounds good for beginners.

[Rob Lewis]

I just used contrapose for the first time today in the sensitivity proof. It's suprisingly useful, especially the ! variant that fixes double negations.

[Rob Lewis]

https://github.com/leanprover-community/mathlib/pull/1302

[Johan Commelin]

Right, with ! it is really powerful. It fixes double negations, but also changes \not \exists into \forall and vice versa.

[Johan Commelin]

And it does this recursively

[Johan Commelin]

(This feature is also available standalone, as push_neg)

[Johan Commelin]

Once again: kudos to @Patrick Massot

[Johan Commelin]

@Rob Lewis does #1302 also clear the old hypothesis?

[Johan Commelin]

Because that would make sense, I think. Otherwise you end up with a hypothesis that is the negation of the goal. Pretty useless, as long as Lean is consistent :wink:

[Rob Lewis]

Yes, it reverts the old hypothesis, contraposes the goal, then introduces the new hypothesis with the new name.

[Johan Commelin]

Awesome!

[Johan Commelin]

Sometimes contrapose fails because I'm not in classical mode. What do people think of enhancing contrapose so that it invokes classical automatically in such cases?

[Patrick Massot]

Indeed this tactic doesn't make much sense in anon-classical context. It could start with classical.

[Johan Commelin]

Well, sometimes it works... If you're doing fake proof by contradiction.