bookshelf/Bookshelf/Avigad/Chapter_4.lean

262 lines
7.4 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.

/-! # Avigad.Chapter4
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 Avigad.Chapter4
namespace ex1
variable (α : Type _)
variable (p q : α → Prop)
theorem forall_and
: (∀ 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⟩)
theorem forall_imp_distrib
: (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun h₁ h₂ x =>
have px : p x := h₂ x
h₁ x px
theorem forall_or_distrib
: (∀ 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)
theorem self_imp_forall : α → ((∀ _ : α, r) ↔ r) :=
fun a => Iff.intro (fun h => h a) (fun hr _ => hr)
section
open Classical
theorem forall_or_right : (∀ 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
theorem forall_swap : (∀ 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)
theorem barber_paradox (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)
theorem exists_imp : (∃ _ : α, r) → r :=
fun ⟨_, hr⟩ => hr
theorem exists_intro (a : α) : r → (∃ _ : α, r) :=
fun hr => ⟨a, hr⟩
theorem exists_and_right : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
Iff.intro
(fun ⟨hx, ⟨hp, hr⟩⟩ => ⟨⟨hx, hp⟩, hr⟩)
(fun ⟨⟨hx, hp⟩, hr⟩ => ⟨hx, ⟨hp, hr⟩⟩)
theorem exists_or : (∃ 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⟩))
theorem forall_iff_not_exists : (∀ x, p x) ↔ ¬(∃ x, ¬p x) :=
Iff.intro
(fun h ⟨hx, np⟩ => np (h hx))
(fun h hx => byContradiction
fun np => h ⟨hx, np⟩)
theorem exists_iff_not_forall : (∃ 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⟩))
theorem not_exists : (¬∃ 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)
theorem not_forall : (¬∀ x, p x) ↔ (∃ x, ¬p x) :=
forall_negation α p
theorem forall_iff_exists_imp : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
Iff.intro
(fun h ⟨hx, hp⟩ => h hx hp)
(fun h hx hp => h ⟨hx, hp⟩)
theorem exists_iff_forall_imp (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⟩))
theorem exists_self_iff_self_exists (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)
theorem exp_add_mul_exp (x y z : Float)
: exp (x + y + z) = exp x * exp y * exp z :=
by rw [exp_add, exp_add]
theorem exp_log_eq_self (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
end Avigad.Chapter4