Avigad.Chapter5

Tactics

Exercise 1

Go back to the exercises in Chapter 3 and Chapter 4 and redo as many as you can now with tactic proofs, using also rw and simp as appropriate.

Exercises 3.1

theorem Avigad.Chapter5.ex1.and_comm' (p : Prop) (q : Prop) : p ∧ q ↔ q ∧ p

theorem Avigad.Chapter5.ex1.or_comm' (p : Prop) (q : Prop) : p ∨ q ↔ q ∨ p

theorem Avigad.Chapter5.ex1.and_assoc (p : Prop) (q : Prop) (r : Prop) : (p ∧ q) ∧ r ↔ p ∧ q ∧ r

theorem Avigad.Chapter5.ex1.or_assoc' (p : Prop) (q : Prop) (r : Prop) : (p ∨ q) ∨ r ↔ p ∨ q ∨ r

theorem Avigad.Chapter5.ex1.and_or_left (p : Prop) (q : Prop) (r : Prop) : p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r

theorem Avigad.Chapter5.ex1.or_and_left (p : Prop) (q : Prop) (r : Prop) : p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)

theorem Avigad.Chapter5.ex1.imp_imp_iff_and_imp (p : Prop) (q : Prop) (r : Prop) : p → q → r ↔ p ∧ q → r

theorem Avigad.Chapter5.ex1.or_imp (p : Prop) (q : Prop) (r : Prop) : p ∨ q → r ↔ (p → r) ∧ (q → r)

theorem Avigad.Chapter5.ex1.nor_or (p : Prop) (q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q

theorem Avigad.Chapter5.ex1.not_and_or_mpr (p : Prop) (q : Prop) : ¬p ∨ ¬q → ¬(p ∧ q)

theorem Avigad.Chapter5.ex1.and_not_self (p : Prop) : ¬(p ∧ ¬p)

theorem Avigad.Chapter5.ex1.not_imp_o_and_not (p : Prop) (q : Prop) : p ∧ ¬q → ¬(p → q)

theorem Avigad.Chapter5.ex1.false_elim_self (p : Prop) (q : Prop) : ¬p → p → q

theorem Avigad.Chapter5.ex1.not_or_imp_imp (p : Prop) (q : Prop) : ¬p ∨ q → p → q

theorem Avigad.Chapter5.ex1.or_false_iff (p : Prop) : p ∨ False ↔ p

theorem Avigad.Chapter5.ex1.and_false_iff (p : Prop) : p ∧ False ↔ False

theorem Avigad.Chapter5.ex1.imp_imp_not_imp_not (p : Prop) (q : Prop) : (p → q) → ¬q → ¬p

Exercises 3.2

theorem Avigad.Chapter5.ex1.imp_or_mp (p : Prop) (r : Prop) (s : Prop) (hp : p) : (p → r ∨ s) → (p → r) ∨ (p → s)

theorem Avigad.Chapter5.ex1.not_and_iff_or_not (p : Prop) (q : Prop) : ¬(p ∧ q) → ¬p ∨ ¬q

theorem Avigad.Chapter5.ex1.not_imp_mp (p : Prop) (q : Prop) : ¬(p → q) → p ∧ ¬q

theorem Avigad.Chapter5.ex1.not_or_of_imp (p : Prop) (q : Prop) : (p → q) → ¬p ∨ q

theorem Avigad.Chapter5.ex1.not_imp_not_imp_imp (p : Prop) (q : Prop) : (¬q → ¬p) → p → q

theorem Avigad.Chapter5.ex1.or_not (p : Prop) : p ∨ ¬p

theorem Avigad.Chapter5.ex1.imp_imp_imp (p : Prop) (q : Prop) : ((p → q) → p) → p

Exercises 3.3

theorem Avigad.Chapter5.ex1.iff_not_self (p : Prop) (hp : p) : ¬(p ↔ ¬p)

Exercises 4.1

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

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

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

Exercises 4.2

theorem Avigad.Chapter5.ex1.self_imp_forall (α : Type u_1) (r : Prop) : α → (α → r ↔ r)

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

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

Exercises 4.3

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

Exercises 4.5

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

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

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

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

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

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

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

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

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

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

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

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

Exercise 2

Use tactic combinators to obtain a one line proof of the following:

theorem Avigad.Chapter5.ex2.or_and_or_and_or (p : Prop) (q : Prop) (r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p)