modus tollens in context

Stream: Is there code for X?

[Patrick Thomas]

If I have P -> Q in the context, is there a tactic to get ~Q -> ~P, or if I have both P -> Q and ~Q to get ~P?

[Yury G. Kudryashov]

I usually write term mode proofs in this case, see docs#mt.

[Yury G. Kudryashov]

E.g., you can write have h' := mt h or have h' := mt hpq hq.

[Yury G. Kudryashov]

Probably you can do something like have h' : not P := by tauto.

[Yury G. Kudryashov]

See also by_contra tactic and tactic#contrapose

[Patrick Thomas]

Thank you.