bookshelf/Exercises/Avigad/Chapter5.lean

464 lines
10 KiB
Plaintext
Raw Normal View History

2023-05-04 22:37:54 +00:00
/-! # Exercises.Avigad.Chapter5
2023-04-02 14:57:58 +00:00
Tactics
-/
2023-05-04 22:37:54 +00:00
/-! #### 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.
-/
namespace Exercises.Avigad.Chapter5
2023-04-08 16:32:20 +00:00
2023-02-10 21:51:20 +00:00
namespace ex1
2023-05-04 22:37:54 +00:00
/-! ##### Exercises 3.1 -/
2023-02-10 21:51:20 +00:00
section ex3_1
2023-02-10 21:51:20 +00:00
variable (p q r : Prop)
2023-02-10 21:51:20 +00:00
-- Commutativity of ∧ and
2023-05-04 22:37:54 +00:00
theorem and_comm' : p ∧ q ↔ q ∧ p := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro ⟨hp, hq⟩
exact ⟨hq, hp⟩
· intro ⟨hq, hp⟩
exact ⟨hp, hq⟩
2023-05-04 22:37:54 +00:00
theorem or_comm' : p q ↔ q p := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro
| Or.inl hp => exact Or.inr hp
| Or.inr hq => exact Or.inl hq
· intro
| Or.inl hq => exact Or.inr hq
| Or.inr hp => exact Or.inl hp
2023-02-10 21:51:20 +00:00
-- Associativity of ∧ and
2023-05-04 22:37:54 +00:00
theorem and_assoc : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro ⟨⟨hp, hq⟩, hr⟩
exact ⟨hp, hq, hr⟩
· intro ⟨hp, hq, hr⟩
exact ⟨⟨hp, hq⟩, hr⟩
2023-05-04 22:37:54 +00:00
theorem or_assoc' : (p q) r ↔ p (q r) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro
| Or.inl (Or.inl hp) => exact Or.inl hp
| Or.inl (Or.inr hq) => exact Or.inr (Or.inl hq)
| Or.inr hr => exact Or.inr (Or.inr hr)
· intro
| Or.inl hp => exact Or.inl (Or.inl hp)
| Or.inr (Or.inl hq) => exact Or.inl (Or.inr hq)
| Or.inr (Or.inr hr) => exact Or.inr hr
-- Distributivity
2023-05-04 22:37:54 +00:00
theorem and_or_left : p ∧ (q r) ↔ (p ∧ q) (p ∧ r) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro
| ⟨hp, Or.inl hq⟩ => exact Or.inl ⟨hp, hq⟩
| ⟨hp, Or.inr hr⟩ => exact Or.inr ⟨hp, hr⟩
· intro
| Or.inl ⟨hp, hq⟩ => exact ⟨hp, Or.inl hq⟩
| Or.inr ⟨hp, hr⟩ => exact ⟨hp, Or.inr hr⟩
2023-05-04 22:37:54 +00:00
theorem or_and_left : p (q ∧ r) ↔ (p q) ∧ (p r) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro
| Or.inl hp => exact ⟨Or.inl hp, Or.inl hp⟩
| Or.inr ⟨hq, hr⟩ => exact ⟨Or.inr hq, Or.inr hr⟩
· intro
| ⟨Or.inl hp, _⟩ => exact Or.inl hp
| ⟨Or.inr _, Or.inl hp⟩ => exact Or.inl hp
| ⟨Or.inr hq, Or.inr hr⟩ => exact Or.inr ⟨hq, hr⟩
-- Other properties
2023-05-04 22:37:54 +00:00
theorem imp_imp_iff_and_imp : (p → (q → r)) ↔ (p ∧ q → r) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro h ⟨hp, hq⟩
exact h hp hq
· intro h hp hq
exact h ⟨hp, hq⟩
2023-05-04 22:37:54 +00:00
theorem or_imp : ((p q) → r) ↔ (p → r) ∧ (q → r) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro h
apply And.intro
· intro hp
exact h (Or.inl hp)
· intro hq
exact h (Or.inr hq)
· intro ⟨hpr, hqr⟩ h
apply Or.elim h
· intro hp
exact hpr hp
· intro hq
exact hqr hq
2023-05-04 22:37:54 +00:00
theorem nor_or : ¬(p q) ↔ ¬p ∧ ¬q := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro h
apply And.intro
· intro hp
exact h (Or.inl hp)
· intro hq
exact h (Or.inr hq)
· intro ⟨np, nq⟩
intro
| Or.inl hp => exact absurd hp np
| Or.inr hq => exact absurd hq nq
2023-05-04 22:37:54 +00:00
theorem not_and_or_mpr : ¬p ¬q → ¬(p ∧ q) := by
2023-02-10 21:51:20 +00:00
intro
| Or.inl np => intro h; exact absurd h.left np
| Or.inr nq => intro h; exact absurd h.right nq
2023-05-04 22:37:54 +00:00
theorem and_not_self : ¬(p ∧ ¬p) := by
2023-02-10 21:51:20 +00:00
intro ⟨hp, np⟩
exact absurd hp np
2023-05-04 22:37:54 +00:00
theorem not_imp_o_and_not : p ∧ ¬q → ¬(p → q) := by
2023-02-10 21:51:20 +00:00
intro ⟨hp, nq⟩ h
exact absurd (h hp) nq
2023-05-04 22:37:54 +00:00
theorem false_elim_self : ¬p → (p → q) := by
2023-02-10 21:51:20 +00:00
intro np hp
exact absurd hp np
2023-05-04 22:37:54 +00:00
theorem not_or_imp_imp : (¬p q) → (p → q) := by
2023-02-10 21:51:20 +00:00
intro
| Or.inl np => intro hp; exact absurd hp np
| Or.inr hq => exact fun _ => hq
2023-05-04 22:37:54 +00:00
theorem or_false_iff : p False ↔ p := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro
| Or.inl hp => exact hp
| Or.inr ff => exact False.elim ff
· intro hp
exact Or.inl hp
2023-05-04 22:37:54 +00:00
theorem and_false_iff : p ∧ False ↔ False := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro ⟨_, ff⟩
exact ff
· intro ff
exact False.elim ff
2023-05-04 22:37:54 +00:00
theorem imp_imp_not_imp_not : (p → q) → (¬q → ¬p) := by
2023-02-10 21:51:20 +00:00
intro hpq nq hp
exact absurd (hpq hp) nq
end ex3_1
2023-05-04 22:37:54 +00:00
/-! ##### Exercises 3.2 -/
2023-02-10 21:51:20 +00:00
section ex3_2
open Classical
variable (p q r s : Prop)
2023-05-04 22:37:54 +00:00
theorem imp_or_mp (hp : p) : (p → r s) → ((p → r) (p → s)) := by
2023-02-10 21:51:20 +00:00
intro h
apply (h hp).elim
· intro hr
exact Or.inl (fun _ => hr)
· intro hs
exact Or.inr (fun _ => hs)
2023-05-04 22:37:54 +00:00
theorem not_and_iff_or_not : ¬(p ∧ q) → ¬p ¬q := by
2023-02-10 21:51:20 +00:00
intro h
apply (em p).elim
· intro hp
apply (em q).elim
· intro hq
exact False.elim (h ⟨hp, hq⟩)
· intro nq
exact Or.inr nq
· intro np
exact Or.inl np
2023-05-04 22:37:54 +00:00
theorem not_imp_mp : ¬(p → q) → p ∧ ¬q := by
2023-02-10 21:51:20 +00:00
intro h
apply And.intro
· apply byContradiction
intro np
apply h
intro hp
exact absurd hp np
· intro hq
apply h
intro _
exact hq
2023-05-04 22:37:54 +00:00
theorem not_or_of_imp : (p → q) → (¬p q) := by
2023-02-10 21:51:20 +00:00
intro hpq
apply (em p).elim
· intro hp
exact Or.inr (hpq hp)
· intro np
exact Or.inl np
2023-05-04 22:37:54 +00:00
theorem not_imp_not_imp_imp : (¬q → ¬p) → (p → q) := by
2023-02-10 21:51:20 +00:00
intro hqp hp
apply byContradiction
intro nq
exact absurd hp (hqp nq)
2023-05-04 22:37:54 +00:00
theorem or_not : p ¬p := by apply em
2023-02-10 21:51:20 +00:00
2023-05-04 22:37:54 +00:00
theorem imp_imp_imp : (((p → q) → p) → p) := by
2023-02-10 21:51:20 +00:00
intro h
apply (em p).elim
· intro hp
exact hp
· intro np
apply h
intro hp
exact absurd hp np
end ex3_2
2023-05-04 22:37:54 +00:00
/-! ##### Exercises 3.3 -/
2023-02-10 21:51:20 +00:00
section ex3_3
variable (p : Prop)
2023-05-04 22:37:54 +00:00
theorem iff_not_self (hp : p) : ¬(p ↔ ¬p) := by
2023-02-10 21:51:20 +00:00
intro h
exact absurd hp (h.mp hp)
end ex3_3
2023-05-04 22:37:54 +00:00
/-! ##### Exercises 4.1 -/
2023-02-10 21:51:20 +00:00
section ex4_1
variable (α : Type _)
variable (p q : α → Prop)
2023-05-04 22:37:54 +00:00
theorem forall_and : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro h
apply And.intro
· intro hx; exact And.left (h hx)
· intro hx; exact And.right (h hx)
· intro h hx
have lhs : ∀ (x : α), p x := And.left h
have rhs : ∀ (x : α), q x := And.right h
exact ⟨lhs hx, rhs hx⟩
2023-05-04 22:37:54 +00:00
theorem forall_imp_distrib : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) := by
2023-02-10 21:51:20 +00:00
intro h₁ h₂ hx
exact h₁ hx (h₂ hx)
2023-05-04 22:37:54 +00:00
theorem forall_or_distrib : (∀ x, p x) (∀ x, q x) → ∀ x, p x q x := by
2023-02-10 21:51:20 +00:00
intro
| Or.inl h => intro hx; exact Or.inl (h hx)
| Or.inr h => intro hx; exact Or.inr (h hx)
2023-02-10 21:51:20 +00:00
end ex4_1
2023-05-04 22:37:54 +00:00
/-! ##### Exercises 4.2 -/
2023-02-10 21:51:20 +00:00
section ex4_2
2023-02-10 21:51:20 +00:00
variable (α : Type _)
variable (p q : α → Prop)
variable (r : Prop)
2023-05-04 22:37:54 +00:00
theorem self_imp_forall : α → ((∀ _ : α, r) ↔ r) := by
2023-02-10 21:51:20 +00:00
intro ha
apply Iff.intro
· intro har
apply har
exact ha
· intro hr _
exact hr
section
2023-02-10 21:51:20 +00:00
open Classical
2023-05-04 22:37:54 +00:00
theorem forall_or_right : (∀ x, p x r) ↔ (∀ x, p x) r := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro h
apply (em r).elim
· intro hr
exact Or.inr hr
· intro nr
apply Or.inl
· intro hx
apply (h hx).elim
· exact id
· intro hr
exact absurd hr nr
· intro h₁ hx
apply h₁.elim
· intro h₂
exact Or.inl (h₂ hx)
· intro hr
exact Or.inr hr
end
2023-05-04 22:37:54 +00:00
theorem forall_swap : (∀ x, r → p x) ↔ (r → ∀ x, p x) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro h hr hx
exact h hx hr
· intro h hx hr
exact h hr hx
2023-02-10 21:51:20 +00:00
end ex4_2
2023-05-04 22:37:54 +00:00
/-! ##### Exercises 4.3 -/
2023-02-10 21:51:20 +00:00
section ex4_3
2023-02-10 21:51:20 +00:00
open Classical
2023-02-10 21:51:20 +00:00
variable (men : Type _)
variable (barber : men)
variable (shaves : men → men → Prop)
2023-05-04 22:37:54 +00:00
theorem barber_paradox (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x)
: False := by
2023-02-10 21:51:20 +00:00
apply (em (shaves barber barber)).elim
· intro hb
exact absurd hb ((h barber).mp hb)
· intro nb
exact absurd ((h barber).mpr nb) nb
2023-02-10 21:51:20 +00:00
end ex4_3
2023-05-04 22:37:54 +00:00
/-! ##### Exercises 4.5 -/
2023-02-10 21:51:20 +00:00
section ex4_5
2023-02-10 21:51:20 +00:00
open Classical
2023-02-10 21:51:20 +00:00
variable (α : Type _)
variable (p q : α → Prop)
variable (r s : Prop)
2023-05-04 22:37:54 +00:00
theorem exists_imp : (∃ _ : α, r) → r := by
2023-02-10 21:51:20 +00:00
intro ⟨_, hr⟩
exact hr
2023-05-04 22:37:54 +00:00
theorem exists_intro (a : α) : r → (∃ _ : α, r) := by
2023-02-10 21:51:20 +00:00
intro hr
exact ⟨a, hr⟩
2023-05-04 22:37:54 +00:00
theorem exists_and_right : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro ⟨hx, hp, hr⟩
exact ⟨⟨hx, hp⟩, hr⟩
· intro ⟨⟨hx, hp⟩, hr⟩
exact ⟨hx, hp, hr⟩
2023-05-04 22:37:54 +00:00
theorem exists_or : (∃ x, p x q x) ↔ (∃ x, p x) (∃ x, q x) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro
| ⟨hx, Or.inl hp⟩ => exact Or.inl ⟨hx, hp⟩
| ⟨hx, Or.inr hq⟩ => exact Or.inr ⟨hx, hq⟩
· intro
| Or.inl ⟨hx, hp⟩ => exact ⟨hx, Or.inl hp⟩
| Or.inr ⟨hx, hq⟩ => exact ⟨hx, Or.inr hq⟩
2023-05-04 22:37:54 +00:00
theorem forall_iff_not_exists : (∀ x, p x) ↔ ¬(∃ x, ¬p x) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro ha ⟨hx, np⟩
exact absurd (ha hx) np
· intro he hx
apply byContradiction
intro np
exact he ⟨hx, np⟩
2023-05-04 22:37:54 +00:00
theorem exists_iff_not_forall : (∃ x, p x) ↔ ¬(∀ x, ¬p x) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro ⟨hx, hp⟩ h
exact absurd hp (h hx)
· intro h₁
apply byContradiction
intro h₂
apply h₁
intro hx hp
exact h₂ ⟨hx, hp⟩
2023-05-04 22:37:54 +00:00
theorem not_exists : (¬∃ x, p x) ↔ (∀ x, ¬p x) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro h hx hp
exact h ⟨hx, hp⟩
2023-02-10 21:51:20 +00:00
· intro h ⟨hx, hp⟩
exact absurd hp (h hx)
2023-02-10 21:51:20 +00:00
theorem forall_negation : (¬∀ x, p x) ↔ (∃ x, ¬p x) := by
apply Iff.intro
· intro h₁
apply byContradiction
intro h₂
exact h₁ (fun (x : α) => by
apply byContradiction
intro np
exact h₂ ⟨x, np⟩)
· intro ⟨hx, np⟩ h
exact absurd (h hx) np
2023-05-04 22:37:54 +00:00
theorem not_forall : (¬∀ x, p x) ↔ (∃ x, ¬p x) := forall_negation α p
2023-02-10 21:51:20 +00:00
2023-05-04 22:37:54 +00:00
theorem forall_iff_exists_imp : (∀ x, p x → r) ↔ (∃ x, p x) → r := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro h ⟨hx, hp⟩
exact h hx hp
· intro h hx hp
exact h ⟨hx, hp⟩
2023-05-04 22:37:54 +00:00
theorem exists_iff_forall_imp (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro ⟨hx, hp⟩ h
apply hp
exact h hx
· intro h₁
apply (em (∀ x, p x)).elim
· intro h₂
exact ⟨a, fun _ => h₁ h₂⟩
· intro h₂
have ⟨hx, np⟩ : (∃ x, ¬p x) := (forall_negation α p).mp h₂
exact ⟨hx, fun hp => absurd hp np⟩
2023-05-04 22:37:54 +00:00
theorem exists_self_iff_self_exists (a : α)
: (∃ x, r → p x) ↔ (r → ∃ x, p x) := by
2023-02-10 21:51:20 +00:00
apply Iff.intro
· intro ⟨hx, h⟩ hr
exact ⟨hx, h hr⟩
· intro h
apply (em r).elim
· intro hr
have ⟨hx, hp⟩ := h hr
exact ⟨hx, fun _ => hp⟩
· intro nr
exact ⟨a, fun hr => absurd hr nr⟩
end ex4_5
end ex1
2023-05-04 22:37:54 +00:00
/-! #### Exercise 2
Use tactic combinators to obtain a one line proof of the following:
-/
2023-04-08 16:32:20 +00:00
2023-02-10 21:51:20 +00:00
namespace ex2
2023-05-04 22:37:54 +00:00
theorem or_and_or_and_or (p q r : Prop) (hp : p)
: (p q r) ∧ (q p r) ∧ (q r p) := by
simp [*]
2023-02-10 21:51:20 +00:00
end ex2
2023-05-04 22:37:54 +00:00
end Exercises.Avigad.Chapter5