Migrate to lean 4.
parent
e18b705ad3
commit
5f8cc89727
|
|
@ -1,43 +1,33 @@
|
|||
/- Exercises 2.10
|
||||
/- Exercises 2
|
||||
-
|
||||
- Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
|
||||
-/
|
||||
|
||||
-- Borrowed from the book.
|
||||
def double (x : ℕ) : ℕ := x + x
|
||||
def do_twice (f : ℕ → ℕ) (x : ℕ) : ℕ := f (f x)
|
||||
|
||||
-- Exercise 1
|
||||
--
|
||||
-- Define the function `Do_Twice`, as described in Section 2.4.
|
||||
section ex_1
|
||||
def Do_Twice (f : (ℕ → ℕ) → (ℕ → ℕ)) (x : ℕ → ℕ)
|
||||
: (ℕ → ℕ) :=
|
||||
f (f x)
|
||||
end ex_1
|
||||
namespace ex1
|
||||
|
||||
def double (x : Nat) := x + x
|
||||
def doTwice (f : Nat → Nat) (x : Nat) : Nat := f (f x)
|
||||
def doTwiceTwice (f : (Nat → Nat) → (Nat → Nat)) (x : Nat → Nat) := f (f x)
|
||||
|
||||
#reduce doTwiceTwice doTwice double 2
|
||||
|
||||
end ex1
|
||||
|
||||
-- Exercise 2
|
||||
--
|
||||
-- Define the functions `curry` and `uncurry`, as described in Section 2.4.
|
||||
section ex_2
|
||||
def curry (α β γ : Type*) (f : α × β → γ)
|
||||
: α → β → γ :=
|
||||
λ α β, f (α, β)
|
||||
namespace ex2
|
||||
|
||||
def uncurry (α β γ : Type*) (f : α → β → γ)
|
||||
: α × β → γ :=
|
||||
λ x, f x.1 x.2
|
||||
end ex_2
|
||||
def curry (f : α × β → γ) : (α → β → γ) :=
|
||||
fun α β => f (α, β)
|
||||
|
||||
-- Borrowed from the book.
|
||||
universe u
|
||||
constant vec : Type u → ℕ → Type u
|
||||
def uncurry (f : α → β → γ) : (α × β → γ) :=
|
||||
fun x => f x.1 x.2
|
||||
|
||||
namespace vec
|
||||
constant empty : Π (α : Type u), vec α 0
|
||||
constant cons : Π (α : Type u) (n : ℕ), α → vec α n → vec α (n + 1)
|
||||
constant append : Π (α : Type u) (n m : ℕ), vec α m → vec α n → vec α (n + m)
|
||||
end vec
|
||||
end ex2
|
||||
|
||||
-- Exercise 3
|
||||
--
|
||||
|
|
@ -48,23 +38,30 @@ end vec
|
|||
-- implicit arguments for parameters that can be inferred. Declare some
|
||||
-- variables and check some expressions involving the constants that you have
|
||||
-- declared.
|
||||
section ex_3
|
||||
namespace ex3
|
||||
|
||||
universe u
|
||||
axiom vec : Type u → Nat → Type u
|
||||
|
||||
namespace vec
|
||||
constant add :
|
||||
Π {α : Type u} {n : ℕ}, vec α n → vec α n → vec α n
|
||||
constant reverse :
|
||||
Π {α : Type u} {n : ℕ}, vec α n → vec α n
|
||||
|
||||
axiom empty : ∀ (α : Type u), vec α 0
|
||||
axiom cons : ∀ (α : Type u) (n : Nat), α → vec α n → vec α (n + 1)
|
||||
axiom append : ∀ (α : Type u) (n m : Nat), vec α m → vec α n → vec α (n + m)
|
||||
axiom add : ∀ {α : Type u} {n : Nat}, vec α n → vec α n → vec α n
|
||||
axiom reverse : ∀ {α : Type u} {n : Nat}, vec α n → vec α n
|
||||
|
||||
end vec
|
||||
|
||||
-- Check results.
|
||||
variables a b : vec Prop 1
|
||||
variables c d : vec Prop 2
|
||||
variable (a b : vec Prop 1)
|
||||
variable (c d : vec Prop 2)
|
||||
|
||||
#check vec.add a b
|
||||
-- #check vec.add a c
|
||||
#check vec.reverse a
|
||||
|
||||
end ex_3
|
||||
end ex3
|
||||
|
||||
-- Exercise 4
|
||||
--
|
||||
|
|
@ -74,23 +71,29 @@ end ex_3
|
|||
-- (using vec) multiplication of a matrix by a vector. Once again, declare some
|
||||
-- variables and check some expressions involving the constants that you have
|
||||
-- declared.
|
||||
constant matrix : Type u → ℕ → ℕ → Type u
|
||||
namespace ex4
|
||||
|
||||
section ex_4
|
||||
universe u
|
||||
axiom matrix : Type u → Nat → Nat → Type u
|
||||
|
||||
namespace matrix
|
||||
constant add : Π {α : Type u} {m n : ℕ}, matrix α m n → matrix α m n → matrix α m n
|
||||
constant mul : Π {α : Type u} {m n p : ℕ}, matrix α m n → matrix α n p → matrix α m p
|
||||
constant app : Π {α : Type u} {m n : ℕ}, matrix α m n → vec α n → vec α m
|
||||
|
||||
axiom add : ∀ {α : Type u} {m n : Nat},
|
||||
matrix α m n → matrix α m n → matrix α m n
|
||||
axiom mul : ∀ {α : Type u} {m n p : Nat},
|
||||
matrix α m n → matrix α n p → matrix α m p
|
||||
axiom app : ∀ {α : Type u} {m n : Nat},
|
||||
matrix α m n → ex3.vec α n → ex3.vec α m
|
||||
|
||||
end matrix
|
||||
|
||||
variables a b : matrix Prop 5 7
|
||||
variable c : matrix Prop 7 3
|
||||
variable d : vec Prop 3
|
||||
variable (a b : matrix Prop 5 7)
|
||||
variable (c : matrix Prop 7 3)
|
||||
variable (d : ex3.vec Prop 3)
|
||||
|
||||
#check matrix.add a b
|
||||
-- #check matrix.add a c
|
||||
#check matrix.mul a c
|
||||
#check matrix.app c d
|
||||
|
||||
end ex_4
|
||||
end ex4
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
/- Exercises 3.7
|
||||
/- Exercises 3
|
||||
-
|
||||
- Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
|
||||
-/
|
||||
|
|
@ -7,189 +7,153 @@
|
|||
--
|
||||
-- Prove the following identities, replacing the "sorry" placeholders with
|
||||
-- actual proofs.
|
||||
section ex_1
|
||||
namespace ex1
|
||||
|
||||
open or
|
||||
|
||||
variables p q r : Prop
|
||||
variable (p q r : Prop)
|
||||
|
||||
-- Commutativity of ∧ and ∨
|
||||
example : p ∧ q ↔ q ∧ p :=
|
||||
iff.intro
|
||||
(assume ⟨p, q⟩, ⟨q, p⟩)
|
||||
(assume ⟨q, p⟩, ⟨p, q⟩)
|
||||
Iff.intro
|
||||
(fun ⟨hp, hq⟩ => show q ∧ p from ⟨hq, hp⟩)
|
||||
(fun ⟨hq, hp⟩ => show p ∧ q from ⟨hp, hq⟩)
|
||||
|
||||
example : p ∨ q ↔ q ∨ p :=
|
||||
iff.intro
|
||||
(assume h, h.elim
|
||||
(assume hp : p, inr hp)
|
||||
(assume hq : q, inl hq))
|
||||
(assume h, h.elim
|
||||
(assume hq : q, inr hq)
|
||||
(assume hp : p, inl hp))
|
||||
Iff.intro
|
||||
(fun h => h.elim Or.inr Or.inl)
|
||||
(fun h => h.elim Or.inr Or.inl)
|
||||
|
||||
-- Associativity of ∧ and ∨
|
||||
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
|
||||
iff.intro
|
||||
(assume ⟨⟨p, q⟩, r⟩, ⟨p, q, r⟩)
|
||||
(assume ⟨p, q, r⟩, ⟨⟨p, q⟩, r⟩)
|
||||
Iff.intro
|
||||
(fun ⟨⟨hp, hq⟩, hr⟩ => ⟨hp, hq, hr⟩)
|
||||
(fun ⟨hp, hq, hr⟩ => ⟨⟨hp, hq⟩, hr⟩)
|
||||
|
||||
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
|
||||
iff.intro
|
||||
(assume h₁, h₁.elim
|
||||
(assume h₂, h₂.elim (assume p, inl p) (assume q, inr (inl q)))
|
||||
(assume r, inr (inr r)))
|
||||
(assume h₁, h₁.elim
|
||||
(assume p, inl (inl p))
|
||||
(assume h₂, h₂.elim (assume q, inl (inr q)) (assume r, inr r)))
|
||||
Iff.intro
|
||||
(fun h₁ => h₁.elim
|
||||
(fun h₂ => h₂.elim Or.inl (Or.inr ∘ Or.inl))
|
||||
(Or.inr ∘ Or.inr))
|
||||
(fun h₁ => h₁.elim
|
||||
(Or.inl ∘ Or.inl)
|
||||
(fun h₂ => h₂.elim (Or.inl ∘ Or.inr) Or.inr))
|
||||
|
||||
-- Distributivity
|
||||
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
|
||||
iff.intro
|
||||
(assume ⟨hp, hqr⟩, hqr.elim
|
||||
(assume hq, inl ⟨hp, hq⟩)
|
||||
(assume hr, inr ⟨hp, hr⟩))
|
||||
(assume h₁, h₁.elim
|
||||
(assume ⟨hp, hq⟩, ⟨hp, inl hq⟩)
|
||||
(assume ⟨hp, hr⟩, ⟨hp, inr hr⟩))
|
||||
Iff.intro
|
||||
(fun ⟨hp, hqr⟩ => hqr.elim (Or.inl ⟨hp, ·⟩) (Or.inr ⟨hp, ·⟩))
|
||||
(fun h₁ => h₁.elim
|
||||
(fun ⟨hp, hq⟩ => ⟨hp, Or.inl hq⟩)
|
||||
(fun ⟨hp, hr⟩ => ⟨hp, Or.inr hr⟩))
|
||||
|
||||
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
|
||||
iff.intro
|
||||
(assume h, h.elim
|
||||
(assume hp, ⟨inl hp, inl hp⟩)
|
||||
(assume ⟨hq, hr⟩, ⟨inr hq, inr hr⟩))
|
||||
(assume ⟨h₁, h₂⟩, h₁.elim
|
||||
(assume hp, inl hp)
|
||||
(assume hq, h₂.elim (assume hp, inl hp) (assume hr, inr ⟨hq, hr⟩)))
|
||||
Iff.intro
|
||||
(fun h => h.elim
|
||||
(fun hp => ⟨Or.inl hp, Or.inl hp⟩)
|
||||
(fun ⟨hq, hr⟩ => ⟨Or.inr hq, Or.inr hr⟩))
|
||||
(fun ⟨h₁, h₂⟩ => h₁.elim
|
||||
Or.inl
|
||||
(fun hq => h₂.elim Or.inl (fun hr => Or.inr ⟨hq, hr⟩)))
|
||||
|
||||
-- Other properties
|
||||
example : (p → (q → r)) ↔ (p ∧ q → r) :=
|
||||
iff.intro
|
||||
(assume h ⟨hp, hq⟩, h hp hq)
|
||||
(assume h hp hq, h ⟨hp, hq⟩)
|
||||
Iff.intro
|
||||
(fun h ⟨hp, hq⟩ => h hp hq)
|
||||
(fun h hp hq => h ⟨hp, hq⟩)
|
||||
|
||||
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
|
||||
iff.intro
|
||||
(assume h,
|
||||
have h₁ : p → r, from (assume hp, h (or.inl hp)),
|
||||
have h₂ : q → r, from (assume hq, h (or.inr hq)),
|
||||
⟨h₁, h₂⟩)
|
||||
(assume ⟨hpr, hqr⟩, assume hpq, hpq.elim hpr hqr)
|
||||
Iff.intro
|
||||
(fun h =>
|
||||
have h₁ : p → r := h ∘ Or.inl
|
||||
have h₂ : q → r := h ∘ Or.inr
|
||||
show (p → r) ∧ (q → r) from ⟨h₁, h₂⟩)
|
||||
(fun ⟨h₁, h₂⟩ h => h.elim h₁ h₂)
|
||||
|
||||
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
|
||||
iff.intro
|
||||
(assume h, and.intro
|
||||
(assume hp, h (inl hp))
|
||||
(assume hq, h (inr hq)))
|
||||
(assume h₁ h₂, h₂.elim
|
||||
(assume hp, have np : ¬p, from h₁.left, absurd hp np)
|
||||
(assume hq, have nq : ¬q, from h₁.right, absurd hq nq))
|
||||
Iff.intro
|
||||
(fun h => ⟨h ∘ Or.inl, h ∘ Or.inr⟩)
|
||||
(fun h₁ h₂ => h₂.elim (absurd · h₁.left) (absurd · h₁.right))
|
||||
|
||||
example : ¬p ∨ ¬q → ¬(p ∧ q) :=
|
||||
assume h₁ h₂,
|
||||
h₁.elim
|
||||
(assume np : ¬p, have hp : p, from h₂.left, absurd hp np)
|
||||
(assume nq : ¬q, have hq : q, from h₂.right, absurd hq nq)
|
||||
fun h₁ h₂ => h₁.elim (absurd h₂.left ·) (absurd h₂.right ·)
|
||||
|
||||
example : ¬(p ∧ ¬p) :=
|
||||
assume h,
|
||||
have hp : p, from h.left,
|
||||
have np : ¬p, from h.right,
|
||||
absurd hp np
|
||||
fun h => absurd h.left h.right
|
||||
|
||||
example : p ∧ ¬q → ¬(p → q) :=
|
||||
assume ⟨hp, nq⟩ hpq,
|
||||
absurd (hpq hp) nq
|
||||
fun ⟨hp, nq⟩ hpq => absurd (hpq hp) nq
|
||||
|
||||
example : ¬p → (p → q) :=
|
||||
assume np hp,
|
||||
absurd hp np
|
||||
fun np hp => absurd hp np
|
||||
|
||||
example : (¬p ∨ q) → (p → q) :=
|
||||
assume npq hp,
|
||||
npq.elim
|
||||
(assume np, absurd hp np)
|
||||
(assume hq, hq)
|
||||
fun npq hp => npq.elim (absurd hp ·) id
|
||||
|
||||
example : p ∨ false ↔ p :=
|
||||
iff.intro
|
||||
(assume hpf, hpf.elim
|
||||
(assume hp, hp)
|
||||
(assume hf, false.elim hf))
|
||||
(assume hp, inl hp)
|
||||
example : p ∨ False ↔ p :=
|
||||
Iff.intro (fun hpf => hpf.elim id False.elim) Or.inl
|
||||
|
||||
example : p ∧ false ↔ false :=
|
||||
iff.intro
|
||||
(assume ⟨hp, hf⟩, hf)
|
||||
(assume hf, false.elim hf)
|
||||
example : p ∧ False ↔ False :=
|
||||
Iff.intro (fun ⟨_, hf⟩ => hf) False.elim
|
||||
|
||||
example : (p → q) → (¬q → ¬p) :=
|
||||
assume hpq nq hp,
|
||||
absurd (hpq hp) nq
|
||||
fun hpq nq hp => absurd (hpq hp) nq
|
||||
|
||||
end ex_1
|
||||
end ex1
|
||||
|
||||
-- Example 2
|
||||
--
|
||||
-- Prove the following identities, replacing the “sorry” placeholders with
|
||||
-- actual proofs. These require classical reasoning.
|
||||
section ex_2
|
||||
namespace ex2
|
||||
|
||||
open classical
|
||||
open Classical
|
||||
|
||||
variables p q r s : Prop
|
||||
variable (p q r s : Prop)
|
||||
|
||||
example (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
|
||||
assume h₁,
|
||||
or.elim (h₁ hp)
|
||||
(assume hr, or.inl (assume hp, hr))
|
||||
(assume hs, or.inr (assume hp, hs))
|
||||
fun h => (h hp).elim
|
||||
(fun hr => Or.inl (fun _ => hr))
|
||||
(fun hs => Or.inr (fun _ => hs))
|
||||
|
||||
example : ¬(p ∧ q) → ¬p ∨ ¬q :=
|
||||
assume npq,
|
||||
or.elim (em p)
|
||||
(assume hp, or.elim (em q)
|
||||
(assume hq, false.elim (npq ⟨hp, hq⟩))
|
||||
(assume nq, or.inr nq))
|
||||
(assume np, or.inl np)
|
||||
fun npq => (em p).elim
|
||||
(fun hp => (em q).elim
|
||||
(fun hq => False.elim (npq ⟨hp, hq⟩))
|
||||
Or.inr)
|
||||
Or.inl
|
||||
|
||||
example : ¬(p → q) → p ∧ ¬q :=
|
||||
assume h₁,
|
||||
and.intro
|
||||
(by_contradiction (
|
||||
assume np,
|
||||
h₁ (λ (hp : p), absurd hp np)
|
||||
))
|
||||
(assume hq, h₁ (λ (hp : p), hq))
|
||||
fun h =>
|
||||
have lhs : p := byContradiction
|
||||
fun np => h (fun (hp : p) => absurd hp np)
|
||||
⟨lhs, fun hq => h (fun _ => hq)⟩
|
||||
|
||||
example : (p → q) → (¬p ∨ q) :=
|
||||
assume hpq,
|
||||
or.elim (em p)
|
||||
(assume hp, or.inr (hpq hp))
|
||||
(assume np, or.inl np)
|
||||
fun hpq => (em p).elim (fun hp => Or.inr (hpq hp)) Or.inl
|
||||
|
||||
example : (¬q → ¬p) → (p → q) :=
|
||||
assume h₁ hp,
|
||||
by_contradiction (assume nq, absurd hp (h₁ nq))
|
||||
fun h hp => byContradiction
|
||||
fun nq => absurd hp (h nq)
|
||||
|
||||
example : p ∨ ¬p := em p
|
||||
|
||||
example : (((p → q) → p) → p) :=
|
||||
assume h₁,
|
||||
by_contradiction (
|
||||
assume np,
|
||||
suffices hp : p, from absurd hp np,
|
||||
h₁ (λ (hp : p), absurd hp np)
|
||||
)
|
||||
fun h => byContradiction
|
||||
fun np =>
|
||||
suffices hp : p from absurd hp np
|
||||
h (fun (hp : p) => absurd hp np)
|
||||
|
||||
end ex_2
|
||||
end ex2
|
||||
|
||||
-- Example 3
|
||||
--
|
||||
-- Prove `¬(p ↔ ¬p)` without using classical logic.
|
||||
section ex_3
|
||||
namespace ex3
|
||||
|
||||
variable p : Prop
|
||||
variable (p : Prop)
|
||||
|
||||
example (hp : p) : ¬(p ↔ ¬p) :=
|
||||
assume h,
|
||||
absurd hp (iff.elim_left h (hp))
|
||||
fun h => absurd hp (Iff.mp h hp)
|
||||
|
||||
end ex_3
|
||||
end ex3
|
||||
|
|
|
|||
|
|
@ -1,102 +1,94 @@
|
|||
/- Exercises 4.6
|
||||
/- Exercises 4
|
||||
-
|
||||
- Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
|
||||
-/
|
||||
import data.int.basic
|
||||
import data.nat.basic
|
||||
import data.real.basic
|
||||
|
||||
-- Exercise 1
|
||||
--
|
||||
-- Prove these equivalences. You should also try to understand why the reverse
|
||||
-- implication is not derivable in the last example.
|
||||
section ex_1
|
||||
namespace ex1
|
||||
|
||||
variables (α : Type*) (p q : α → Prop)
|
||||
variable (α : Type _)
|
||||
variable (p q : α → Prop)
|
||||
|
||||
example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
|
||||
iff.intro
|
||||
( assume h,
|
||||
and.intro
|
||||
(assume x, and.left (h x))
|
||||
(assume x, and.right (h x)))
|
||||
(assume ⟨h₁, h₂⟩ x, ⟨h₁ x, h₂ 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⟩)
|
||||
|
||||
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
|
||||
assume h₁ h₂ x,
|
||||
have px : p x, from h₂ x,
|
||||
h₁ x px
|
||||
fun h₁ h₂ x =>
|
||||
have px : p x := h₂ x
|
||||
h₁ x px
|
||||
|
||||
example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
|
||||
assume h₁ x,
|
||||
h₁.elim
|
||||
(assume h₂, or.inl (h₂ x))
|
||||
(assume h₂, or.inr (h₂ 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 ex_1
|
||||
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).
|
||||
section ex_2
|
||||
namespace ex2
|
||||
|
||||
variables (α : Type*) (p q : α → Prop)
|
||||
variable r : Prop
|
||||
variable (α : Type _)
|
||||
variable (p q : α → Prop)
|
||||
variable (r : Prop)
|
||||
|
||||
example : α → ((∀ x : α, r) ↔ r) :=
|
||||
assume ha,
|
||||
iff.intro (assume h, h ha) (assume hr ha, hr)
|
||||
example : α → ((∀ _ : α, r) ↔ r) :=
|
||||
fun a => Iff.intro (fun h => h a) (fun hr _ => hr)
|
||||
|
||||
-- Ensure we do not use classical logic in the first or third subproblems.
|
||||
section
|
||||
|
||||
open classical
|
||||
open Classical
|
||||
|
||||
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
|
||||
iff.intro
|
||||
(assume h₁, or.elim (classical.em r)
|
||||
(assume hr, or.inr hr)
|
||||
(assume nr, or.inl (λ (x : α), or.elim (h₁ x)
|
||||
(assume hp, hp)
|
||||
(assume hr, absurd hr nr))))
|
||||
(assume h₁, or.elim h₁
|
||||
(assume h₂, (λ (x : α), or.inl (h₂ x)))
|
||||
(assume hr, (λ (x : α), or.inr hr)))
|
||||
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
|
||||
|
||||
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
|
||||
iff.intro
|
||||
(assume h₁ hr hx, h₁ hx hr)
|
||||
(assume h₁ hx hr, h₁ hr hx)
|
||||
Iff.intro
|
||||
(fun h hr hx => h hx hr)
|
||||
(fun h hx hr => h hr hx)
|
||||
|
||||
end ex_2
|
||||
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.
|
||||
section ex_3
|
||||
namespace ex3
|
||||
|
||||
open classical
|
||||
open Classical
|
||||
|
||||
variables (men : Type*) (barber : men)
|
||||
variable (men : Type _)
|
||||
variable (barber : men)
|
||||
variable (shaves : men → men → Prop)
|
||||
|
||||
example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) :
|
||||
false :=
|
||||
have b : shaves barber barber ↔ ¬ shaves barber barber, from h barber,
|
||||
or.elim (classical.em (shaves barber barber))
|
||||
(assume b', absurd b' (iff.elim_left b b'))
|
||||
(assume b', absurd (iff.elim_right b b') b')
|
||||
example (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 ex_3
|
||||
end ex3
|
||||
|
||||
-- Exercise 4
|
||||
--
|
||||
|
|
@ -108,162 +100,141 @@ end ex_3
|
|||
-- 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.
|
||||
section ex_4
|
||||
namespace ex4
|
||||
|
||||
def prime (n : ℕ) : Prop :=
|
||||
n > 1 ∧ ∀ (m : ℕ), (1 < m ∧ m < n) → n % m ≠ 0
|
||||
def even (a : Nat) := ∃ b, a = 2 * b
|
||||
|
||||
def infinitely_many_primes : Prop :=
|
||||
∀ (n : ℕ), (∃ (m : ℕ), m > n ∧ prime m)
|
||||
def odd (a : Nat) := ¬even a
|
||||
|
||||
def Fermat_prime (n : ℕ) : Prop :=
|
||||
∃ (m : ℕ), n = 2^(2^m) + 1
|
||||
def prime (n : Nat) : Prop :=
|
||||
n > 1 ∧ ∀ (m : Nat), (1 < m ∧ m < n) → n % m ≠ 0
|
||||
|
||||
def infinitely_many_Fermat_primes : Prop :=
|
||||
∀ (n : ℕ), (∃ (m : ℕ), m > n ∧ Fermat_prime m)
|
||||
def infinitelyManyPrimes : Prop :=
|
||||
∀ (n : Nat), (∃ (m : Nat), m > n ∧ prime m)
|
||||
|
||||
def goldbach_conjecture : Prop :=
|
||||
∀ (n : ℕ), even n ∧ n > 2 → (∃ (x y : ℕ), prime x ∧ prime y ∧ x + y = n)
|
||||
def FermatPrime (n : Nat) : Prop :=
|
||||
∃ (m : Nat), n = 2^(2^m) + 1
|
||||
|
||||
def Goldbach's_weak_conjecture : Prop :=
|
||||
∀ (n : ℕ), odd n ∧ n > 5 → (∃ (x y z : ℕ), prime x ∧ prime y ∧ prime z ∧ x + y + z = n)
|
||||
def infinitelyManyFermatPrimes : Prop :=
|
||||
∀ (n : Nat), (∃ (m : Nat), m > n ∧ FermatPrime m)
|
||||
|
||||
def Fermat's_last_theorem : Prop :=
|
||||
∀ (n : ℕ), n > 2 → (∀ (a b c : ℕ), a^n + b^n ≠ c^n)
|
||||
def GoldbachConjecture : Prop :=
|
||||
∀ (n : Nat), even n ∧ n > 2 →
|
||||
∃ (x y : Nat), prime x ∧ prime y ∧ x + y = n
|
||||
|
||||
end ex_4
|
||||
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.
|
||||
section ex_5
|
||||
namespace ex5
|
||||
|
||||
open classical
|
||||
open Classical
|
||||
|
||||
variables (α : Type*) (p q : α → Prop)
|
||||
variables r s : Prop
|
||||
variable (α : Type _)
|
||||
variable (p q : α → Prop)
|
||||
variable (r s : Prop)
|
||||
|
||||
example : (∃ x : α, r) → r :=
|
||||
assume ⟨hx, hr⟩,
|
||||
hr
|
||||
example : (∃ _ : α, r) → r :=
|
||||
fun ⟨_, hr⟩ => hr
|
||||
|
||||
example (a : α) : r → (∃ x : α, r) :=
|
||||
assume hr,
|
||||
⟨a, hr⟩
|
||||
example (a : α) : r → (∃ _ : α, r) :=
|
||||
fun hr => ⟨a, hr⟩
|
||||
|
||||
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
|
||||
iff.intro
|
||||
(assume ⟨hx, ⟨hp, hr⟩⟩, ⟨⟨hx, hp⟩, hr⟩)
|
||||
(assume ⟨⟨hx, hp⟩, hr⟩, ⟨hx, ⟨hp, hr⟩⟩)
|
||||
Iff.intro
|
||||
(fun ⟨hx, ⟨hp, hr⟩⟩ => ⟨⟨hx, hp⟩, hr⟩)
|
||||
(fun ⟨⟨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 (⟨hx, hp⟩))
|
||||
(assume hq, or.inr (⟨hx, hq⟩)))
|
||||
(assume h, h.elim
|
||||
(assume ⟨hx, hp⟩, ⟨hx, or.inl hp⟩)
|
||||
(assume ⟨hx, hq⟩, ⟨hx, or.inr hq⟩))
|
||||
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⟩))
|
||||
|
||||
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 ⟨hx, np⟩))
|
||||
example : (∀ x, p x) ↔ ¬(∃ x, ¬p x) :=
|
||||
Iff.intro
|
||||
(fun h ⟨hx, np⟩ => np (h hx))
|
||||
(fun h hx => byContradiction
|
||||
fun 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' ⟨x, hp⟩)
|
||||
))
|
||||
example : (∃ 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⟩))
|
||||
|
||||
example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
|
||||
iff.intro
|
||||
(assume h hx hp, h ⟨hx, hp⟩)
|
||||
(assume h ⟨hx, hp⟩, absurd hp (h hx))
|
||||
example : (¬∃ x, p x) ↔ (∀ x, ¬p x) :=
|
||||
Iff.intro
|
||||
(fun h hx hp => h ⟨hx, hp⟩)
|
||||
(fun h ⟨hx, hp⟩ => absurd hp (h hx))
|
||||
|
||||
lemma forall_negation : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
|
||||
iff.intro
|
||||
(assume h, classical.by_contradiction (
|
||||
assume h',
|
||||
h (λ (x : α), classical.by_contradiction (
|
||||
assume np,
|
||||
h' ⟨x, np⟩
|
||||
))
|
||||
))
|
||||
(assume ⟨hx, np⟩ h, absurd (h hx) np)
|
||||
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)
|
||||
|
||||
example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
|
||||
example : (¬∀ x, p x) ↔ (∃ x, ¬p x) :=
|
||||
forall_negation α p
|
||||
|
||||
example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
|
||||
iff.intro
|
||||
(assume h ⟨hx, hp⟩, h hx hp)
|
||||
(assume h hx hp, h ⟨hx, hp⟩)
|
||||
Iff.intro
|
||||
(fun h ⟨hx, hp⟩ => h hx hp)
|
||||
(fun h hx hp => h ⟨hx, hp⟩)
|
||||
|
||||
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₂, ⟨a, assume hp, h₁ h₂⟩)
|
||||
(assume h₂,
|
||||
have h₃ : (∃ x, ¬p x), from iff.elim_left (forall_negation α p) h₂,
|
||||
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, (assume hp', absurd hp' hp)⟩
|
||||
end))
|
||||
| ⟨hx, hp⟩ => ⟨hx, fun hp' => absurd hp' hp⟩))
|
||||
|
||||
example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
|
||||
iff.intro
|
||||
(assume ⟨hx, hrp⟩ hr, ⟨hx, hrp hr⟩)
|
||||
(assume h, or.elim (classical.em r)
|
||||
(assume hr, match h hr with
|
||||
⟨hx, hp⟩ := ⟨hx, (assume hr, hp)⟩
|
||||
end)
|
||||
(assume nr, ⟨a, (assume hr, absurd hr nr)⟩))
|
||||
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 ex_5
|
||||
end ex5
|
||||
|
||||
-- Exercise 6
|
||||
--
|
||||
-- Give a calculational proof of the theorem `log_mul` below.
|
||||
section ex_6
|
||||
namespace ex6
|
||||
|
||||
variables log exp : real → real
|
||||
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
|
||||
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)
|
||||
|
||||
-- this ensures the assumptions are available in tactic proofs
|
||||
include log_exp_eq exp_log_eq exp_pos exp_add
|
||||
example (x y z : Float) : exp (x + y + z) = exp x * exp y * exp z :=
|
||||
by rw [exp_add, exp_add]
|
||||
|
||||
example (x y z : real) :
|
||||
exp (x + y + z) = exp x * exp y * exp z :=
|
||||
by rw [exp_add, exp_add]
|
||||
example (y : Float) (h : y > 0) : exp (log y) = y := exp_log_eq h
|
||||
|
||||
example (y : real) (h : y > 0) : exp (log y) = y :=
|
||||
exp_log_eq h
|
||||
|
||||
theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) :
|
||||
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
|
||||
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 ex_6
|
||||
|
||||
-- Exercise 7
|
||||
--
|
||||
-- Prove the theorem below, using only the ring properties of ℤ enumerated in
|
||||
-- Section 4.2 and the theorem `sub_self.`
|
||||
section ex_7
|
||||
#check sub_self
|
||||
|
||||
example (x : ℤ) : x * 0 = 0 :=
|
||||
calc x * 0 = x * (x - x) : by rw (sub_self x)
|
||||
... = x * x - x * x : by rw (mul_sub x x x)
|
||||
... = 0 : by rw (sub_self (x * x))
|
||||
|
||||
end ex_7
|
||||
end ex6
|
||||
|
|
|
|||
|
|
@ -1,499 +1,453 @@
|
|||
/- Exercises 5.8
|
||||
/- Exercises 5
|
||||
-
|
||||
- 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
|
||||
namespace ex1
|
||||
|
||||
variables p q r : Prop
|
||||
-- Exercises 3.1
|
||||
|
||||
section ex3_1
|
||||
|
||||
variable (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 := by
|
||||
apply Iff.intro
|
||||
· intro ⟨hp, hq⟩
|
||||
exact ⟨hq, hp⟩
|
||||
· intro ⟨hq, hp⟩
|
||||
exact ⟨hp, hq⟩
|
||||
|
||||
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
|
||||
example : p ∨ q ↔ q ∨ p := by
|
||||
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
|
||||
|
||||
-- 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) := by
|
||||
apply Iff.intro
|
||||
· intro ⟨⟨hp, hq⟩, hr⟩
|
||||
exact ⟨hp, hq, hr⟩
|
||||
· intro ⟨hp, hq, hr⟩
|
||||
exact ⟨⟨hp, hq⟩, hr⟩
|
||||
|
||||
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
|
||||
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
|
||||
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
|
||||
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) := by
|
||||
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⟩
|
||||
|
||||
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
|
||||
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by
|
||||
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
|
||||
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 ∧ q → r) := by
|
||||
apply Iff.intro
|
||||
· intro h ⟨hp, hq⟩
|
||||
exact h hp hq
|
||||
· intro h hp hq
|
||||
exact h ⟨hp, hq⟩
|
||||
|
||||
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) → r) ↔ (p → r) ∧ (q → r) := by
|
||||
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
|
||||
|
||||
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 := by
|
||||
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
|
||||
|
||||
example : ¬p ∨ ¬q → ¬(p ∧ q) :=
|
||||
begin
|
||||
rintro (np | nq) ⟨hp, hq⟩,
|
||||
{ apply np, assumption },
|
||||
{ apply nq, assumption },
|
||||
end
|
||||
example : ¬p ∨ ¬q → ¬(p ∧ q) := by
|
||||
intro
|
||||
| Or.inl np => intro h; exact absurd h.left np
|
||||
| Or.inr nq => intro h; exact absurd h.right nq
|
||||
|
||||
example : ¬(p ∧ ¬p) :=
|
||||
begin
|
||||
rintro ⟨hp, np⟩,
|
||||
example : ¬(p ∧ ¬p) := by
|
||||
intro ⟨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 ∧ ¬q → ¬(p → q) := by
|
||||
intro ⟨hp, nq⟩ h
|
||||
exact absurd (h hp) nq
|
||||
|
||||
example : ¬p → (p → q) :=
|
||||
begin
|
||||
intros np hp,
|
||||
exact absurd hp np,
|
||||
end
|
||||
example : ¬p → (p → q) := by
|
||||
intro np hp
|
||||
exact absurd hp np
|
||||
|
||||
example : (¬p ∨ q) → (p → q) :=
|
||||
begin
|
||||
rintros (np | hq) hp,
|
||||
{ exact absurd hp np },
|
||||
{ exact hq },
|
||||
end
|
||||
example : (¬p ∨ q) → (p → q) := by
|
||||
intro
|
||||
| Or.inl np => intro hp; exact absurd hp np
|
||||
| Or.inr hq => exact fun _ => hq
|
||||
|
||||
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 ↔ p := by
|
||||
apply Iff.intro
|
||||
· intro
|
||||
| Or.inl hp => exact hp
|
||||
| Or.inr ff => exact False.elim ff
|
||||
· intro hp
|
||||
exact Or.inl hp
|
||||
|
||||
example : p ∧ false ↔ false :=
|
||||
begin
|
||||
split,
|
||||
{ rintro ⟨hp, hf⟩, assumption },
|
||||
{ intro hf, exact false.elim hf },
|
||||
end
|
||||
example : p ∧ False ↔ False := by
|
||||
apply Iff.intro
|
||||
· intro ⟨_, ff⟩
|
||||
exact ff
|
||||
· intro ff
|
||||
exact False.elim ff
|
||||
|
||||
example : (p → q) → (¬q → ¬p) :=
|
||||
begin
|
||||
rintro hpq nq hp,
|
||||
apply nq,
|
||||
exact absurd (hpq hp) nq,
|
||||
end
|
||||
example : (p → q) → (¬q → ¬p) := by
|
||||
intro hpq nq hp
|
||||
exact absurd (hpq hp) nq
|
||||
|
||||
end ex_1_3_1
|
||||
end ex3_1
|
||||
|
||||
section ex_1_3_2
|
||||
-- Exercises 3.2
|
||||
|
||||
open classical
|
||||
section ex3_2
|
||||
|
||||
variables p q r s : Prop
|
||||
open Classical
|
||||
|
||||
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
|
||||
variable (p q r s : Prop)
|
||||
|
||||
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 (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) := by
|
||||
intro h
|
||||
apply (h hp).elim
|
||||
· intro hr
|
||||
exact Or.inl (fun _ => hr)
|
||||
· intro hs
|
||||
exact Or.inr (fun _ => hs)
|
||||
|
||||
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 := by
|
||||
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
|
||||
|
||||
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 : ¬(p → q) → p ∧ ¬q := by
|
||||
intro h
|
||||
apply And.intro
|
||||
· apply byContradiction
|
||||
intro np
|
||||
apply h
|
||||
intro hp
|
||||
exact absurd hp np
|
||||
· intro hq
|
||||
apply h
|
||||
intro _
|
||||
exact hq
|
||||
|
||||
example : (¬q → ¬p) → (p → q) :=
|
||||
begin
|
||||
intros hqp hp,
|
||||
by_contradiction nq,
|
||||
exact absurd hp (hqp nq),
|
||||
end
|
||||
example : (p → q) → (¬p ∨ q) := by
|
||||
intro hpq
|
||||
apply (em p).elim
|
||||
· intro hp
|
||||
exact Or.inr (hpq hp)
|
||||
· intro np
|
||||
exact Or.inl np
|
||||
|
||||
example : p ∨ ¬p :=
|
||||
by apply classical.em
|
||||
example : (¬q → ¬p) → (p → q) := by
|
||||
intro hqp hp
|
||||
apply byContradiction
|
||||
intro nq
|
||||
exact absurd hp (hqp nq)
|
||||
|
||||
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
|
||||
example : p ∨ ¬p := by apply em
|
||||
|
||||
end ex_1_3_2
|
||||
example : (((p → q) → p) → p) := by
|
||||
intro h
|
||||
apply (em p).elim
|
||||
· intro hp
|
||||
exact hp
|
||||
· intro np
|
||||
apply h
|
||||
intro hp
|
||||
exact absurd hp np
|
||||
|
||||
section ex_1_3_3
|
||||
end ex3_2
|
||||
|
||||
variable p : Prop
|
||||
-- Exercises 3.3
|
||||
|
||||
example (hp : p) : ¬(p ↔ ¬p) :=
|
||||
begin
|
||||
intro h₁,
|
||||
cases h₁ with h₂,
|
||||
exact absurd hp (h₂ hp),
|
||||
end
|
||||
section ex3_3
|
||||
|
||||
end ex_1_3_3
|
||||
variable (p : Prop)
|
||||
|
||||
section ex_1_4_1
|
||||
example (hp : p) : ¬(p ↔ ¬p) := by
|
||||
intro h
|
||||
exact absurd hp (h.mp hp)
|
||||
|
||||
variables (α : Type*) (p q : α → Prop)
|
||||
end ex3_3
|
||||
|
||||
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
|
||||
-- Exercises 4.1
|
||||
|
||||
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
|
||||
begin
|
||||
intros h₁ h₂ hx,
|
||||
section ex4_1
|
||||
|
||||
variable (α : Type _)
|
||||
variable (p q : α → Prop)
|
||||
|
||||
example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := by
|
||||
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⟩
|
||||
|
||||
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) := by
|
||||
intro 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
|
||||
example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := by
|
||||
intro
|
||||
| Or.inl h => intro hx; exact Or.inl (h hx)
|
||||
| Or.inr h => intro hx; exact Or.inr (h hx)
|
||||
|
||||
end ex_1_4_1
|
||||
end ex4_1
|
||||
|
||||
section ex_1_4_2
|
||||
-- Exercises 4.2
|
||||
|
||||
variables (α : Type*) (p q : α → Prop)
|
||||
variable r : Prop
|
||||
section ex4_2
|
||||
|
||||
example : α → ((∀ x : α, r) ↔ r) :=
|
||||
begin
|
||||
intro hα,
|
||||
split,
|
||||
{ intro hαr, apply hαr, exact hα },
|
||||
{ intros hr hα, exact hr },
|
||||
end
|
||||
variable (α : Type _)
|
||||
variable (p q : α → Prop)
|
||||
variable (r : Prop)
|
||||
|
||||
example : α → ((∀ _ : α, r) ↔ r) := by
|
||||
intro ha
|
||||
apply Iff.intro
|
||||
· intro har
|
||||
apply har
|
||||
exact ha
|
||||
· intro hr _
|
||||
exact hr
|
||||
|
||||
section
|
||||
|
||||
open classical
|
||||
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
|
||||
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := by
|
||||
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
|
||||
|
||||
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
|
||||
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := by
|
||||
apply Iff.intro
|
||||
· intro h hr hx
|
||||
exact h hx hr
|
||||
· intro h hx hr
|
||||
exact h hr hx
|
||||
|
||||
end ex_1_4_2
|
||||
end ex4_2
|
||||
|
||||
section ex_1_4_3
|
||||
-- Exercises 4.3
|
||||
|
||||
open classical
|
||||
section ex4_3
|
||||
|
||||
variables (men : Type*) (barber : men)
|
||||
open Classical
|
||||
|
||||
variable (men : Type _)
|
||||
variable (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
|
||||
example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := by
|
||||
apply (em (shaves barber barber)).elim
|
||||
· intro hb
|
||||
exact absurd hb ((h barber).mp hb)
|
||||
· intro nb
|
||||
exact absurd ((h barber).mpr nb) nb
|
||||
|
||||
end ex_1_4_3
|
||||
end ex4_3
|
||||
|
||||
section ex_1_4_5
|
||||
-- Exercises 4.5
|
||||
|
||||
open classical
|
||||
section ex4_5
|
||||
|
||||
variables (α : Type*) (p q : α → Prop)
|
||||
variables r s : Prop
|
||||
open Classical
|
||||
|
||||
example : (∃ x : α, r) → r :=
|
||||
begin
|
||||
rintro ⟨hx, hr⟩,
|
||||
exact hr,
|
||||
end
|
||||
variable (α : Type _)
|
||||
variable (p q : α → Prop)
|
||||
variable (r s : Prop)
|
||||
|
||||
example (a : α) : r → (∃ x : α, r) :=
|
||||
begin
|
||||
intro hr,
|
||||
example : (∃ _ : α, r) → r := by
|
||||
intro ⟨_, hr⟩
|
||||
exact hr
|
||||
|
||||
example (a : α) : r → (∃ _ : α, r) := by
|
||||
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 ∧ r) ↔ (∃ x, p x) ∧ r := by
|
||||
apply Iff.intro
|
||||
· intro ⟨hx, hp, hr⟩
|
||||
exact ⟨⟨hx, hp⟩, hr⟩
|
||||
· intro ⟨⟨hx, hp⟩, hr⟩
|
||||
exact ⟨hx, hp, hr⟩
|
||||
|
||||
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 ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) := by
|
||||
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⟩
|
||||
|
||||
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) := by
|
||||
apply Iff.intro
|
||||
· intro ha ⟨hx, np⟩
|
||||
exact absurd (ha hx) np
|
||||
· intro he hx
|
||||
apply byContradiction
|
||||
intro np
|
||||
exact he ⟨hx, np⟩
|
||||
|
||||
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⟩,
|
||||
example : (∃ x, p x) ↔ ¬(∀ x, ¬p x) := by
|
||||
apply Iff.intro
|
||||
· intro ⟨hx, hp⟩ h
|
||||
exact absurd hp (h hx)
|
||||
},
|
||||
end
|
||||
· intro h₁
|
||||
apply byContradiction
|
||||
intro h₂
|
||||
apply h₁
|
||||
intro hx hp
|
||||
exact h₂ ⟨hx, hp⟩
|
||||
|
||||
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,
|
||||
example : (¬∃ x, p x) ↔ (∀ x, ¬p x) := by
|
||||
apply Iff.intro
|
||||
· intro h hx hp
|
||||
exact h ⟨hx, hp⟩
|
||||
},
|
||||
end
|
||||
· intro h ⟨hx, hp⟩
|
||||
exact absurd hp (h hx)
|
||||
|
||||
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
|
||||
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
|
||||
|
||||
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
|
||||
example : (¬∀ x, p x) ↔ (∃ x, ¬p x) := forall_negation α p
|
||||
|
||||
end ex_1_4_5
|
||||
example : (∀ x, p x → r) ↔ (∃ x, p x) → r := by
|
||||
apply Iff.intro
|
||||
· intro h ⟨hx, hp⟩
|
||||
exact h hx hp
|
||||
· intro h hx hp
|
||||
exact h ⟨hx, hp⟩
|
||||
|
||||
example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r := by
|
||||
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⟩
|
||||
|
||||
example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) := by
|
||||
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
|
||||
|
||||
-- Exercise 2
|
||||
--
|
||||
-- Use tactic combinators to obtain a one line proof of the following:
|
||||
section ex_2
|
||||
namespace ex2
|
||||
|
||||
example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) :=
|
||||
by simp *
|
||||
by simp [*]
|
||||
|
||||
end ex_2
|
||||
end ex2
|
||||
|
|
|
|||
|
|
@ -1,8 +1,7 @@
|
|||
/- Exercises 7.10
|
||||
/- Exercises 7
|
||||
-
|
||||
- Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
|
||||
-/
|
||||
import data.nat.basic
|
||||
|
||||
-- Exercise 1
|
||||
--
|
||||
|
|
@ -15,41 +14,63 @@ import data.nat.basic
|
|||
-- Since many of these are already defined in Lean’s core library, you should
|
||||
-- work within a namespace named hide, or something like that, in order to avoid
|
||||
-- name clashes.
|
||||
namespace ex_1
|
||||
namespace ex1
|
||||
|
||||
-- As defined in the book.
|
||||
inductive nat : Type
|
||||
| zero : nat
|
||||
| succ : nat → nat
|
||||
inductive Nat where
|
||||
| zero : Nat
|
||||
| succ : Nat → Nat
|
||||
|
||||
def add (m n : nat) : nat :=
|
||||
nat.rec_on n m (λ k ak, nat.succ ak)
|
||||
namespace Nat
|
||||
|
||||
theorem add_zero (m : nat) : add m nat.zero = m := rfl
|
||||
theorem add_succ (m n : nat) : add m n.succ = (add m n).succ := rfl
|
||||
def add (m n : Nat) : Nat :=
|
||||
match n with
|
||||
| Nat.zero => m
|
||||
| Nat.succ n => Nat.succ (add m n)
|
||||
|
||||
theorem zero_add (n : nat) : add nat.zero n = n :=
|
||||
nat.rec_on n
|
||||
(add_zero nat.zero)
|
||||
(assume n ih,
|
||||
show add nat.zero (nat.succ n) = nat.succ n, from calc
|
||||
add nat.zero (nat.succ n) = nat.succ (add nat.zero n) : add_succ nat.zero n
|
||||
... = nat.succ n : by rw ih)
|
||||
instance : Add Nat where
|
||||
add := add
|
||||
|
||||
theorem addZero (m : Nat) : m + Nat.zero = m :=
|
||||
rfl
|
||||
|
||||
theorem addSucc (m n : Nat) : m + n.succ = (m + n).succ :=
|
||||
rfl
|
||||
|
||||
theorem zeroAdd (n : Nat) : Nat.zero + n = n :=
|
||||
Nat.recOn (motive := fun x => Nat.zero + x = x)
|
||||
n
|
||||
(show Nat.zero + Nat.zero = Nat.zero from rfl)
|
||||
(fun (n : Nat) (ih : Nat.zero + n = n) =>
|
||||
show Nat.zero + n.succ = n.succ from
|
||||
calc
|
||||
Nat.zero + n.succ = (Nat.zero + n).succ := addSucc Nat.zero n
|
||||
_ = n.succ := by rw [ih])
|
||||
|
||||
-- Additional definitions.
|
||||
def mul (m n : nat) : nat :=
|
||||
nat.rec_on n nat.zero (λ k ak, add m ak)
|
||||
def mul (m n : Nat) : Nat := sorry
|
||||
|
||||
def pred (n : nat) : nat :=
|
||||
nat.cases_on n nat.zero id
|
||||
-- def mul (m n : nat) : nat :=
|
||||
-- nat.rec_on n nat.zero (λ k ak, add m ak)
|
||||
|
||||
def sub (m n : nat) : nat :=
|
||||
nat.rec_on n m (λ k ak, pred ak)
|
||||
def pred (n : Nat) : Nat := sorry
|
||||
|
||||
def exp (m n : nat) : nat :=
|
||||
nat.rec_on n (nat.zero.succ) (λ k ak, mul m ak)
|
||||
-- def pred (n : nat) : nat :=
|
||||
-- nat.cases_on n nat.zero id
|
||||
|
||||
end ex_1
|
||||
def sub (m n : Nat) : Nat := sorry
|
||||
|
||||
-- def sub (m n : nat) : nat :=
|
||||
-- nat.rec_on n m (λ k ak, pred ak)
|
||||
|
||||
def exp (m n : Nat) : Nat := sorry
|
||||
|
||||
-- def exp (m n : nat) : nat :=
|
||||
-- nat.rec_on n (nat.zero.succ) (λ k ak, mul m ak)
|
||||
|
||||
end Nat
|
||||
|
||||
end ex1
|
||||
|
||||
-- Exercise 2
|
||||
--
|
||||
|
|
@ -59,46 +80,45 @@ end ex_1
|
|||
-- a. `length (s ++ t) = length s + length t`
|
||||
-- b. `length (reverse t) = length t`
|
||||
-- c. `reverse (reverse t) = t`
|
||||
section ex_2
|
||||
namespace ex2
|
||||
|
||||
open list
|
||||
open List
|
||||
|
||||
variable {α : Type*}
|
||||
variable {α : Type _}
|
||||
|
||||
-- Additional theorems.
|
||||
theorem length_sum (s t : list α) : length (s ++ t) = length s + length t :=
|
||||
list.rec_on s
|
||||
(by rw [nil_append, length, zero_add])
|
||||
(assume hd tl ih, by rw [
|
||||
length,
|
||||
cons_append,
|
||||
length,
|
||||
ih,
|
||||
add_assoc,
|
||||
add_comm t.length,
|
||||
add_assoc
|
||||
])
|
||||
-- theorem length_sum (s t : list α) : length (s ++ t) = length s + length t :=
|
||||
-- list.rec_on s
|
||||
-- (by rw [nil_append, length, zero_add])
|
||||
-- (assume hd tl ih, by rw [
|
||||
-- length,
|
||||
-- cons_append,
|
||||
-- length,
|
||||
-- ih,
|
||||
-- add_assoc,
|
||||
-- add_comm t.length,
|
||||
-- add_assoc
|
||||
-- ])
|
||||
--
|
||||
-- lemma cons_reverse (hd : α) (tl : list α)
|
||||
-- : reverse (hd :: tl) = reverse tl ++ [hd] :=
|
||||
-- sorry
|
||||
--
|
||||
-- theorem length_reverse (t : list α) : length (reverse t) = length t :=
|
||||
-- list.rec_on t
|
||||
-- (by unfold reverse reverse_core)
|
||||
-- (assume hd tl ih, begin
|
||||
-- unfold length,
|
||||
-- rw cons_reverse,
|
||||
-- rw length_sum,
|
||||
-- unfold length,
|
||||
-- rw zero_add,
|
||||
-- rw ih,
|
||||
-- end)
|
||||
--
|
||||
-- theorem reverse_reverse (t : list α) : reverse (reverse t) = t :=
|
||||
-- list.rec_on t rfl (assume hd tl ih, sorry)
|
||||
|
||||
lemma cons_reverse (hd : α) (tl : list α)
|
||||
: reverse (hd :: tl) = reverse tl ++ [hd] :=
|
||||
sorry
|
||||
|
||||
theorem length_reverse (t : list α) : length (reverse t) = length t :=
|
||||
list.rec_on t
|
||||
(by unfold reverse reverse_core)
|
||||
(assume hd tl ih, begin
|
||||
unfold length,
|
||||
rw cons_reverse,
|
||||
rw length_sum,
|
||||
unfold length,
|
||||
rw zero_add,
|
||||
rw ih,
|
||||
end)
|
||||
|
||||
theorem reverse_reverse (t : list α) : reverse (reverse t) = t :=
|
||||
list.rec_on t rfl (assume hd tl ih, sorry)
|
||||
|
||||
end ex_2
|
||||
end ex2
|
||||
|
||||
-- Exercise 3
|
||||
--
|
||||
|
|
@ -112,27 +132,27 @@ end ex_2
|
|||
--
|
||||
-- Recursively define a function that evaluates any such term with respect to an
|
||||
-- assignment of values to the variables.
|
||||
namespace ex_3
|
||||
namespace ex3
|
||||
|
||||
inductive foo : Type*
|
||||
| const : ℕ → foo
|
||||
| var : ℕ → foo
|
||||
| plus : foo → foo → foo
|
||||
| times : foo → foo → foo
|
||||
-- inductive foo : Type*
|
||||
-- | const : ℕ → foo
|
||||
-- | var : ℕ → foo
|
||||
-- | plus : foo → foo → foo
|
||||
-- | times : foo → foo → foo
|
||||
--
|
||||
-- def value_at : ℕ → list ℕ → ℕ
|
||||
-- | 0 vs := list.head vs
|
||||
-- | i [] := default
|
||||
-- | (i + 1) vs := value_at i (list.tail vs)
|
||||
--
|
||||
-- -- The provided "variables" are supplied in a 0-indexed list.
|
||||
-- def eval_foo : foo → list ℕ → ℕ
|
||||
-- | (foo.const n) vs := n
|
||||
-- | (foo.var n) vs := value_at n vs
|
||||
-- | (foo.plus m n) vs := eval_foo m vs + eval_foo n vs
|
||||
-- | (foo.times m n) vs := eval_foo m vs * eval_foo n vs
|
||||
|
||||
def value_at : ℕ → list ℕ → ℕ
|
||||
| 0 vs := list.head vs
|
||||
| i [] := default
|
||||
| (i + 1) vs := value_at i (list.tail vs)
|
||||
|
||||
-- The provided "variables" are supplied in a 0-indexed list.
|
||||
def eval_foo : foo → list ℕ → ℕ
|
||||
| (foo.const n) vs := n
|
||||
| (foo.var n) vs := value_at n vs
|
||||
| (foo.plus m n) vs := eval_foo m vs + eval_foo n vs
|
||||
| (foo.times m n) vs := eval_foo m vs * eval_foo n vs
|
||||
|
||||
end ex_3
|
||||
end ex3
|
||||
|
||||
-- Exercise 4
|
||||
--
|
||||
|
|
@ -140,35 +160,35 @@ end ex_3
|
|||
-- the type of such formulas: an evaluation function, functions that measure the
|
||||
-- complexity of a formula, and a function that substitutes another formula for
|
||||
-- a given variable.
|
||||
namespace ex_4
|
||||
namespace ex4
|
||||
|
||||
inductive foo : Type*
|
||||
| tt : foo
|
||||
| ff : foo
|
||||
| and : foo → foo → foo
|
||||
| or : foo → foo → foo
|
||||
-- inductive foo : Type*
|
||||
-- | tt : foo
|
||||
-- | ff : foo
|
||||
-- | and : foo → foo → foo
|
||||
-- | or : foo → foo → foo
|
||||
--
|
||||
-- def eval_foo : foo → bool
|
||||
-- | foo.tt := true
|
||||
-- | foo.ff := false
|
||||
-- | (foo.and lhs rhs) := eval_foo lhs ∧ eval_foo rhs
|
||||
-- | (foo.or lhs rhs) := eval_foo lhs ∨ eval_foo rhs
|
||||
--
|
||||
-- def complexity_foo : foo → ℕ
|
||||
-- | foo.tt := 1
|
||||
-- | foo.ff := 1
|
||||
-- | (foo.and lhs rhs) := 1 + complexity_foo lhs + complexity_foo rhs
|
||||
-- | (foo.or lhs rhs) := 1 + complexity_foo lhs + complexity_foo rhs
|
||||
--
|
||||
-- def substitute : foo → foo := sorry
|
||||
|
||||
def eval_foo : foo → bool
|
||||
| foo.tt := true
|
||||
| foo.ff := false
|
||||
| (foo.and lhs rhs) := eval_foo lhs ∧ eval_foo rhs
|
||||
| (foo.or lhs rhs) := eval_foo lhs ∨ eval_foo rhs
|
||||
|
||||
def complexity_foo : foo → ℕ
|
||||
| foo.tt := 1
|
||||
| foo.ff := 1
|
||||
| (foo.and lhs rhs) := 1 + complexity_foo lhs + complexity_foo rhs
|
||||
| (foo.or lhs rhs) := 1 + complexity_foo lhs + complexity_foo rhs
|
||||
|
||||
def substitute : foo → foo := sorry
|
||||
|
||||
end ex_4
|
||||
end ex4
|
||||
|
||||
-- Exercise 5
|
||||
--
|
||||
-- Simulate the mutual inductive definition of `even` and `odd` described in
|
||||
-- Section 7.9 with an ordinary inductive type, using an index to encode the
|
||||
-- choice between them in the target type.
|
||||
section ex_5
|
||||
namespace ex5
|
||||
|
||||
end ex_5
|
||||
end ex5
|
||||
|
|
|
|||
Loading…
Reference in New Issue