Zulip Chat Archive

Stream: new members

Topic: Contraposition Proof

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Dec 04 2018 at 01:35):

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

view this post on Zulip Cameron Crossman (Dec 04 2018 at 01:40):

Thank you!

Last updated: May 16 2021 at 22:14 UTC