Theorem Proving in Lean. Finish exercises 5.

finite-set-exercises
Joshua Potter 2023-02-08 09:41:23 -07:00
parent 497d2cbe5d
commit 7a0c03cdd4
2 changed files with 515 additions and 19 deletions

View File

@ -149,41 +149,38 @@ example : (∃ x : α, r) → r :=
example (a : α) : r → (∃ x : α, r) :=
assume hr,
exists.intro a hr
⟨a, hr⟩
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
iff.intro
(assume ⟨hx, ⟨hp, hr⟩⟩, ⟨exists.intro hx hp, hr⟩)
(assume ⟨⟨hx, hp⟩, hr⟩, exists.intro hx ⟨hp, hr⟩)
(assume ⟨hx, ⟨hp, hr⟩⟩, ⟨⟨hx, hp⟩, hr⟩)
(assume ⟨⟨hx, hp⟩, hr⟩, ⟨hx, ⟨hp, hr⟩⟩)
example : (∃ x, p x q x) ↔ (∃ x, p x) (∃ x, q x) :=
iff.intro
(assume ⟨hx, hpq⟩, hpq.elim
(assume hp, or.inl (exists.intro hx hp))
(assume hq, or.inr (exists.intro hx hq)))
(assume hp, or.inl (⟨hx, hp⟩))
(assume hq, or.inr (⟨hx, hq⟩)))
(assume h, h.elim
(assume ⟨hx, hp⟩, exists.intro hx (or.inl hp))
(assume ⟨hx, hq⟩, exists.intro hx (or.inr hq)))
(assume ⟨hx, hp⟩, ⟨hx, or.inl hp⟩)
(assume ⟨hx, hq⟩, ⟨hx, or.inr hq⟩))
example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
iff.intro
(assume h ⟨hx, np⟩, np (h hx))
(assume h hx, classical.by_contradiction (
assume np,
h (exists.intro hx np)
))
(assume h hx, classical.by_contradiction (assume np, h ⟨hx, np⟩))
example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
iff.intro
(assume ⟨hx, hp⟩ h, absurd hp (h hx))
(assume h, classical.by_contradiction (
assume h',
h (λ (x : α), assume hp, h' (exists.intro x hp))
h (λ (x : α), assume hp, h' ⟨x, hp⟩)
))
example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
iff.intro
(assume h hx hp, h (exists.intro hx hp))
(assume h hx hp, h ⟨hx, hp⟩)
(assume h ⟨hx, hp⟩, absurd hp (h hx))
lemma forall_negation : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
@ -192,7 +189,7 @@ lemma forall_negation : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
assume h',
h (λ (x : α), classical.by_contradiction (
assume np,
h' (exists.intro x np)
h' ⟨x, np⟩
))
))
(assume ⟨hx, np⟩ h, absurd (h hx) np)
@ -209,21 +206,21 @@ example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
iff.intro
(assume ⟨hx, hp⟩ h, hp (h hx))
(assume h₁, or.elim (classical.em (∀ x, p x))
(assume h₂, exists.intro a (assume hp, h₁ h₂))
(assume h₂, ⟨a, assume hp, h₁ h₂⟩)
(assume h₂,
have h₃ : (∃ x, ¬p x), from iff.elim_left (forall_negation α p) h₂,
match h₃ with
⟨hx, hp⟩ := exists.intro hx (assume hp', absurd hp' hp)
⟨hx, hp⟩ := ⟨hx, (assume hp', absurd hp' hp)⟩
end))
example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
iff.intro
(assume ⟨hx, hrp⟩ hr, exists.intro hx (hrp hr))
(assume ⟨hx, hrp⟩ hr, ⟨hx, hrp hr⟩)
(assume h, or.elim (classical.em r)
(assume hr, match h hr with
⟨hx, hp⟩ := exists.intro hx (assume hr, hp)
⟨hx, hp⟩ := ⟨hx, (assume hr, hp)⟩
end)
(assume nr, exists.intro a (assume hr, absurd hr nr)))
(assume nr, ⟨a, (assume hr, absurd hr nr)⟩))
end ex_5

