## Stream: new members

### Topic: Contraposition Proof

#### Cameron Crossman (Dec 03 2018 at 23:36):

I am a new user and I am just getting my bearings with the platform. Would someone be able to walk me through a proof of Contraposition written in Lean? (p → q) → (¬q → ¬p). Much appreciated! I know the general steps but am getting confused about how to translate that into Lean.
(p → q)
¬(p ^ ¬q)
¬( ¬q ^ p)
r = ¬q, s = ¬p substitution
¬(r ^ ¬s )
(r → s)
substitute back in
¬q → ¬p

#### Kevin Buzzard (Dec 03 2018 at 23:40):

In tactic mode? If you keep using the intro tactic you will find yourself with hypotheses p->q, not q and p and with a goal of false. Now apply your hypotheses until you're done. Sorry, on phone and just off to bed, hope this helps

#### Mario Carneiro (Dec 04 2018 at 00:40):

Lean's logic is similar to natural deduction, where ¬p means p -> false so the proof is actually a lot easier than the one you sketched

#### Bryan Gin-ge Chen (Dec 04 2018 at 01:35):

Here's the proof in lean core, called "mt" for "modus tollens".

#### Cameron Crossman (Dec 04 2018 at 01:40):

Thank you!

Last updated: May 16 2021 at 22:14 UTC