# Zulip Chat Archive

## 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