View File

@ -0,0 +1,499 @@
/- Exercises 5.8
-
- Avigad, Jeremy. Theorem Proving in Lean, n.d.
-/
import tactic.rcases
-- 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.
section ex_1_3_1
variables p q r : Prop
-- Commutativity of ∧ and
example : p ∧ q ↔ q ∧ p :=
begin
split,
{ rintro ⟨p, q⟩, exact ⟨q, p⟩ },
{ rintro ⟨q, p⟩, exact ⟨p, q⟩ },
end
example : p q ↔ q p :=
begin
split,
{ rintro (p | q),
{ exact or.inr p },
{ exact or.inl q },
},
{ rintro (q | p),
{ exact or.inr q },
{ exact or.inl p },
},
end
-- Associativity of ∧ and
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
begin
split,
{ rintro ⟨⟨p, q⟩, r⟩, exact ⟨p, q, r⟩ },
{ rintro ⟨p, q, r⟩, exact ⟨⟨p, q⟩, r⟩ },
end
example : (p q) r ↔ p (q r) :=
begin
split,
{ rintro ((p | q) | r),
{ exact or.inl p },
{ exact or.inr (or.inl q) },
{ exact or.inr (or.inr r) },
},
{ rintro (p | q | r),
{ exact or.inl (or.inl p) },
{ exact or.inl (or.inr q) },
{ exact or.inr r },
},
end
-- Distributivity
example : p ∧ (q r) ↔ (p ∧ q) (p ∧ r) :=
begin
split,
{ rintro ⟨p, (q | r)⟩,
{ exact or.inl ⟨p, q⟩ },
{ exact or.inr ⟨p, r⟩ },
},
{ rintro (⟨p, q⟩ | ⟨p, r⟩),
{ exact ⟨p, or.inl q⟩ },
{ exact ⟨p, or.inr r⟩ },
},
end
example : p (q ∧ r) ↔ (p q) ∧ (p r) :=
begin
split,
{ rintro (p | ⟨q, r⟩),
{ exact ⟨or.inl p, or.inl p⟩ },
{ exact ⟨or.inr q, or.inr r⟩ },
},
{ rintro ⟨(p | q), (p | r)⟩;
exact or.inl p <|> exact or.inr ⟨q, r⟩,
},
end
-- Other properties
example : (p → (q → r)) ↔ (p ∧ q → r) :=
begin
split,
{ rintros h ⟨hp, hq⟩, exact h hp hq },
{ intros h hp hq, exact h ⟨hp, hq⟩ },
end
example : ((p q) → r) ↔ (p → r) ∧ (q → r) :=
begin
split,
{ intros h₁,
split,
{ intro p, exact h₁ (or.inl p) },
{ intro q, exact h₁ (or.inr q) },
},
{ rintros ⟨hp, hq⟩ h,
apply or.elim h,
{ intro p, exact hp p },
{ intro q, exact hq q },
},
end
example : ¬(p q) ↔ ¬p ∧ ¬q :=
begin
split,
{ intro h,
split,
{ intro hp, apply h, exact or.inl hp },
{ intro hq, apply h, exact or.inr hq },
},
{ rintros ⟨np, nq⟩ (p | q),
{ apply np, assumption },
{ apply nq, assumption },
},
end
example : ¬p ¬q → ¬(p ∧ q) :=
begin
rintro (np | nq) ⟨hp, hq⟩,
{ apply np, assumption },
{ apply nq, assumption },
end
example : ¬(p ∧ ¬p) :=
begin
rintro ⟨hp, np⟩,
exact absurd hp np
end
example : p ∧ ¬q → ¬(p → q) :=
begin
rintro ⟨hp, nq⟩ hpq,
apply nq,
exact hpq hp
end
example : ¬p → (p → q) :=
begin
intros np hp,
exact absurd hp np,
end
example : (¬p q) → (p → q) :=
begin
rintros (np | hq) hp,
{ exact absurd hp np },
{ exact hq },
end
example : p false ↔ p :=
begin
split,
{ rintro (hp | hf),
{ exact hp },
{ exact false.elim hf },
},
{ intro hp,
exact or.inl hp,
},
end
example : p ∧ false ↔ false :=
begin
split,
{ rintro ⟨hp, hf⟩, assumption },
{ intro hf, exact false.elim hf },
end
example : (p → q) → (¬q → ¬p) :=
begin
rintro hpq nq hp,
apply nq,
exact absurd (hpq hp) nq,
end
end ex_1_3_1
section ex_1_3_2
open classical
variables p q r s : Prop
example (hp : p) : (p → r s) → ((p → r) (p → s)) :=
begin
intro h,
apply or.elim (h hp),
{ intro hr, exact or.inl (assume hp, hr) },
{ intro hs, exact or.inr (assume hp, hs) }
end
example : ¬(p ∧ q) → ¬p ¬q :=
begin
intro h₁,
apply or.elim (classical.em p),
{ intro hp,
apply or.elim (classical.em q),
{ assume hq, exact false.elim (h₁ ⟨hp, hq⟩) },
{ assume nq, exact or.inr nq },
},
{ intro np,
exact or.inl np,
},
end
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h₁,
split,
{ by_contradiction np, apply h₁, intro hp, exact absurd hp np },
{ intro hq, apply h₁, intro hp, exact hq },
end
example : (p → q) → (¬p q) :=
begin
intro hpq,
apply or.elim (classical.em p),
{ assume hp, exact or.inr (hpq hp) },
{ assume np, exact or.inl np },
end
example : (¬q → ¬p) → (p → q) :=
begin
intros hqp hp,
by_contradiction nq,
exact absurd hp (hqp nq),
end
example : p ¬p :=
by apply classical.em
example : (((p → q) → p) → p) :=
begin
intro h,
apply or.elim (classical.em p),
{ intro hp, assumption },
{ intro np, apply h, intro hp, exact absurd hp np },
end
end ex_1_3_2
section ex_1_3_3
variable p : Prop
example (hp : p) : ¬(p ↔ ¬p) :=
begin
intro h₁,
cases h₁ with h₂,
exact absurd hp (h₂ hp),
end
end ex_1_3_3
section ex_1_4_1
variables (α : Type*) (p q : α → Prop)
example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
begin
split,
{ intro h,
split,
{ intro hx, exact and.left (h hx) },
{ intro hx, exact and.right (h hx) },
},
{ intros h hx,
have hl : ∀ (x : α), p x, from and.left h,
have hr : ∀ (x : α), q x, from and.right h,
exact ⟨hl hx, hr hx⟩
},
end
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
begin
intros h₁ h₂ hx,
exact h₁ hx (h₂ hx)
end
example : (∀ x, p x) (∀ x, q x) → ∀ x, p x q x :=
begin
rintro (h₁ | h₂),
{ intro hx, exact or.inl (h₁ hx) },
{ intro hx, exact or.inr (h₂ hx) },
end
end ex_1_4_1
section ex_1_4_2
variables (α : Type*) (p q : α → Prop)
variable r : Prop
example : α → ((∀ x : α, r) ↔ r) :=
begin
intro hα,
split,
{ intro hαr, apply hαr, exact hα },
{ intros hr hα, exact hr },
end
section
open classical
example : (∀ x, p x r) ↔ (∀ x, p x) r :=
begin
split,
{ intro h₁,
apply or.elim (classical.em r),
{ intro hr, exact or.inr hr },
{ intro nr,
exact or.inl begin
intro hx,
have h₂ : p hx r, from h₁ hx,
apply or.elim h₂,
{ intro hp, exact hp },
{ intro hr, exact absurd hr nr },
end
},
},
{ assume h₁ hx,
apply or.elim h₁,
{ assume h₂, exact or.inl (h₂ hx) },
{ assume hr, exact or.inr hr },
},
end
end
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
begin
split,
{ intros h hr hx, exact h hx hr },
{ intros h hx hr, exact h hr hx },
end
end ex_1_4_2
section ex_1_4_3
open classical
variables (men : Type*) (barber : men)
variable (shaves : men → men → Prop)
example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) :
false :=
begin
apply or.elim (classical.em (shaves barber barber)),
{ intro hb,
apply iff.elim_left (h barber) hb,
exact hb,
},
{ intro nb,
have s, from iff.elim_right (h barber) nb,
exact absurd s nb
},
end
end ex_1_4_3
section ex_1_4_5
open classical
variables (α : Type*) (p q : α → Prop)
variables r s : Prop
example : (∃ x : α, r) → r :=
begin
rintro ⟨hx, hr⟩,
exact hr,
end
example (a : α) : r → (∃ x : α, r) :=
begin
intro hr,
exact ⟨a, hr⟩
end
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{ rintro ⟨hx, ⟨hp, hr⟩⟩, exact ⟨⟨hx, hp⟩, hr⟩ },
{ rintro ⟨⟨hx, hp⟩, hr⟩, exact ⟨hx, ⟨hp, hr⟩⟩ },
end
example : (∃ x, p x q x) ↔ (∃ x, p x) (∃ x, q x) :=
begin
split,
{ rintro ⟨hx, (hp | hq)⟩,
{ exact or.inl ⟨hx, hp⟩ },
{ exact or.inr ⟨hx, hq⟩ },
},
{ rintro (⟨hx, hp⟩ | ⟨hx, hq⟩),
{ exact ⟨hx, or.inl hp⟩ },
{ exact ⟨hx, or.inr hq⟩ },
},
end
example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
begin
split,
{ rintros ha ⟨hx, np⟩, exact absurd (ha hx) np },
{ intros he hx, by_contradiction np, exact he ⟨hx, np⟩ },
end
example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
begin
split,
{ rintro ⟨hx, hp⟩ h, exact absurd hp (h hx) },
{ intro h₁,
by_contradiction h₂,
apply h₁,
intros hx hp,
exact h₂ ⟨hx, hp⟩,
},
end
example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
begin
split,
{ intros h hx hp,
exact h ⟨hx, hp⟩
},
{ rintros h ⟨hx, hp⟩,
exact absurd hp (h hx)
},
end
lemma forall_negation : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
begin
split,
{ intro h₁,
by_contradiction h₂,
exact h₁ (λ (x : α), begin
by_contradiction np,
exact h₂ ⟨x, np⟩
end)
},
{ rintros ⟨hx, np⟩ h, exact absurd (h hx) np },
end
example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := forall_negation α p
example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
begin
split,
{ rintros h ⟨hx, hp⟩, exact h hx hp },
{ intros h hx hp,
exact h ⟨hx, hp⟩
},
end
example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
begin
split,
{ rintros ⟨hx, hp⟩ h, apply hp, exact h hx },
{ intro h₁,
apply or.elim (classical.em (∀ x, p x)),
{ intro h₂, exact ⟨a, (assume hp, h₁ h₂)⟩ },
{ intro h₂,
have h₃ : (∃ x, ¬p x), from iff.elim_left (forall_negation α p) h₂,
exact let ⟨hx, hp⟩ := h₃ in ⟨hx, (assume hp', absurd hp' hp)⟩,
},
},
end
example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
begin
split,
{ rintros ⟨hx, h⟩ hr, exact ⟨hx, h hr⟩ },
{ intro h,
apply or.elim (classical.em r),
{ intro hr,
exact let ⟨hx, hp⟩ := h hr in ⟨hx, (assume hr, hp)⟩
},
{ intro nr, exact ⟨a, (assume hr, absurd hr nr)⟩ },
},
end
end ex_1_4_5
-- Exercise 2
--
-- Use tactic combinators to obtain a one line proof of the following:
section ex_2
example (p q r : Prop) (hp : p) : (p q r) ∧ (q p r) ∧ (q r p) :=
by simp *
end ex_2