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.

theorem Avigad.Chapter4.ex1.forall_and (α : Type u_1) (p : α → Prop) (q : α → Prop) : (∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x

theorem Avigad.Chapter4.ex1.forall_imp_distrib (α : Type u_1) (p : α → Prop) (q : α → Prop) : (∀ (x : α), p x → q x) → (∀ (x : α), p x) → ∀ (x : α), q x

theorem Avigad.Chapter4.ex1.forall_or_distrib (α : Type u_1) (p : α → Prop) (q : α → Prop) : ((∀ (x : α), p x) ∨ ∀ (x : α), q x) → ∀ (x : α), p x ∨ q x

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).

theorem Avigad.Chapter4.ex2.self_imp_forall (α : Type u_1) (r : Prop) : α → (α → r ↔ r)

theorem Avigad.Chapter4.ex2.forall_or_right (α : Type u_1) (p : α → Prop) (r : Prop) : (∀ (x : α), p x ∨ r) ↔ (∀ (x : α), p x) ∨ r

theorem Avigad.Chapter4.ex2.forall_swap (α : Type u_1) (p : α → Prop) (r : Prop) : (∀ (x : α), r → p x) ↔ r → ∀ (x : α), p x

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.

theorem Avigad.Chapter4.ex3.barber_paradox (men : Type u_1) (barber : men) (shaves : men → men → Prop) (h : ∀ (x : men), shaves barber x ↔ ¬shaves x x) : False

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. Goldbach’s 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.

def Avigad.Chapter4.ex4.even (a : Nat) : Prop

Equations

• Avigad.Chapter4.ex4.even a = ∃ (b : Nat), a = 2 * b

def Avigad.Chapter4.ex4.odd (a : Nat) : Prop

Equations

• Avigad.Chapter4.ex4.odd a = ¬Avigad.Chapter4.ex4.even a

def Avigad.Chapter4.ex4.prime (n : Nat) : Prop

Equations

• Avigad.Chapter4.ex4.prime n = (n > 1 ∧ ∀ (m : Nat), 1 < m ∧ m < n → n % m ≠ 0)

def Avigad.Chapter4.ex4.infinitelyManyPrimes : Prop

Equations

• Avigad.Chapter4.ex4.infinitelyManyPrimes = ∀ (n : Nat), ∃ (m : Nat), m > n ∧ Avigad.Chapter4.ex4.prime m

def Avigad.Chapter4.ex4.FermatPrime (n : Nat) : Prop

Equations

• Avigad.Chapter4.ex4.FermatPrime n = ∃ (m : Nat), n = 2 ^ 2 ^ m + 1

def Avigad.Chapter4.ex4.infinitelyManyFermatPrimes : Prop

Equations

• Avigad.Chapter4.ex4.infinitelyManyFermatPrimes = ∀ (n : Nat), ∃ (m : Nat), m > n ∧ Avigad.Chapter4.ex4.FermatPrime m

def Avigad.Chapter4.ex4.GoldbachConjecture : Prop

Equations

• One or more equations did not get rendered due to their size.

def Avigad.Chapter4.ex4.Goldbach'sWeakConjecture : Prop

Equations

• One or more equations did not get rendered due to their size.

def Avigad.Chapter4.ex4.Fermat'sLastTheorem : Prop

Equations

• Avigad.Chapter4.ex4.Fermat'sLastTheorem = ∀ (n : Nat), n > 2 → ∀ (a b c : Nat), a ^ n + b ^ n ≠ c ^ n

Exercise 5

Prove as many of the identities listed in Section 4.4 as you can.

theorem Avigad.Chapter4.ex5.exists_imp (α : Type u_1) (r : Prop) : (∃ (x : α), r) → r

theorem Avigad.Chapter4.ex5.exists_intro (α : Type u_1) (r : Prop) (a : α) : r → ∃ (x : α), r

theorem Avigad.Chapter4.ex5.exists_and_right (α : Type u_1) (p : α → Prop) (r : Prop) : (∃ (x : α), p x ∧ r) ↔ (∃ (x : α), p x) ∧ r

theorem Avigad.Chapter4.ex5.exists_or (α : Type u_1) (p : α → Prop) (q : α → Prop) : (∃ (x : α), p x ∨ q x) ↔ (∃ (x : α), p x) ∨ ∃ (x : α), q x

theorem Avigad.Chapter4.ex5.forall_iff_not_exists (α : Type u_1) (p : α → Prop) : (∀ (x : α), p x) ↔ ¬∃ (x : α), ¬p x

theorem Avigad.Chapter4.ex5.exists_iff_not_forall (α : Type u_1) (p : α → Prop) : (∃ (x : α), p x) ↔ ¬∀ (x : α), ¬p x

theorem Avigad.Chapter4.ex5.not_exists (α : Type u_1) (p : α → Prop) : (¬∃ (x : α), p x) ↔ ∀ (x : α), ¬p x

theorem Avigad.Chapter4.ex5.forall_negation (α : Type u_1) (p : α → Prop) : (¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x

theorem Avigad.Chapter4.ex5.not_forall (α : Type u_1) (p : α → Prop) : (¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x

theorem Avigad.Chapter4.ex5.forall_iff_exists_imp (α : Type u_1) (p : α → Prop) (r : Prop) : (∀ (x : α), p x → r) ↔ (∃ (x : α), p x) → r

theorem Avigad.Chapter4.ex5.exists_iff_forall_imp (α : Type u_1) (p : α → Prop) (r : Prop) (a : α) : (∃ (x : α), p x → r) ↔ (∀ (x : α), p x) → r

theorem Avigad.Chapter4.ex5.exists_self_iff_self_exists (α : Type u_1) (p : α → Prop) (r : Prop) (a : α) : (∃ (x : α), r → p x) ↔ r → ∃ (x : α), p x

Exercise 6

Give a calculational proof of the theorem log_mul below.

theorem Avigad.Chapter4.ex6.exp_add_mul_exp (exp : Float → Float) (exp_add : ∀ (x y : Float), exp (x + y) = exp x * exp y) (x : Float) (y : Float) (z : Float) : exp (x + y + z) = exp x * exp y * exp z

theorem Avigad.Chapter4.ex6.exp_log_eq_self (log : Float → Float) (exp : Float → Float) (exp_log_eq : ∀ {x : Float}, x > 0 → exp (log x) = x) (y : Float) (h : y > 0) : exp (log y) = y

theorem Avigad.Chapter4.ex6.log_mul (log : Float → Float) (exp : Float → Float) (log_exp_eq : ∀ (x : Float), log (exp x) = x) (exp_log_eq : ∀ {x : Float}, x > 0 → exp (log x) = x) (exp_add : ∀ (x y : Float), exp (x + y) = exp x * exp y) {x : Float} {y : Float} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y