A De Morgan law
Show ¬(P ∨ Q) gives ¬P ∧ ¬Q, combining everything so far.
In this course 8 / 11
One of De Morgan’s laws says that if neither P nor Q holds, then P does not hold and Q does not hold: ¬(P ∨ Q) → ¬P ∧ ¬Q. This direction needs no classical reasoning, and it uses every move in this course.
The goal ¬P ∧ ¬Q is a conjunction, so constructor gives ⊢ ¬P and ⊢ ¬Q. Each of those is an implication into False, so each branch opens with intro.
Inside a branch you need False, and the only thing in the context that produces False is h. But h demands a proof of a disjunction, and nothing in the context is one yet. You have to build it from what the intro just gave you.
This is where Or.inl and Or.inr appear as terms rather than as the left and right tactics. The disjunction is not the goal; it is an argument you are handing to a hypothesis. The worked example proves the converse, where the disjunction arrives as an assumption and is consumed by cases instead.
Worked example
example (A B : Prop) (h : ¬A ∧ ¬B) : ¬(A ∨ B) := by
intro hab
cases hab with
| inl ha => exact h.1 ha
| inr hb => exact h.2 hbThis is the other direction of the same law, and the moves run backwards: the conjunction is taken apart with .1 and .2, and the disjunction is consumed by cases. In your exercise the conjunction is the goal and the disjunction is built.
Large proofs are small moves stacked up: split the goal, introduce what you may assume, then build the exact term a hypothesis is asking for.
- 14. Classical De Morgan Medium
Prove ¬P ∧ ¬Q from h : ¬(P ∨ Q).
Suggested steps
- Split the conjunction
- In the first branch, build the left disjunct
- In the second branch, build the right disjunct
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