by_contra!

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have a name for by_contra H, push_neg at H?

[Kevin Buzzard]

Is it something like contrapose!?

[Anne Baanen]

Not really, since contrapose needs an implication. Well, perhaps by { have : true := \<\>, contrapose! this }? :P

[Yury G. Kudryashov]

contrapose! needs an assumption.

[Anne Baanen]

by_contra is in core, so I don't think we can easily extend it

[Yury G. Kudryashov]

Can we extend contrapose! to act like by_contra! if called without arguments? Currently it expects the goal to be an implication in this case.

[Yaël Dillies]

Oh yeah, good idea. I wanted something like that a while back.

[Patrick Massot]

Having contrapose! acting as by_contra! would be weird. You wouldn't call that a contraposition on paper.

[Yury G. Kudryashov]

OK, then we can have by_contra'.

[Yury G. Kudryashov]

(though it's the same word)