Prove a contrapositive
From P → Q and ¬Q, build ¬P by introducing an assumed P.
In this course 7 / 11
From P → Q and ¬Q, conclude ¬P. Once you remember that ¬X is X → False, this is composition: P → Q followed by Q → False is P → False.
The goal ¬P is an implication, so intro hp works on it. The state becomes hp : P above the line and ⊢ False below. From there you follow the implications until something produces False.
Parentheses are not decoration. hnq (hpq hp) applies hpq to hp first and feeds the result into hnq. Without them, hnq hpq hp means applying hnq to two arguments, which it does not take, and the error talks about a function type rather than about your reasoning.
The worked example stretches the chain to two functions so the nesting is visible: the innermost application runs first, and each layer outwards consumes the result of the one inside it.
Worked example
example (A B C : Prop) (f : A → B) (g : B → C) (hnc : ¬C) : ¬A := by
intro ha
exact hnc (g (f ha))Read hnc (g (f ha)) from the inside out: f ha : B, then g (f ha) : C, then hnc of that is False. Your exercise runs a chain of the same shape twice, entering it at a different point each time, because both negations have to be proved.
To prove ¬P, assume P and derive False. Composing implications gives the contrapositive.
- 5. Contrapositive Easy
Push a negation back along a chain of two implications, to both of its earlier points.
Suggested steps
- Split the two negations
- Assume P and travel the whole chain
- Assume Q and travel what is left of it
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct