bookshelf/TheoremProvingInLean/Chapter4.lean

260 lines
7.5 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

/-
Chapter 4
Quantifiers and Equality
-/
-- ========================================
-- Exercise 1
--
-- Prove these equivalences. You should also try to understand why the reverse
-- implication is not derivable in the last example.
-- ========================================
namespace ex1
variable (α : Type _)
variable (p q : α → Prop)
example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
Iff.intro
(fun h => ⟨fun x => And.left (h x), fun x => And.right (h x)⟩)
(fun ⟨h₁, h₂⟩ x => ⟨h₁ x, h₂ x⟩)
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun h₁ h₂ x =>
have px : p x := h₂ x
h₁ x px
example : (∀ x, p x) (∀ x, q x) → ∀ x, p x q x :=
fun h₁ x => h₁.elim
(fun h₂ => Or.inl (h₂ x))
(fun h₂ => Or.inr (h₂ x))
-- The implication in the above example cannot be proven in the other direction
-- because it may be the case predicate `p x` holds for certain values of `x`
-- but not others that `q x` may hold for (and vice versa).
end ex1
-- ========================================
-- Exercise 2
--
-- It is often possible to bring a component of a formula outside a universal
-- quantifier, when it does not depend on the quantified variable. Try proving
-- these (one direction of the second of these requires classical logic).
-- ========================================
namespace ex2
variable (α : Type _)
variable (p q : α → Prop)
variable (r : Prop)
example : α → ((∀ _ : α, r) ↔ r) :=
fun a => Iff.intro (fun h => h a) (fun hr _ => hr)
section
open Classical
example : (∀ x, p x r) ↔ (∀ x, p x) r :=
Iff.intro
(fun h₁ => (em r).elim
Or.inr
(fun nr => Or.inl (fun x => (h₁ x).elim id (absurd · nr))))
(fun h₁ => h₁.elim
(fun h₂ x => Or.inl (h₂ x))
(fun hr _ => Or.inr hr))
end
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
Iff.intro
(fun h hr hx => h hx hr)
(fun h hx hr => h hr hx)
end ex2
-- ========================================
-- Exercise 3
--
-- Consider the "barber paradox," that is, the claim that in a certain town
-- there is a (male) barber that shaves all and only the men who do not shave
-- themselves. Prove that this is a contradiction.
-- ========================================
namespace ex3
open Classical
variable (men : Type _)
variable (barber : men)
variable (shaves : men → men → Prop)
example (h : ∀ x : men, shaves barber x ↔ ¬shaves x x) : False :=
have b : shaves barber barber ↔ ¬shaves barber barber := h barber
(em (shaves barber barber)).elim
(fun b' => absurd b' (Iff.mp b b'))
(fun b' => absurd (Iff.mpr b b') b')
end ex3
-- ========================================
-- Exercise 4
--
-- Remember that, without any parameters, an expression of type `Prop` is just
-- an assertion. Fill in the definitions of `prime` and `Fermat_prime` below,
-- and construct each of the given assertions. For example, you can say that
-- there are infinitely many primes by asserting that for every natural number
-- `n`, there is a prime number greater than `n.` Goldbachs weak conjecture
-- states that every odd number greater than `5` is the sum of three primes.
-- Look up the definition of a Fermat prime or any of the other statements, if
-- necessary.
-- ========================================
namespace ex4
def even (a : Nat) := ∃ b, a = 2 * b
def odd (a : Nat) := ¬even a
def prime (n : Nat) : Prop :=
n > 1 ∧ ∀ (m : Nat), (1 < m ∧ m < n) → n % m ≠ 0
def infinitelyManyPrimes : Prop :=
∀ (n : Nat), (∃ (m : Nat), m > n ∧ prime m)
def FermatPrime (n : Nat) : Prop :=
∃ (m : Nat), n = 2^(2^m) + 1
def infinitelyManyFermatPrimes : Prop :=
∀ (n : Nat), (∃ (m : Nat), m > n ∧ FermatPrime m)
def GoldbachConjecture : Prop :=
∀ (n : Nat), even n ∧ n > 2 →
∃ (x y : Nat), prime x ∧ prime y ∧ x + y = n
def Goldbach'sWeakConjecture : Prop :=
∀ (n : Nat), odd n ∧ n > 5 →
∃ (x y z : Nat), prime x ∧ prime y ∧ prime z ∧ x + y + z = n
def Fermat'sLastTheorem : Prop :=
∀ (n : Nat), n > 2 → (∀ (a b c : Nat), a^n + b^n ≠ c^n)
end ex4
-- ========================================
-- Exercise 5
--
-- Prove as many of the identities listed in Section 4.4 as you can.
-- ========================================
namespace ex5
open Classical
variable (α : Type _)
variable (p q : α → Prop)
variable (r s : Prop)
example : (∃ _ : α, r) → r :=
fun ⟨_, hr⟩ => hr
example (a : α) : r → (∃ _ : α, r) :=
fun hr => ⟨a, hr⟩
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
Iff.intro
(fun ⟨hx, ⟨hp, hr⟩⟩ => ⟨⟨hx, hp⟩, hr⟩)
(fun ⟨⟨hx, hp⟩, hr⟩ => ⟨hx, ⟨hp, hr⟩⟩)
example : (∃ x, p x q x) ↔ (∃ x, p x) (∃ x, q x) :=
Iff.intro
(fun ⟨hx, hpq⟩ => hpq.elim
(fun hp => Or.inl ⟨hx, hp⟩)
(fun hq => Or.inr ⟨hx, hq⟩))
(fun h => h.elim
(fun ⟨hx, hp⟩ => ⟨hx, Or.inl hp⟩)
(fun ⟨hx, hq⟩ => ⟨hx, Or.inr hq⟩))
example : (∀ x, p x) ↔ ¬(∃ x, ¬p x) :=
Iff.intro
(fun h ⟨hx, np⟩ => np (h hx))
(fun h hx => byContradiction
fun np => h ⟨hx, np⟩)
example : (∃ x, p x) ↔ ¬(∀ x, ¬p x) :=
Iff.intro
(fun ⟨hx, hp⟩ h => absurd hp (h hx))
(fun h => byContradiction
fun h' => h (fun (x : α) hp => h' ⟨x, hp⟩))
example : (¬∃ x, p x) ↔ (∀ x, ¬p x) :=
Iff.intro
(fun h hx hp => h ⟨hx, hp⟩)
(fun h ⟨hx, hp⟩ => absurd hp (h hx))
theorem forall_negation : (¬∀ x, p x) ↔ (∃ x, ¬p x) :=
Iff.intro
(fun h => byContradiction
fun h' => h (fun (x : α) => byContradiction
fun np => h' ⟨x, np⟩))
(fun ⟨hx, np⟩ h => absurd (h hx) np)
example : (¬∀ x, p x) ↔ (∃ x, ¬p x) :=
forall_negation α p
example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
Iff.intro
(fun h ⟨hx, hp⟩ => h hx hp)
(fun h hx hp => h ⟨hx, hp⟩)
example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
Iff.intro
(fun ⟨hx, hp⟩ h => hp (h hx))
(fun h₁ => (em (∀ x, p x)).elim
(fun h₂ => ⟨a, fun _ => h₁ h₂⟩)
(fun h₂ =>
have h₃ : (∃ x, ¬p x) := Iff.mp (forall_negation α p) h₂
match h₃ with
| ⟨hx, hp⟩ => ⟨hx, fun hp' => absurd hp' hp⟩))
example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
Iff.intro
(fun ⟨hx, hrp⟩ hr => ⟨hx, hrp hr⟩)
(fun h => (em r).elim
(fun hr => match h hr with
| ⟨hx, hp⟩ => ⟨hx, fun _ => hp⟩)
(fun nr => ⟨a, fun hr => absurd hr nr⟩))
end ex5
-- ========================================
-- Exercise 6
--
-- Give a calculational proof of the theorem `log_mul` below.
-- ========================================
namespace ex6
variable (log exp : Float → Float)
variable (log_exp_eq : ∀ x, log (exp x) = x)
variable (exp_log_eq : ∀ {x}, x > 0 → exp (log x) = x)
variable (exp_pos : ∀ x, exp x > 0)
variable (exp_add : ∀ x y, exp (x + y) = exp x * exp y)
example (x y z : Float) : exp (x + y + z) = exp x * exp y * exp z :=
by rw [exp_add, exp_add]
example (y : Float) (h : y > 0) : exp (log y) = y := exp_log_eq h
theorem log_mul {x y : Float} (hx : x > 0) (hy : y > 0) :
log (x * y) = log x + log y :=
calc log (x * y) = log (x * exp (log y)) := by rw [exp_log_eq hy]
_ = log (exp (log x) * exp (log y)) := by rw [exp_log_eq hx]
_ = log (exp (log x + log y)) := by rw [exp_add]
_ = log x + log y := by rw [log_exp_eq]
end ex6