Below is a solution to a basic exercise from chapter 3 of "Theorem Proving in Lean 4". It shows, separately, both directions of the Theorem ¬(p ∨ q) ↔ ¬p ∧ ¬q.
The error message in both cases is identical -- function expected at xxx, term has type False. What confuses me is that False is exactly what I'm trying to show -- and exactly at that point in the code. Can someone explain what I'm missing?
theorem negAndOr_Fwd : ¬(p ∨ q) → ¬p ∧ ¬q :=
λ h: ¬(p ∨ q) =>
And.intro
λ hp:p =>
have hpq:(p ∨ q) := Or.inl hp
show False from h hpq -- What's wrong here?
λ hq:q => -- Error msg: "function expected at h hpq term has type False"
have hpq:(p ∨ q) := Or.inr hq
show False from hpq h
theorem negAndOr_Bwd : ¬p ∧ ¬q → ¬(p ∨ q) :=
λ h: (¬p ∧ ¬q) =>
have hnp:¬p := And.left h
have hnq:¬q := And.right h
λ hpq: (p ∨ q) => -- show ¬(p ∨ q) by showing that
hpq.elim -- both sides of the OR yield False
λ hp:p =>
show False from hnp hp -- Same msg here
λ hq:q =>
show False from hnq hq
The parser is confused due to missing parentheses. In your example, the parser sees the expression as show False from h hpq λ hq:q => ... as a single expression, and it is complaining that you can't call h hpq like a function with the following lambda because h hpq is a term of type False.
Corrected:
theorem negAndOr_Fwd : ¬(p ∨ q) → ¬p ∧ ¬q :=
λ h: ¬(p ∨ q) =>
And.intro
(λ hp:p =>
have hpq:(p ∨ q) := Or.inl hp
show False from h hpq)
(λ hq:q =>
have hpq:(p ∨ q) := Or.inr hq
show False from h hpq)
theorem negAndOr_Bwd : ¬p ∧ ¬q → ¬(p ∨ q) :=
λ h: (¬p ∧ ¬q) =>
have hnp:¬p := And.left h
have hnq:¬q := And.right h
λ hpq: (p ∨ q) =>
hpq.elim
(λ hp:p =>
show False from hnp hp)
(λ hq:q =>
show False from hnq hq)