Add documentation throughout modules.
parent
cab7aa82a3
commit
4b32563cee
|
|
@ -1,5 +1,20 @@
|
|||
/-! # Bookshelf.Combinator.Aviary
|
||||
|
||||
A collection of combinator birds representable in Lean. Certain duplicators,
|
||||
e.g. mockingbirds, are not directly expressible since they would require
|
||||
encoding a signature in which an argument has types `α` *and* `α → α`.
|
||||
|
||||
Duplicators that are included, e.g. the warbler, are not exactly correct
|
||||
considering they still have the same limitation described above during actual
|
||||
use. Their inclusion here serves more as pseudo-documentation than anything.
|
||||
|
||||
[^1]: Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles
|
||||
Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford
|
||||
university press, 2000.
|
||||
-/
|
||||
|
||||
/--
|
||||
Bald Eagle
|
||||
#### Bald Eagle
|
||||
|
||||
`E'xy₁y₂y₃z₁z₂z₃ = x(y₁y₂y₃)(z₁z₂z₃)`
|
||||
-/
|
||||
|
|
@ -8,35 +23,35 @@ def E' (x : α → β → γ)
|
|||
(z₁ : ζ → η → β) (z₂ : ζ) (z₃ : η) := x (y₁ y₂ y₃) (z₁ z₂ z₃)
|
||||
|
||||
/--
|
||||
Becard
|
||||
#### Becard
|
||||
|
||||
`B₃xyzw = x(y(zw))`
|
||||
-/
|
||||
def B₃ (x : α → ε) (y : β → α) (z : γ → β) (w : γ) := x (y (z w))
|
||||
|
||||
/--
|
||||
Blackbird
|
||||
#### Blackbird
|
||||
|
||||
`B₁xyzw = x(yzw)`
|
||||
-/
|
||||
def B₁ (x : α → ε) (y : β → γ → α) (z : β) (w : γ) := x (y z w)
|
||||
|
||||
/--
|
||||
Bluebird
|
||||
#### Bluebird
|
||||
|
||||
`Bxyz = x(yz)`
|
||||
-/
|
||||
def B (x : α → γ) (y : β → α) (z : β) := x (y z)
|
||||
|
||||
/--
|
||||
Bunting
|
||||
#### Bunting
|
||||
|
||||
`B₂xyzwv = x(yzwv)`
|
||||
-/
|
||||
def B₂ (x : α → ζ) (y : β → γ → ε → α) (z : β) (w : γ) (v : ε) := x (y z w v)
|
||||
|
||||
/--
|
||||
Cardinal Once Removed
|
||||
#### Cardinal Once Removed
|
||||
|
||||
`C*xyzw = xywz`
|
||||
-/
|
||||
|
|
@ -45,49 +60,49 @@ def C_star (x : α → β → γ → δ) (y : α) (z : γ) (w : β) := x y w z
|
|||
notation "C*" => C_star
|
||||
|
||||
/--
|
||||
Cardinal
|
||||
#### Cardinal
|
||||
|
||||
`Cxyz = xzy`
|
||||
-/
|
||||
def C (x : α → β → δ) (y : β) (z : α) := x z y
|
||||
|
||||
/--
|
||||
Converse Warbler
|
||||
#### Converse Warbler
|
||||
|
||||
`W'xy = yxx`
|
||||
-/
|
||||
def W' (x : α) (y : α → α → β) := y x x
|
||||
|
||||
/--
|
||||
Dickcissel
|
||||
#### Dickcissel
|
||||
|
||||
`D₁xyzwv = xyz(wv)`
|
||||
-/
|
||||
def D₁ (x : α → β → δ → ε) (y : α) (z : β) (w : γ → δ) (v : γ) := x y z (w v)
|
||||
|
||||
/--
|
||||
Dove
|
||||
#### Dove
|
||||
|
||||
`Dxyzw = xy(zw)`
|
||||
-/
|
||||
def D (x : α → γ → δ) (y : α) (z : β → γ) (w : β) := x y (z w)
|
||||
|
||||
/--
|
||||
Dovekie
|
||||
#### Dovekie
|
||||
|
||||
`D₂xyzwv = x(yz)(wv)`
|
||||
-/
|
||||
def D₂ (x : α → δ → ε) (y : β → α) (z : β) (w : γ → δ) (v : γ) := x (y z) (w v)
|
||||
|
||||
/--
|
||||
Eagle
|
||||
#### Eagle
|
||||
|
||||
`Exyzwv = xy(zwv)`
|
||||
-/
|
||||
def E (x : α → δ → ε) (y : α) (z : β → γ → δ) (w : β) (v : γ) := x y (z w v)
|
||||
|
||||
/--
|
||||
Finch Once Removed
|
||||
#### Finch Once Removed
|
||||
|
||||
`F*xyzw = xwzy`
|
||||
-/
|
||||
|
|
@ -96,98 +111,98 @@ def F_star (x : α → β → γ → δ) (y : γ) (z : β) (w : α) := x w z y
|
|||
notation "F*" => F_star
|
||||
|
||||
/--
|
||||
Finch
|
||||
#### Finch
|
||||
|
||||
`Fxyz = zyx`
|
||||
-/
|
||||
def F (x : α) (y : β) (z : β → α → γ) := z y x
|
||||
|
||||
/--
|
||||
Goldfinch
|
||||
#### Goldfinch
|
||||
|
||||
`Gxyzw = xw(yz)`
|
||||
-/
|
||||
def G (x : α → γ → δ) (y : β → γ) (z : β) (w : α) := x w (y z)
|
||||
|
||||
/--
|
||||
Hummingbird
|
||||
#### Hummingbird
|
||||
|
||||
`Hxyz = xyzy`
|
||||
-/
|
||||
def H (x : α → β → α → γ) (y : α) (z : β) := x y z y
|
||||
|
||||
/--
|
||||
Identity Bird
|
||||
#### Identity Bird
|
||||
|
||||
`Ix = x`
|
||||
-/
|
||||
def I (x : α) : α := x
|
||||
|
||||
/--
|
||||
Kestrel
|
||||
#### Kestrel
|
||||
|
||||
`Kxy = x`
|
||||
-/
|
||||
def K (x : α) (_ : β) := x
|
||||
|
||||
/--
|
||||
Owl
|
||||
#### Owl
|
||||
|
||||
`Oxy = y(xy)`
|
||||
-/
|
||||
def O (x : (α → β) → α) (y : α → β) := y (x y)
|
||||
|
||||
/--
|
||||
Phoenix
|
||||
#### Phoenix
|
||||
|
||||
`Φxyzw = x(yw)(zw)`
|
||||
-/
|
||||
def Φ (x : β → γ → δ) (y : α → β) (z : α → γ) (w : α) := x (y w) (z w)
|
||||
|
||||
/--
|
||||
Psi Bird
|
||||
#### Psi Bird
|
||||
|
||||
`Ψxyzw = x(yz)(yw)`
|
||||
-/
|
||||
def Ψ (x : α → α → γ) (y : β → α) (z : β) (w : β) := x (y z) (y w)
|
||||
|
||||
/--
|
||||
Quacky Bird
|
||||
#### Quacky Bird
|
||||
|
||||
`Q₄xyz = z(yx)`
|
||||
-/
|
||||
def Q₄ (x : α) (y : α → β) (z : β → γ) := z (y x)
|
||||
|
||||
/--
|
||||
Queer Bird
|
||||
#### Queer Bird
|
||||
|
||||
`Qxyz = y(xz)`
|
||||
-/
|
||||
def Q (x : α → β) (y : β → γ) (z : α) := y (x z)
|
||||
|
||||
/--
|
||||
Quirky Bird
|
||||
#### Quirky Bird
|
||||
|
||||
`Q₃xyz = z(xy)`
|
||||
-/
|
||||
def Q₃ (x : α → β) (y : α) (z : β → γ) := z (x y)
|
||||
|
||||
/--
|
||||
Quixotic Bird
|
||||
#### Quixotic Bird
|
||||
|
||||
`Q₁xyz = x(zy)`
|
||||
-/
|
||||
def Q₁ (x : α → γ) (y : β) (z : β → α) := x (z y)
|
||||
|
||||
/--
|
||||
Quizzical Bird
|
||||
#### Quizzical Bird
|
||||
|
||||
`Q₂xyz = y(zx)`
|
||||
-/
|
||||
def Q₂ (x : α) (y : β → γ) (z : α → β) := y (z x)
|
||||
|
||||
/--
|
||||
Robin Once Removed
|
||||
#### Robin Once Removed
|
||||
|
||||
`R*xyzw = xzwy`
|
||||
-/
|
||||
|
|
@ -196,35 +211,35 @@ def R_star (x : α → β → γ → δ) (y : γ) (z : α) (w : β) := x z w y
|
|||
notation "R*" => R_star
|
||||
|
||||
/--
|
||||
Robin
|
||||
#### Robin
|
||||
|
||||
`Rxyz = yzx`
|
||||
-/
|
||||
def R (x : α) (y : β → α → γ) (z : β) := y z x
|
||||
|
||||
/--
|
||||
Sage Bird
|
||||
#### Sage Bird
|
||||
|
||||
`Θx = x(Θx)`
|
||||
-/
|
||||
partial def Θ [Inhabited α] (x : α → α) := x (Θ x)
|
||||
|
||||
/--
|
||||
Starling
|
||||
#### Starling
|
||||
|
||||
`Sxyz = xz(yz)`
|
||||
-/
|
||||
def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
|
||||
|
||||
/--
|
||||
Thrush
|
||||
#### Thrush
|
||||
|
||||
`Txy = yx`
|
||||
-/
|
||||
def T (x : α) (y : α → β) := y x
|
||||
|
||||
/--
|
||||
Vireo Once Removed
|
||||
#### Vireo Once Removed
|
||||
|
||||
`V*xyzw = xwyz`
|
||||
-/
|
||||
|
|
@ -233,14 +248,14 @@ def V_star (x : α → β → γ → δ) (y : β) (z : γ) (w : α) := x w y z
|
|||
notation "V*" => V_star
|
||||
|
||||
/--
|
||||
Vireo
|
||||
#### Vireo
|
||||
|
||||
`Vxyz = zxy`
|
||||
-/
|
||||
def V (x : α) (y : β) (z : α → β → γ) := z x y
|
||||
|
||||
/--
|
||||
Warbler
|
||||
#### Warbler
|
||||
|
||||
`Wxy = xyy`
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -1,21 +1,34 @@
|
|||
import Mathlib.Tactic.Ring
|
||||
|
||||
/-! # Bookshelf.LTuple.Basic
|
||||
|
||||
The following is a representation of a (possibly empty) left-biased tuple. A
|
||||
left-biased `n`-tuple is defined recursively as follows:
|
||||
|
||||
```
|
||||
⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩
|
||||
```
|
||||
|
||||
Note a `Tuple` exists in Lean already. This implementation differs in two
|
||||
notable ways:
|
||||
|
||||
1. It is left-associative. The built-in `Tuple` instance evaluates e.g.
|
||||
`(x₁, x₂, x₃)` as `(x₁, (x₂, x₃))` instead of `((x₁, x₂), x₃)`.
|
||||
2. Internally, the built-in `Tuple` instance is syntactic sugar for nested
|
||||
`Prod` instances. Unlike this implementation, an `LTuple` is a homogeneous
|
||||
collection.
|
||||
|
||||
In general, prefer using `Prod` over `LTuple`. This exists primarily to solve
|
||||
certain theorems outlined in [^1].
|
||||
|
||||
[^1]: Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San
|
||||
Diego: Harcourt/Academic Press, 2001.
|
||||
-/
|
||||
|
||||
/--
|
||||
A representation of a possibly empty left-biased tuple. `n`-tuples are defined
|
||||
recursively as follows:
|
||||
#### LTuple
|
||||
|
||||
`⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩`
|
||||
|
||||
Keep in mind a tuple in Lean already exists but it differs in two ways:
|
||||
|
||||
1. It is right associative. That is, `(x₁, x₂, x₃)` evaluates to
|
||||
`(x₁, (x₂, x₃))` instead of `((x₁, x₂), x₃)`.
|
||||
2. Internally a tuple is syntactic sugar for nested `Prod` instances. Inputs
|
||||
types of `Prod` are not required to be the same meaning non-homogeneous
|
||||
collections are allowed.
|
||||
|
||||
In general, prefer using `Prod` over this `Tuple` definition. This exists solely
|
||||
for proving theorems outlined in Enderton's book.
|
||||
A left-biased, possibly empty, homogeneous `Tuple`-like structure..
|
||||
-/
|
||||
inductive LTuple : (α : Type u) → (size : Nat) → Type u where
|
||||
| nil : LTuple α 0
|
||||
|
|
@ -23,9 +36,7 @@ inductive LTuple : (α : Type u) → (size : Nat) → Type u where
|
|||
|
||||
namespace LTuple
|
||||
|
||||
-- ========================================
|
||||
-- Coercions
|
||||
-- ========================================
|
||||
/-! ## Coercions -/
|
||||
|
||||
scoped instance : CoeOut (LTuple α (min (m + n) m)) (LTuple α m) where
|
||||
coe := cast (by simp)
|
||||
|
|
@ -48,17 +59,19 @@ scoped instance : Coe (LTuple α (min m n + 1)) (LTuple α (min (m + 1) (n + 1))
|
|||
scoped instance : Coe (LTuple α m) (LTuple α (min (m + n) m)) where
|
||||
coe := cast (by simp)
|
||||
|
||||
-- ========================================
|
||||
-- Equality
|
||||
-- ========================================
|
||||
|
||||
theorem eq_nil : @LTuple.nil α = nil := rfl
|
||||
/-! ### Equality -/
|
||||
|
||||
/--
|
||||
Two values `a` and `b` are equal **iff** `[a] = [b]`.
|
||||
-/
|
||||
theorem eq_iff_singleton : (a = b) ↔ (snoc a nil = snoc b nil) := by
|
||||
apply Iff.intro
|
||||
· intro h; rw [h]
|
||||
· intro h; injection h
|
||||
|
||||
/--
|
||||
Two lists are equal **iff** their heads and tails are equal.
|
||||
-/
|
||||
theorem eq_iff_snoc {t₁ t₂ : LTuple α n}
|
||||
: (a = b ∧ t₁ = t₂) ↔ (snoc t₁ a = snoc t₂ b) := by
|
||||
apply Iff.intro
|
||||
|
|
@ -74,7 +87,7 @@ equality.
|
|||
protected def hasDecEq [DecidableEq α] (t₁ t₂ : LTuple α n)
|
||||
: Decidable (Eq t₁ t₂) :=
|
||||
match t₁, t₂ with
|
||||
| nil, nil => isTrue eq_nil
|
||||
| nil, nil => isTrue rfl
|
||||
| snoc as a, snoc bs b =>
|
||||
match LTuple.hasDecEq as bs with
|
||||
| isFalse np => isFalse (fun h => absurd (eq_iff_snoc.mpr h).right np)
|
||||
|
|
@ -86,47 +99,43 @@ protected def hasDecEq [DecidableEq α] (t₁ t₂ : LTuple α n)
|
|||
|
||||
instance [DecidableEq α] : DecidableEq (LTuple α n) := LTuple.hasDecEq
|
||||
|
||||
-- ========================================
|
||||
-- Basic API
|
||||
-- ========================================
|
||||
/-! ## Basic API -/
|
||||
|
||||
/--
|
||||
Returns the number of entries of the `Tuple`.
|
||||
Returns the number of entries in an `LTuple`.
|
||||
-/
|
||||
def size (_ : LTuple α n) : Nat := n
|
||||
|
||||
/--
|
||||
Returns all but the last entry of the `Tuple`.
|
||||
Returns all but the last entry of an `LTuple`.
|
||||
-/
|
||||
def init : (t : LTuple α (n + 1)) → LTuple α n
|
||||
| snoc vs _ => vs
|
||||
|
||||
/--
|
||||
Returns the last entry of the `Tuple`.
|
||||
Returns the last entry of an `LTuple`.
|
||||
-/
|
||||
def last : LTuple α (n + 1) → α
|
||||
| snoc _ v => v
|
||||
|
||||
/--
|
||||
Prepends an entry to the start of the `Tuple`.
|
||||
Prepends an entry to an `LTuple`.
|
||||
-/
|
||||
def cons : LTuple α n → α → LTuple α (n + 1)
|
||||
| nil, a => snoc nil a
|
||||
| snoc ts t, a => snoc (cons ts a) t
|
||||
|
||||
-- ========================================
|
||||
-- Concatenation
|
||||
-- ========================================
|
||||
/-! ## Concatenation -/
|
||||
|
||||
/--
|
||||
Join two `Tuple`s together end to end.
|
||||
Joins two `LTuple`s together end to end.
|
||||
-/
|
||||
def concat : LTuple α m → LTuple α n → LTuple α (m + n)
|
||||
| is, nil => is
|
||||
| is, snoc ts t => snoc (concat is ts) t
|
||||
|
||||
/--
|
||||
Concatenating a `Tuple` with `nil` yields the original `Tuple`.
|
||||
Concatenating an `LTuple` with `nil` yields the original `LTuple`.
|
||||
-/
|
||||
theorem self_concat_nil_eq_self (t : LTuple α m) : concat t nil = t :=
|
||||
match t with
|
||||
|
|
@ -134,7 +143,7 @@ theorem self_concat_nil_eq_self (t : LTuple α m) : concat t nil = t :=
|
|||
| snoc _ _ => rfl
|
||||
|
||||
/--
|
||||
Concatenating `nil` with a `Tuple` yields the `Tuple`.
|
||||
Concatenating `nil` with an `LTuple` yields the original `LTuple`.
|
||||
-/
|
||||
theorem nil_concat_self_eq_self (t : LTuple α m) : concat nil t = t := by
|
||||
induction t with
|
||||
|
|
@ -158,15 +167,16 @@ theorem nil_concat_self_eq_self (t : LTuple α m) : concat nil t = t := by
|
|||
h₁
|
||||
|
||||
/--
|
||||
Concatenating a `Tuple` to a nonempty `Tuple` moves `concat` calls closer to
|
||||
expression leaves.
|
||||
Concatenating an `LTuple` to a nonempty `LTuple` moves `concat` calls closer to
|
||||
the expression leaves.
|
||||
-/
|
||||
theorem concat_snoc_snoc_concat {bs : LTuple α n}
|
||||
: concat as (snoc bs b) = snoc (concat as bs) b :=
|
||||
rfl
|
||||
|
||||
/--
|
||||
`snoc` is equivalent to concatenating the `init` and `last` element together.
|
||||
`snoc` is equivalent to concatenating the `init` and `last` elements of an
|
||||
`LTuple` together.
|
||||
-/
|
||||
theorem snoc_eq_init_concat_last (as : LTuple α m)
|
||||
: snoc as a = concat as (snoc nil a) := by
|
||||
|
|
@ -174,13 +184,11 @@ theorem snoc_eq_init_concat_last (as : LTuple α m)
|
|||
| nil => rfl
|
||||
| snoc _ _ => simp; unfold concat concat; rfl
|
||||
|
||||
-- ========================================
|
||||
-- Initial sequences
|
||||
-- ========================================
|
||||
/-! ## Initial Sequences -/
|
||||
|
||||
/--
|
||||
Take the first `k` entries from the `Tuple` to form a new `Tuple`, or the entire
|
||||
`Tuple` if `k` exceeds the number of entries.
|
||||
Takes the first `k` entries from an `LTuple` to form a new `LTuple`, or the
|
||||
entire `LTuple` if `k` exceeds the size.
|
||||
-/
|
||||
def take (t : LTuple α n) (k : Nat) : LTuple α (min n k) :=
|
||||
if h : n ≤ k then
|
||||
|
|
@ -196,7 +204,7 @@ def take (t : LTuple α n) (k : Nat) : LTuple α (min n k) :=
|
|||
rw [min_eq_right h', min_eq_right (Nat.le_trans h' (Nat.le_succ m))]
|
||||
|
||||
/--
|
||||
Taking no entries from any `Tuple` should yield an empty one.
|
||||
Taking no entries from any `LTuple` should yield an empty `LTuple`.
|
||||
-/
|
||||
theorem self_take_zero_eq_nil (t : LTuple α n) : take t 0 = @nil α := by
|
||||
induction t with
|
||||
|
|
@ -204,13 +212,14 @@ theorem self_take_zero_eq_nil (t : LTuple α n) : take t 0 = @nil α := by
|
|||
| snoc as a ih => unfold take; simp; rw [ih]; simp
|
||||
|
||||
/--
|
||||
Taking any number of entries from an empty `Tuple` should yield an empty one.
|
||||
Taking any number of entries from an empty `LTuple` should yield an empty
|
||||
`LTuple`.
|
||||
-/
|
||||
theorem nil_take_zero_eq_nil (k : Nat) : (take (@nil α) k) = @nil α := by
|
||||
cases k <;> (unfold take; simp)
|
||||
|
||||
/--
|
||||
Taking `n` entries from a `Tuple` of size `n` should yield the same `Tuple`.
|
||||
Taking `n` entries from an `LTuple` of size `n` should yield the same `LTuple`.
|
||||
-/
|
||||
theorem self_take_size_eq_self (t : LTuple α n) : take t n = t := by
|
||||
cases t with
|
||||
|
|
@ -218,8 +227,8 @@ theorem self_take_size_eq_self (t : LTuple α n) : take t n = t := by
|
|||
| snoc as a => unfold take; simp
|
||||
|
||||
/--
|
||||
Taking all but the last entry of a `Tuple` is the same result, regardless of the
|
||||
value of the last entry.
|
||||
Taking `n - 1` elements from an `LTuple` of size `n` yields the same result,
|
||||
regardless of the last entry's value.
|
||||
-/
|
||||
theorem take_subst_last {as : LTuple α n} (a₁ a₂ : α)
|
||||
: take (snoc as a₁) n = take (snoc as a₂) n := by
|
||||
|
|
@ -227,7 +236,8 @@ theorem take_subst_last {as : LTuple α n} (a₁ a₂ : α)
|
|||
simp
|
||||
|
||||
/--
|
||||
Taking `n` elements from a tuple of size `n + 1` is the same as invoking `init`.
|
||||
Taking `n` elements from an `LTuple` of size `n + 1` is the same as invoking
|
||||
`init`.
|
||||
-/
|
||||
theorem init_eq_take_pred (t : LTuple α (n + 1)) : take t n = init t := by
|
||||
cases t with
|
||||
|
|
@ -238,8 +248,8 @@ theorem init_eq_take_pred (t : LTuple α (n + 1)) : take t n = init t := by
|
|||
simp
|
||||
|
||||
/--
|
||||
If two `Tuple`s are equal, then any initial sequences of those two `Tuple`s are
|
||||
also equal.
|
||||
If two `LTuple`s are equal, then any initial sequences of these two `LTuple`s
|
||||
are also equal.
|
||||
-/
|
||||
theorem eq_tuple_eq_take {t₁ t₂ : LTuple α n}
|
||||
: (t₁ = t₂) → (t₁.take k = t₂.take k) := by
|
||||
|
|
@ -247,8 +257,8 @@ theorem eq_tuple_eq_take {t₁ t₂ : LTuple α n}
|
|||
rw [h]
|
||||
|
||||
/--
|
||||
Given a `Tuple` of size `k`, concatenating an arbitrary `Tuple` and taking `k`
|
||||
elements yields the original `Tuple`.
|
||||
Given an `LTuple` of size `k`, concatenating an arbitrary `LTuple` and taking
|
||||
`k` elements yields the original `LTuple`.
|
||||
-/
|
||||
theorem eq_take_concat {t₁ : LTuple α m} {t₂ : LTuple α n}
|
||||
: take (concat t₁ t₂) m = t₁ := by
|
||||
|
|
@ -264,4 +274,4 @@ theorem eq_take_concat {t₁ : LTuple α m} {t₂ : LTuple α n}
|
|||
rw [ih]
|
||||
simp
|
||||
|
||||
end LTuple
|
||||
end LTuple
|
||||
|
|
@ -1,27 +1,28 @@
|
|||
import Mathlib.Data.Fintype.Basic
|
||||
import Mathlib.Tactic.NormNum
|
||||
|
||||
/-! # Bookshelf.List.Basic
|
||||
|
||||
Additional theorems and definitions useful in the context of `List`s.
|
||||
-/
|
||||
|
||||
namespace List
|
||||
|
||||
-- ========================================
|
||||
-- Indexing
|
||||
-- ========================================
|
||||
/-! ## Indexing -/
|
||||
|
||||
/--
|
||||
Getting an element `i` from a list is equivalent to `get`ting an element `i + 1`
|
||||
from that list as a tail.
|
||||
Getting the `(i + 1)`st entry of a `List` is equivalent to getting the `i`th
|
||||
entry of the `List`'s tail.
|
||||
-/
|
||||
theorem get_cons_succ_self_eq_get_tail_self
|
||||
: get (x :: xs) (Fin.succ i) = get xs i := by
|
||||
conv => lhs; unfold get; simp only
|
||||
|
||||
-- ========================================
|
||||
-- Length
|
||||
-- ========================================
|
||||
/-! ### Length -/
|
||||
|
||||
/--
|
||||
A list is nonempty if and only if it can be written as a head concatenated with
|
||||
a tail.
|
||||
A `List` is nonempty **iff** it can be written as some head concatenated with
|
||||
some tail.
|
||||
-/
|
||||
theorem self_neq_nil_imp_exists_mem : xs ≠ [] ↔ (∃ a as, xs = a :: as) := by
|
||||
apply Iff.intro
|
||||
|
|
@ -34,7 +35,7 @@ theorem self_neq_nil_imp_exists_mem : xs ≠ [] ↔ (∃ a as, xs = a :: as) :=
|
|||
simp
|
||||
|
||||
/--
|
||||
Only the empty list has length zero.
|
||||
A `List` is empty **iff** it has length zero.
|
||||
-/
|
||||
theorem eq_nil_iff_length_zero : xs = [] ↔ length xs = 0 := by
|
||||
apply Iff.intro
|
||||
|
|
@ -47,7 +48,7 @@ theorem eq_nil_iff_length_zero : xs = [] ↔ length xs = 0 := by
|
|||
| cons a as => simp at h
|
||||
|
||||
/--
|
||||
If the length of a list is greater than zero, it cannot be `List.nil`.
|
||||
A `List` is nonempty **iff** it has length greater than zero.
|
||||
-/
|
||||
theorem neq_nil_iff_length_gt_zero : xs ≠ [] ↔ xs.length > 0 := by
|
||||
have : ¬xs = [] ↔ ¬length xs = 0 := Iff.not eq_nil_iff_length_zero
|
||||
|
|
@ -57,12 +58,10 @@ theorem neq_nil_iff_length_gt_zero : xs ≠ [] ↔ xs.length > 0 := by
|
|||
← zero_lt_iff
|
||||
] at this
|
||||
|
||||
-- ========================================
|
||||
-- Membership
|
||||
-- ========================================
|
||||
/-! ### Membership -/
|
||||
|
||||
/--
|
||||
If there exists a member of a list, the list must be nonempty.
|
||||
There exists a member of a `List` **iff** the `List` is nonempty.
|
||||
-/
|
||||
theorem exists_mem_iff_neq_nil : (∃ x, x ∈ xs) ↔ xs ≠ [] := by
|
||||
apply Iff.intro
|
||||
|
|
@ -74,18 +73,18 @@ theorem exists_mem_iff_neq_nil : (∃ x, x ∈ xs) ↔ xs ≠ [] := by
|
|||
| cons a as => exact ⟨a, by simp⟩
|
||||
|
||||
/--
|
||||
Any value that can be retrieved via `get` must be a member of the list argument.
|
||||
If `i` is a valid index of `List` `xs`, then `xs[i]` is a member of `xs`.
|
||||
-/
|
||||
theorem get_mem_self {xs : List α} {i : Fin xs.length} : get xs i ∈ xs := by
|
||||
induction xs with
|
||||
| nil => have ⟨_, hj⟩ := i; simp at hj
|
||||
| cons a as ih =>
|
||||
by_cases hk : i = ⟨0, by simp⟩
|
||||
· -- If `i = 0`, we are `get`ting the head of our list. This element is
|
||||
· -- If `i = 0`, we are `get`ting the head of our list. This entry is
|
||||
-- trivially a member of `xs`.
|
||||
conv => lhs; unfold get; rw [hk]; simp only
|
||||
simp
|
||||
· -- Otherwise we are `get`ting an element in the tail. Our induction
|
||||
· -- Otherwise we are `get`ting an entry in the tail. Our induction
|
||||
-- hypothesis closes this case.
|
||||
have ⟨k', hk'⟩ : ∃ k', i = Fin.succ k' := by
|
||||
have ni : ↑i ≠ (0 : ℕ) := fun hi => hk (Fin.ext hi)
|
||||
|
|
@ -98,8 +97,8 @@ theorem get_mem_self {xs : List α} {i : Fin xs.length} : get xs i ∈ xs := by
|
|||
exact mem_append_of_mem_right [a] ih
|
||||
|
||||
/--
|
||||
`x` is a member of list `xs` if and only if there exists some index of `xs` that
|
||||
`x` corresponds to.
|
||||
A value `x` is a member of `List` `xs` **iff** there exists some index `i` such
|
||||
that `x = xs[i]`.
|
||||
-/
|
||||
theorem mem_iff_exists_get {xs : List α}
|
||||
: x ∈ xs ↔ ∃ i : Fin xs.length, xs.get i = x := by
|
||||
|
|
@ -117,12 +116,10 @@ theorem mem_iff_exists_get {xs : List α}
|
|||
| nil => have nh := i.2; simp at nh
|
||||
| cons a bs => rw [← hi]; exact get_mem_self
|
||||
|
||||
-- ========================================
|
||||
-- Sublists
|
||||
-- ========================================
|
||||
/-! ## Sublists -/
|
||||
|
||||
/--
|
||||
Given nonempty list `xs`, `head` is equivalent to `get`ting the `0`th index.
|
||||
The first entry of a nonempty `List` has index `0`.
|
||||
-/
|
||||
theorem head_eq_get_zero {xs : List α} (h : xs ≠ [])
|
||||
: head xs h = get xs ⟨0, neq_nil_iff_length_gt_zero.mp h⟩ := by
|
||||
|
|
@ -131,8 +128,7 @@ theorem head_eq_get_zero {xs : List α} (h : xs ≠ [])
|
|||
simp
|
||||
|
||||
/--
|
||||
Given nonempty list `xs`, `getLast xs` is equivalent to `get`ting the
|
||||
`length - 1`th index.
|
||||
The last entry of a nonempty `List` has index `1` less than its length.
|
||||
-/
|
||||
theorem getLast_eq_get_length_sub_one {xs : List α} (h : xs ≠ [])
|
||||
: getLast xs h = get xs ⟨xs.length - 1, by
|
||||
|
|
@ -155,12 +151,11 @@ theorem some_tail?_imp_cons (h : tail? xs = some ys) : ∃ x, xs = x :: ys := by
|
|||
| nil => simp at h
|
||||
| cons r rs => exact ⟨r, by simp at h; rw [h]⟩
|
||||
|
||||
-- ========================================
|
||||
-- Zips
|
||||
-- ========================================
|
||||
/-! ### Zips -/
|
||||
|
||||
/--
|
||||
The length of a list zipped with its tail is the length of the tail.
|
||||
The length of a zip consisting of a `List` and its tail is the length of the
|
||||
`List`'s tail.
|
||||
-/
|
||||
theorem length_zipWith_self_tail_eq_length_sub_one
|
||||
: length (zipWith f (a :: as) as) = length as := by
|
||||
|
|
@ -170,7 +165,7 @@ theorem length_zipWith_self_tail_eq_length_sub_one
|
|||
simp only [le_add_iff_nonneg_right]
|
||||
|
||||
/--
|
||||
The result of a `zipWith` is nonempty if and only if both arguments are
|
||||
The output `List` of a `zipWith` is nonempty **iff** both of its inputs are
|
||||
nonempty.
|
||||
-/
|
||||
theorem zipWith_nonempty_iff_args_nonempty
|
||||
|
|
@ -190,7 +185,7 @@ theorem zipWith_nonempty_iff_args_nonempty
|
|||
simp
|
||||
|
||||
/--
|
||||
An index less than the length of a `zip` is less than the length of the left
|
||||
An index less than the length of a `zipWith` is less than the length of the left
|
||||
operand.
|
||||
-/
|
||||
theorem fin_zipWith_imp_val_lt_length_left {i : Fin (zipWith f xs ys).length}
|
||||
|
|
@ -200,7 +195,7 @@ theorem fin_zipWith_imp_val_lt_length_left {i : Fin (zipWith f xs ys).length}
|
|||
exact hi.left
|
||||
|
||||
/--
|
||||
An index less than the length of a `zip` is less than the length of the left
|
||||
An index less than the length of a `zipWith` is less than the length of the left
|
||||
operand.
|
||||
-/
|
||||
theorem fin_zipWith_imp_val_lt_length_right {i : Fin (zipWith f xs ys).length}
|
||||
|
|
@ -209,13 +204,11 @@ theorem fin_zipWith_imp_val_lt_length_right {i : Fin (zipWith f xs ys).length}
|
|||
simp only [length_zipWith, ge_iff_le, lt_min_iff] at hi
|
||||
exact hi.right
|
||||
|
||||
-- ========================================
|
||||
-- Pairwise
|
||||
-- ========================================
|
||||
/-! ### Pairwise -/
|
||||
|
||||
/--
|
||||
Given a list `xs` of length `k`, produces a list of length `k - 1` where the
|
||||
`i`th member of the resulting list is `f xs[i] xs[i + 1]`.
|
||||
Given a `List` `xs` of length `k`, this function produces a `List` of length
|
||||
`k - 1` where the `i`th member of the resulting `List` is `f xs[i] xs[i + 1]`.
|
||||
-/
|
||||
def pairwise (xs : List α) (f : α → α → β) : List β :=
|
||||
match xs.tail? with
|
||||
|
|
@ -223,8 +216,8 @@ def pairwise (xs : List α) (f : α → α → β) : List β :=
|
|||
| some ys => zipWith f xs ys
|
||||
|
||||
/--
|
||||
If list `xs` is empty, then any `pairwise` operation on `xs` yields an empty
|
||||
list.
|
||||
If `List` `xs` is empty, then any `pairwise` operation on `xs` yields an empty
|
||||
`List`.
|
||||
-/
|
||||
theorem len_pairwise_len_nil_eq_zero {xs : List α} (h : xs = [])
|
||||
: (xs.pairwise f).length = 0 := by
|
||||
|
|
@ -248,8 +241,8 @@ theorem len_pairwise_len_cons_sub_one {xs : List α} (h : xs.length > 0)
|
|||
conv => lhs; unfold length
|
||||
|
||||
/--
|
||||
If the `pairwise` list isn't empty, then the original list must have at least
|
||||
two elements.
|
||||
If a `pairwise`'d `List` isn't empty, then the input `List` must have at least
|
||||
two entries.
|
||||
-/
|
||||
theorem mem_pairwise_imp_length_self_ge_2 {xs : List α} (h : xs.pairwise f ≠ [])
|
||||
: xs.length ≥ 2 := by
|
||||
|
|
@ -263,8 +256,8 @@ theorem mem_pairwise_imp_length_self_ge_2 {xs : List α} (h : xs.pairwise f ≠
|
|||
| cons a' bs' => unfold length length; rw [add_assoc]; norm_num
|
||||
|
||||
/--
|
||||
If `x` is a member of the pairwise'd list, there must exist two (adjacent)
|
||||
elements of the list, say `x₁` and `x₂`, such that `x = f x₁ x₂`.
|
||||
If `x` is a member of a `pairwise`'d list, there must exist two (adjacent)
|
||||
entries of the list, say `x₁` and `x₂`, such that `x = f x₁ x₂`.
|
||||
-/
|
||||
theorem mem_pairwise_imp_exists_adjacent {xs : List α} (h : x ∈ xs.pairwise f)
|
||||
: ∃ i : Fin (xs.length - 1), ∃ x₁ x₂,
|
||||
|
|
|
|||
|
|
@ -1,14 +1,30 @@
|
|||
import Mathlib.Data.Real.Basic
|
||||
|
||||
/-! # Bookshelf.Real.Basic
|
||||
|
||||
A collection of basic notational conveniences.
|
||||
-/
|
||||
|
||||
/--
|
||||
An abbreviation of `ℝ²` as the Cartesian product `ℝ × ℝ`.
|
||||
-/
|
||||
notation "ℝ²" => ℝ × ℝ
|
||||
|
||||
namespace Real
|
||||
|
||||
/--
|
||||
The area of a unit circle.
|
||||
Definitionally, the area of a unit circle.
|
||||
|
||||
###### PORT
|
||||
|
||||
As of now, this remains an `axiom`, but it should be replaced by the definition
|
||||
in `Mathlib` once ported to Lean 4.
|
||||
-/
|
||||
axiom pi : ℝ
|
||||
|
||||
/--
|
||||
An abbreviation of `pi` as symbol `π`.
|
||||
-/
|
||||
notation "π" => pi
|
||||
|
||||
end Real
|
||||
|
|
@ -1,6 +1,11 @@
|
|||
import Bookshelf.Real.Basic
|
||||
import Bookshelf.Real.Set.Partition
|
||||
|
||||
/-! # Bookshelf.Real.Function.Step
|
||||
|
||||
A characterization of step functions.
|
||||
-/
|
||||
|
||||
namespace Real.Function
|
||||
|
||||
open Partition
|
||||
|
|
|
|||
|
|
@ -1,6 +1,15 @@
|
|||
import Bookshelf.Real.Function.Step
|
||||
import Bookshelf.Real.Geometry.Rectangle
|
||||
|
||||
/-! # Bookshelf.Real.Geometry.Area
|
||||
|
||||
An axiomatic foundation for the concept of *area*. These axioms are those
|
||||
outlined in [^1].
|
||||
|
||||
[^1]: Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an
|
||||
Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
|
||||
-/
|
||||
|
||||
namespace Real.Geometry.Area
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -1,6 +1,10 @@
|
|||
import Bookshelf.Real.Basic
|
||||
import Mathlib.Data.Real.Sqrt
|
||||
|
||||
import Bookshelf.Real.Basic
|
||||
/-! # Bookshelf.Real.Geometry.Basic
|
||||
|
||||
A collection of useful definitions and theorems around geometry.
|
||||
-/
|
||||
|
||||
namespace Real
|
||||
|
||||
|
|
@ -8,7 +12,10 @@ namespace Real
|
|||
The undirected angle at `p₂` between the line segments to `p₁` and `p₃`. If
|
||||
either of those points equals `p₂`, this is `π / 2`.
|
||||
|
||||
PORT: `geometry.euclidean.angle`
|
||||
###### PORT
|
||||
|
||||
This should be replaced with the original Mathlib `geometry.euclidean.angle`
|
||||
definition once ported.
|
||||
-/
|
||||
axiom angle (p₁ p₂ p₃ : ℝ²) : ℝ
|
||||
|
||||
|
|
@ -24,10 +31,10 @@ noncomputable def dist (x y : ℝ²) :=
|
|||
Real.sqrt ((abs (y.1 - x.1)) ^ 2 + (abs (y.2 - x.2)) ^ 2)
|
||||
|
||||
/--
|
||||
Two sets `S` and `T` are `similar` iff there exists a one-to-one correspondence
|
||||
between `S` and `T` such that the distance between any two points `P, Q ∈ S` and
|
||||
corresponding points `P', Q' ∈ T` differ by some constant `α`. In other words,
|
||||
`α|PQ| = |P'Q'|`.
|
||||
Two sets `S` and `T` are `similar` **iff** there exists a one-to-one
|
||||
correspondence between `S` and `T` such that the distance between any two points
|
||||
`P, Q ∈ S` and corresponding points `P', Q' ∈ T` differ by some constant `α`. In
|
||||
other words, `α|PQ| = |P'Q'|`.
|
||||
-/
|
||||
def similar (S T : Set ℝ²) : Prop :=
|
||||
∃ f : ℝ² → ℝ², Function.Bijective f ∧
|
||||
|
|
@ -43,7 +50,7 @@ def congruent (S T : Set (ℝ × ℝ)) : Prop :=
|
|||
dist x y = dist (f x) (f y)
|
||||
|
||||
/--
|
||||
Any two congruent sets must be similar to one another.
|
||||
Any two `congruent` sets must be similar to one another.
|
||||
-/
|
||||
theorem congruent_similar {S T : Set ℝ²} : congruent S T → similar S T := by
|
||||
intro hc
|
||||
|
|
|
|||
|
|
@ -1,5 +1,15 @@
|
|||
import Bookshelf.Real.Geometry.Basic
|
||||
|
||||
/-! # Bookshelf.Real.Geometry.Rectangle
|
||||
|
||||
A characterization of a rectangle. This follows the definition as outlined in
|
||||
[^1]. Note that a `Point` and a `LineSegment` are both considered rectangles,
|
||||
with one or both dimensions equal to `0` respectively.
|
||||
|
||||
[^1]: Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an
|
||||
Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
|
||||
-/
|
||||
|
||||
namespace Real
|
||||
|
||||
/--
|
||||
|
|
@ -29,11 +39,17 @@ A `Rectangle` is the locus of points bounded by its edges.
|
|||
def set_def (r : Rectangle) : Set ℝ² :=
|
||||
sorry
|
||||
|
||||
/--
|
||||
A `Rectangle`'s top side is equal in length to its bottom side.
|
||||
-/
|
||||
theorem dist_top_eq_dist_bottom (r : Rectangle)
|
||||
: dist r.top_left r.top_right = dist r.bottom_left r.bottom_right := by
|
||||
unfold top_right dist
|
||||
repeat rw [add_comm, sub_right_comm, add_sub_cancel']
|
||||
|
||||
/--
|
||||
A `Rectangle`'s left side is equal in length to its right side.
|
||||
-/
|
||||
theorem dist_left_eq_dist_right (r : Rectangle)
|
||||
: dist r.top_left r.bottom_left = dist r.top_right r.bottom_right := by
|
||||
unfold top_right dist
|
||||
|
|
|
|||
|
|
@ -1,5 +1,12 @@
|
|||
import Bookshelf.Real.Basic
|
||||
|
||||
/-! # Bookshelf.Real.Rational
|
||||
|
||||
Additional theorems and definitions useful in the context of rational numbers.
|
||||
Most of these will likely be deleted once the corresponding functions in
|
||||
`Mathlib` are ported to Lean 4.
|
||||
-/
|
||||
|
||||
/--
|
||||
Assert that a real number is irrational.
|
||||
-/
|
||||
|
|
@ -7,8 +14,5 @@ def irrational (x : ℝ) := x ∉ Set.range RatCast.ratCast
|
|||
|
||||
/--
|
||||
Assert that a real number is rational.
|
||||
|
||||
Note this does *not* require the found rational to be in reduced form. Members
|
||||
of `ℚ` expect this (by proving the numerator and denominator are co-prime).
|
||||
-/
|
||||
def rational (x : ℝ) := ¬ irrational x
|
||||
|
|
|
|||
|
|
@ -1,5 +1,11 @@
|
|||
import Mathlib.Data.Real.Basic
|
||||
|
||||
/-! # Bookshelf.Real.Sequence.Arithmetic
|
||||
|
||||
A characterization of an arithmetic sequence, i.e. a sequence with a common
|
||||
difference between each term.
|
||||
-/
|
||||
|
||||
namespace Real
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -1,5 +1,11 @@
|
|||
import Mathlib.Data.Real.Basic
|
||||
|
||||
/-! # Bookshelf.Real.Sequence.Geometric
|
||||
|
||||
A characterization of a geometric sequence, i.e. a sequence with a common ratio
|
||||
between each term.
|
||||
-/
|
||||
|
||||
namespace Real
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -1,5 +1,10 @@
|
|||
import Mathlib.Data.Real.Basic
|
||||
|
||||
/-! # Bookshelf.Real.Set.Basic
|
||||
|
||||
A collection of useful definitions and theorems regarding sets.
|
||||
-/
|
||||
|
||||
namespace Real
|
||||
|
||||
/--
|
||||
|
|
@ -10,7 +15,7 @@ def minkowski_sum (s t : Set ℝ) :=
|
|||
{ x | ∃ a ∈ s, ∃ b ∈ t, x = a + b }
|
||||
|
||||
/--
|
||||
The sum of two sets is nonempty if and only if the summands are nonempty.
|
||||
The sum of two sets is nonempty **iff** the summands are nonempty.
|
||||
-/
|
||||
def nonempty_minkowski_sum_iff_nonempty_add_nonempty {s t : Set ℝ}
|
||||
: (minkowski_sum s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
|
||||
|
|
|
|||
|
|
@ -1,5 +1,11 @@
|
|||
import Mathlib.Data.Real.Basic
|
||||
|
||||
/-! # Bookshelf.Real.Set.Interval
|
||||
|
||||
A syntactic description of the various types of continuous intervals permitted
|
||||
on the real number line.
|
||||
-/
|
||||
|
||||
/--
|
||||
Representation of a closed interval.
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -1,7 +1,15 @@
|
|||
import Mathlib.Data.List.Sort
|
||||
|
||||
import Bookshelf.List.Basic
|
||||
import Bookshelf.Real.Set.Interval
|
||||
import Mathlib.Data.List.Sort
|
||||
|
||||
/-! # Bookshelf.Real.Set.Partition
|
||||
|
||||
A description of a partition as defined in the context of stepwise functions.
|
||||
Refer to [^1] for more information.
|
||||
|
||||
[^1]: Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an
|
||||
Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
|
||||
-/
|
||||
|
||||
namespace Real
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1 @@
|
|||
-- Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction
|
||||
-- to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
|
||||
import Exercises.Apostol.Chapter_I_3
|
||||
import Exercises.Apostol.Exercises_I_3_12
|
||||
|
|
|
|||
|
|
@ -1,22 +1,22 @@
|
|||
/-
|
||||
Chapter I 3
|
||||
import Bookshelf.Real.Set
|
||||
|
||||
/-! # Exercises.Apostol.Chapter_I_3
|
||||
|
||||
A Set of Axioms for the Real-Number System
|
||||
-/
|
||||
import Bookshelf.Real.Set
|
||||
|
||||
namespace Exercises.Apostol.Chapter_I_3
|
||||
|
||||
#check Archimedean
|
||||
#check Real.exists_isLUB
|
||||
|
||||
namespace Real
|
||||
|
||||
-- ========================================
|
||||
-- The least-upper-bound axiom (completeness axiom)
|
||||
-- ========================================
|
||||
/-! ## The least-upper-bound axiom (completeness axiom) -/
|
||||
|
||||
/--
|
||||
A property holds for the negation of elements in set `S` if and only if it also
|
||||
holds for the elements of the negation of `S`.
|
||||
A property holds for the negation of elements in set `S` **iff** it also holds
|
||||
for the elements of the negation of `S`.
|
||||
-/
|
||||
lemma set_neg_prop_iff_neg_set_prop (S : Set ℝ) (p : ℝ → Prop)
|
||||
: (∀ y, y ∈ S → p (-y)) ↔ (∀ y, y ∈ -S → p y) := by
|
||||
|
|
@ -79,8 +79,8 @@ lemma neg_upper_bounds_eq_lower_bounds_neg (S : Set ℝ)
|
|||
exact hx
|
||||
|
||||
/--
|
||||
An element `x` is the least element of the negation of a set if and only if `-x`
|
||||
if the greatest element of the set.
|
||||
An element `x` is the least element of the negation of a set **iff** `-x` is the
|
||||
greatest element of the set.
|
||||
-/
|
||||
lemma is_least_neg_set_eq_is_greatest_set_neq (S : Set ℝ)
|
||||
: IsLeast (-S) x = IsGreatest S (-x) := by
|
||||
|
|
@ -89,8 +89,8 @@ lemma is_least_neg_set_eq_is_greatest_set_neq (S : Set ℝ)
|
|||
rfl
|
||||
|
||||
/--
|
||||
At least with respect to `ℝ`, `x` is the least upper bound of set `-S` if and
|
||||
only if `-x` is the greatest lower bound of `S`.
|
||||
At least with respect to `ℝ`, `x` is the least upper bound of set `-S` **iff**
|
||||
`-x` is the greatest lower bound of `S`.
|
||||
-/
|
||||
theorem is_lub_neg_set_iff_is_glb_set_neg (S : Set ℝ)
|
||||
: IsLUB (-S) x = IsGLB S (-x) :=
|
||||
|
|
@ -100,8 +100,7 @@ theorem is_lub_neg_set_iff_is_glb_set_neg (S : Set ℝ)
|
|||
_ = IsGreatest (lowerBounds S) (-x) := by rw [is_least_neg_set_eq_is_greatest_set_neq]
|
||||
_ = IsGLB S (-x) := rfl
|
||||
|
||||
/--
|
||||
Theorem I.27
|
||||
/-- #### Theorem I.27
|
||||
|
||||
Every nonempty set `S` that is bounded below has a greatest lower bound; that
|
||||
is, there is a real number `L` such that `L = inf S`.
|
||||
|
|
@ -122,7 +121,7 @@ theorem exists_isGLB (S : Set ℝ) (hne : S.Nonempty) (hbdd : BddBelow S)
|
|||
rw [←bddAbove_def] at hbdd'
|
||||
-- Once we have found a supremum for `-S`, we argue the negation of this value
|
||||
-- is the same as the infimum of `S`.
|
||||
let ⟨ub, ubp⟩ := exists_isLUB (-S) hne' hbdd'
|
||||
let ⟨ub, ubp⟩ := Real.exists_isLUB (-S) hne' hbdd'
|
||||
exact ⟨-ub, (is_lub_neg_set_iff_is_glb_set_neg S).mp ubp⟩
|
||||
|
||||
/--
|
||||
|
|
@ -146,12 +145,9 @@ lemma leq_nat_abs_ceil_self (x : ℝ) : x ≤ Int.natAbs ⌈x⌉ := by
|
|||
_ ≤ 0 := le_of_lt (lt_of_not_le h)
|
||||
_ ≤ ↑(Int.natAbs ⌈x⌉) := GE.ge.le h'
|
||||
|
||||
-- ========================================
|
||||
-- The Archimedean property of the real-number system
|
||||
-- ========================================
|
||||
/-! ## The Archimedean property of the real-number system -/
|
||||
|
||||
/--
|
||||
Theorem I.29
|
||||
/-- #### Theorem I.29
|
||||
|
||||
For every real `x` there exists a positive integer `n` such that `n > x`.
|
||||
-/
|
||||
|
|
@ -163,8 +159,7 @@ theorem exists_pnat_geq_self (x : ℝ) : ∃ n : ℕ+, ↑n > x := by
|
|||
_ = x' := rfl
|
||||
exact ⟨x', h⟩
|
||||
|
||||
/--
|
||||
Theorem I.30
|
||||
/-- #### Theorem I.30
|
||||
|
||||
If `x > 0` and if `y` is an arbitrary real number, there exists a positive
|
||||
integer `n` such that `nx > y`.
|
||||
|
|
@ -179,8 +174,7 @@ theorem exists_pnat_mul_self_geq_of_pos {x y : ℝ}
|
|||
rw [div_mul, div_self (show x ≠ 0 from LT.lt.ne' hx), div_one] at p'
|
||||
exact ⟨n, p'⟩
|
||||
|
||||
/--
|
||||
Theorem I.31
|
||||
/-- #### Theorem I.31
|
||||
|
||||
If three real numbers `a`, `x`, and `y` satisfy the inequalities
|
||||
`a ≤ x ≤ a + y / n` for every integer `n ≥ 1`, then `x = a`.
|
||||
|
|
@ -245,9 +239,7 @@ theorem forall_pnat_frac_leq_self_leq_imp_eq {x y a : ℝ}
|
|||
have z : x < x := lt_of_le_of_lt (h 1).right r
|
||||
simp at z
|
||||
|
||||
-- ========================================
|
||||
-- Fundamental properties of the supremum and infimum
|
||||
-- ========================================
|
||||
/-! ## Fundamental properties of the supremum and infimum -/
|
||||
|
||||
/--
|
||||
Every member of a set `S` is less than or equal to some value `ub` if and only
|
||||
|
|
@ -278,8 +270,7 @@ lemma mem_imp_ge_lub {x : ℝ} (h : IsLUB S s) : x ∈ upperBounds S → x ≥ s
|
|||
intro hx
|
||||
exact h.right hx
|
||||
|
||||
/--
|
||||
Theorem I.32a
|
||||
/-- #### Theorem I.32a
|
||||
|
||||
Let `h` be a given positive number and let `S` be a set of real numbers. If `S`
|
||||
has a supremum, then for some `x` in `S` we have `x > sup S - h`.
|
||||
|
|
@ -330,8 +321,7 @@ lemma mem_imp_le_glb {x : ℝ} (h : IsGLB S s) : x ∈ lowerBounds S → x ≤ s
|
|||
intro hx
|
||||
exact h.right hx
|
||||
|
||||
/--
|
||||
Theorem I.32b
|
||||
/-- #### Theorem I.32b
|
||||
|
||||
Let `h` be a given positive number and let `S` be a set of real numbers. If `S`
|
||||
has an infimum, then for some `x` in `S` we have `x < inf S + h`.
|
||||
|
|
@ -353,8 +343,7 @@ theorem inf_imp_exists_lt_inf_add_delta {S : Set ℝ} {s h : ℝ} (hp : h > 0)
|
|||
exact le_of_not_gt (not_and.mp (nb x) hx)
|
||||
rwa [← mem_lower_bounds_iff_forall_ge] at nb'
|
||||
|
||||
/--
|
||||
Theorem I.33a (Additive Property)
|
||||
/-- #### Theorem I.33a (Additive Property)
|
||||
|
||||
Given nonempty subsets `A` and `B` of `ℝ`, let `C` denote the set
|
||||
`C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has a supremum, then `C`
|
||||
|
|
@ -377,7 +366,7 @@ theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ)
|
|||
_ ≤ a + b := add_le_add hs₁ hs₂
|
||||
-- Now we show `a + b` is the *least* upper bound of `C`. We know a least
|
||||
-- upper bound `c` exists; show that `c = a + b`.
|
||||
have ⟨c, hc⟩ := exists_isLUB C
|
||||
have ⟨c, hc⟩ := Real.exists_isLUB C
|
||||
(Real.nonempty_minkowski_sum_iff_nonempty_add_nonempty.mpr ⟨hA, hB⟩)
|
||||
⟨a + b, hub⟩
|
||||
suffices (∀ n : ℕ+, c ≤ a + b ∧ a + b ≤ c + (1 / n)) by
|
||||
|
|
@ -404,8 +393,7 @@ theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ)
|
|||
_ ≤ a' + b' + 1 / n := le_of_lt hab'
|
||||
_ ≤ c + 1 / n := add_le_add_right hc' (1 / n)
|
||||
|
||||
/--
|
||||
Theorem I.33b (Additive Property)
|
||||
/-- #### Theorem I.33b (Additive Property)
|
||||
|
||||
Given nonempty subsets `A` and `B` of `ℝ`, let `C` denote the set
|
||||
`C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has an infimum, then `C`
|
||||
|
|
@ -455,8 +443,7 @@ theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set ℝ)
|
|||
_ ≤ a + b := le_of_lt hab'
|
||||
· exact hc.right hlb
|
||||
|
||||
/--
|
||||
Theorem I.34
|
||||
/-- #### Theorem I.34
|
||||
|
||||
Given two nonempty subsets `S` and `T` of `ℝ` such that `s ≤ t` for every `s` in
|
||||
`S` and every `t` in `T`. Then `S` has a supremum, and `T` has an infimum, and
|
||||
|
|
@ -503,3 +490,158 @@ theorem forall_mem_le_forall_mem_imp_sup_le_inf (S T : Set ℝ)
|
|||
simp at this
|
||||
|
||||
end Real
|
||||
|
||||
/-! ## Exercises -/
|
||||
|
||||
/-- #### Exercise 1
|
||||
|
||||
If `x` and `y` are arbitrary real numbers with `x < y`, prove that there is at
|
||||
least one real `z` satisfying `x < z < y`.
|
||||
-/
|
||||
theorem exercise1 (x y : ℝ) (h : x < y) : ∃ z, x < z ∧ z < y := by
|
||||
have ⟨z, hz⟩ := exists_pos_add_of_lt' h
|
||||
refine ⟨x + z / 2, ⟨?_, ?_⟩⟩
|
||||
· have hz' : z / 2 > 0 := by
|
||||
have hr := div_lt_div_of_lt (show (0 : ℝ) < 2 by simp) hz.left
|
||||
rwa [zero_div] at hr
|
||||
exact (lt_add_iff_pos_right x).mpr hz'
|
||||
· have hz' : z / 2 < z := div_lt_self hz.left (show 1 < 2 by norm_num)
|
||||
calc x + z / 2
|
||||
_ < x + z := (add_lt_add_iff_left x).mpr hz'
|
||||
_ = y := hz.right
|
||||
|
||||
/-- #### Exercise 2
|
||||
|
||||
If `x` is an arbitrary real number, prove that there are integers `m` and `n`
|
||||
such that `m < x < n`.
|
||||
-/
|
||||
theorem exercise2 (x : ℝ) : ∃ m n : ℝ, m < x ∧ x < n := by
|
||||
refine ⟨x - 1, ⟨x + 1, ⟨?_, ?_⟩⟩⟩ <;> norm_num
|
||||
|
||||
/-- #### Exercise 3
|
||||
|
||||
If `x > 0`, prove that there is a positive integer `n` such that `1 / n < x`.
|
||||
-/
|
||||
theorem exercise3 (x : ℝ) (h : x > 0) : ∃ n : ℕ+, 1 / n < x := by
|
||||
have ⟨n, hn⟩ := @Real.exists_pnat_mul_self_geq_of_pos x 1 h
|
||||
refine ⟨n, ?_⟩
|
||||
have hr := mul_lt_mul_of_pos_right hn (show 0 < 1 / ↑↑n by norm_num)
|
||||
conv at hr => arg 2; rw [mul_comm, ← mul_assoc]; simp
|
||||
rwa [one_mul] at hr
|
||||
|
||||
/-- #### Exercise 4
|
||||
|
||||
If `x` is an arbitrary real number, prove that there is exactly one integer `n`
|
||||
which satisfies the inequalities `n ≤ x < n + 1`. This `n` is called the
|
||||
greatest integer in `x` and is denoted by `⌊x⌋`. For example, `⌊5⌋ = 5`,
|
||||
`⌊5 / 2⌋ = 2`, `⌊-8/3⌋ = -3`.
|
||||
-/
|
||||
theorem exercise4 (x : ℝ) : ∃! n : ℤ, n ≤ x ∧ x < n + 1 := by
|
||||
let n := Int.floor x
|
||||
refine ⟨n, ⟨?_, ?_⟩⟩
|
||||
· exact ⟨Int.floor_le x, Int.lt_floor_add_one x⟩
|
||||
· intro y hy
|
||||
rw [← Int.floor_eq_iff] at hy
|
||||
exact Eq.symm hy
|
||||
|
||||
/-- #### Exercise 5
|
||||
|
||||
If `x` is an arbitrary real number, prove that there is exactly one integer `n`
|
||||
which satisfies `x ≤ n < x + 1`.
|
||||
-/
|
||||
theorem exercise5 (x : ℝ) : ∃! n : ℤ, x ≤ n ∧ n < x + 1 := by
|
||||
let n := Int.ceil x
|
||||
refine ⟨n, ⟨?_, ?_⟩⟩
|
||||
· exact ⟨Int.le_ceil x, Int.ceil_lt_add_one x⟩
|
||||
· simp only
|
||||
intro y hy
|
||||
suffices y - 1 < x ∧ x ≤ y by
|
||||
rw [← Int.ceil_eq_iff] at this
|
||||
exact Eq.symm this
|
||||
apply And.intro
|
||||
· have := (sub_lt_sub_iff_right 1).mpr hy.right
|
||||
rwa [add_sub_cancel] at this
|
||||
· exact hy.left
|
||||
|
||||
/-! #### Exercise 6
|
||||
|
||||
If `x` and `y` are arbitrary real numbers, `x < y`, prove that there exists at
|
||||
least one rational number `r` satisfying `x < r < y`, and hence infinitely many.
|
||||
This property is often described by saying that the rational numbers are *dense*
|
||||
in the real-number system.
|
||||
|
||||
###### TODO
|
||||
-/
|
||||
|
||||
/-! #### Exercise 7
|
||||
|
||||
If `x` is rational, `x ≠ 0`, and `y` irrational, prove that `x + y`, `x - y`,
|
||||
`xy`, `x / y`, and `y / x` are all irrational.
|
||||
|
||||
###### TODO
|
||||
-/
|
||||
|
||||
/-! #### Exercise 8
|
||||
|
||||
Is the sum or product of two irrational numbers always irrational?
|
||||
|
||||
###### TODO
|
||||
-/
|
||||
|
||||
/-! #### Exercise 9
|
||||
|
||||
If `x` and `y` are arbitrary real numbers, `x < y`, prove that there exists at
|
||||
least one irrational number `z` satisfying `x < z < y`, and hence infinitely
|
||||
many.
|
||||
|
||||
###### TODO
|
||||
-/
|
||||
|
||||
/-! #### Exercise 10
|
||||
|
||||
An integer `n` is called *even* if `n = 2m` for some integer `m`, and *odd* if
|
||||
`n + 1` is even. Prove the following statements:
|
||||
|
||||
(a) An integer cannot be both even and odd.
|
||||
|
||||
(b) Every integer is either even or odd.
|
||||
|
||||
(c) The sum or product of two even integers is even. What can you say about the
|
||||
sum or product of two odd integers?
|
||||
|
||||
(d) If `n²` is even, so is `n`. If `a² = 2b²`, where `a` and `b` are integers,
|
||||
then both `a` and `b` are even.
|
||||
|
||||
(e) Every rational number can be expressed in the form `a / b`, where `a` and
|
||||
`b` are integers, at least one of which is odd.
|
||||
|
||||
###### TODO
|
||||
-/
|
||||
|
||||
|
||||
def is_even (n : ℤ) := ∃ m : ℤ, n = 2 * m
|
||||
|
||||
def is_odd (n : ℤ) := is_even (n + 1)
|
||||
|
||||
/-! #### Exercise 11
|
||||
|
||||
Prove that there is no rational number whose square is `2`.
|
||||
|
||||
[Hint: Argue by contradiction. Assume `(a / b)² = 2`, where `a` and `b` are
|
||||
integers, at least one of which is odd. Use parts of Exercise 10 to deduce a
|
||||
contradiction.]
|
||||
|
||||
###### TODO
|
||||
-/
|
||||
|
||||
/-! #### Exercise 12
|
||||
|
||||
The Archimedean property of the real-number system was deduced as a consequence
|
||||
of the least-upper-bound axiom. Prove that the set of rational numbers satisfies
|
||||
the Archimedean property but not the least-upper-bound property. This shows that
|
||||
the Archimedean property does not imply the least-upper-bound axiom.
|
||||
|
||||
###### TODO
|
||||
-/
|
||||
|
||||
end Exercises.Apostol.Chapter_I_3
|
||||
|
|
@ -1,195 +0,0 @@
|
|||
/-
|
||||
Exercises I 3.12
|
||||
|
||||
A Set of Axioms for the Real-Number System
|
||||
-/
|
||||
import Mathlib.Algebra.Order.Floor
|
||||
import Mathlib.Data.PNat.Basic
|
||||
import Mathlib.Data.Real.Basic
|
||||
import Mathlib.Data.Real.Sqrt
|
||||
import Mathlib.Tactic.LibrarySearch
|
||||
|
||||
import Bookshelf.Real.Rational
|
||||
import Exercises.Apostol.Chapter_I_3
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 1
|
||||
--
|
||||
-- If `x` and `y` are arbitrary real numbers with `x < y`, prove that there is
|
||||
-- at least one real `z` satisfying `x < z < y`.
|
||||
-- ========================================
|
||||
|
||||
theorem exercise1 (x y : ℝ) (h : x < y) : ∃ z, x < z ∧ z < y := by
|
||||
have ⟨z, hz⟩ := exists_pos_add_of_lt' h
|
||||
refine ⟨x + z / 2, ⟨?_, ?_⟩⟩
|
||||
· have hz' : z / 2 > 0 := by
|
||||
have hr := div_lt_div_of_lt (show (0 : ℝ) < 2 by simp) hz.left
|
||||
rwa [zero_div] at hr
|
||||
exact (lt_add_iff_pos_right x).mpr hz'
|
||||
· have hz' : z / 2 < z := div_lt_self hz.left (show 1 < 2 by norm_num)
|
||||
calc x + z / 2
|
||||
_ < x + z := (add_lt_add_iff_left x).mpr hz'
|
||||
_ = y := hz.right
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 2
|
||||
--
|
||||
-- If `x` is an arbitrary real number, prove that there are integers `m` and `n`
|
||||
-- such that `m < x < n`.
|
||||
-- ========================================
|
||||
|
||||
theorem exercise2 (x : ℝ) : ∃ m n : ℝ, m < x ∧ x < n := by
|
||||
refine ⟨x - 1, ⟨x + 1, ⟨?_, ?_⟩⟩⟩ <;> norm_num
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 3
|
||||
--
|
||||
-- If `x > 0`, prove that there is a positive integer `n` such that `1 / n < x`.
|
||||
-- ========================================
|
||||
|
||||
theorem exercise3 (x : ℝ) (h : x > 0) : ∃ n : ℕ+, 1 / n < x := by
|
||||
have ⟨n, hn⟩ := @Real.exists_pnat_mul_self_geq_of_pos x 1 h
|
||||
refine ⟨n, ?_⟩
|
||||
have hr := mul_lt_mul_of_pos_right hn (show 0 < 1 / ↑↑n by norm_num)
|
||||
conv at hr => arg 2; rw [mul_comm, ← mul_assoc]; simp
|
||||
rwa [one_mul] at hr
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 4
|
||||
--
|
||||
-- If `x` is an arbitrary real number, prove that there is exactly one integer
|
||||
-- `n` which satisfies the inequalities `n ≤ x < n + 1`. This `n` is called the
|
||||
-- greatest integer in `x` and is denoted by `⌊x⌋`. For example, `⌊5⌋ = 5`,
|
||||
-- `⌊5 / 2⌋ = 2`, `⌊-8/3⌋ = -3`.
|
||||
-- ========================================
|
||||
|
||||
theorem exercise4 (x : ℝ) : ∃! n : ℤ, n ≤ x ∧ x < n + 1 := by
|
||||
let n := Int.floor x
|
||||
refine ⟨n, ⟨?_, ?_⟩⟩
|
||||
· exact ⟨Int.floor_le x, Int.lt_floor_add_one x⟩
|
||||
· intro y hy
|
||||
rw [← Int.floor_eq_iff] at hy
|
||||
exact Eq.symm hy
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 5
|
||||
--
|
||||
-- If `x` is an arbitrary real number, prove that there is exactly one integer
|
||||
-- `n` which satisfies `x ≤ n < x + 1`.
|
||||
-- ========================================
|
||||
|
||||
theorem exercise5 (x : ℝ) : ∃! n : ℤ, x ≤ n ∧ n < x + 1 := by
|
||||
let n := Int.ceil x
|
||||
refine ⟨n, ⟨?_, ?_⟩⟩
|
||||
· exact ⟨Int.le_ceil x, Int.ceil_lt_add_one x⟩
|
||||
· simp only
|
||||
intro y hy
|
||||
suffices y - 1 < x ∧ x ≤ y by
|
||||
rw [← Int.ceil_eq_iff] at this
|
||||
exact Eq.symm this
|
||||
apply And.intro
|
||||
· have := (sub_lt_sub_iff_right 1).mpr hy.right
|
||||
rwa [add_sub_cancel] at this
|
||||
· exact hy.left
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 6
|
||||
--
|
||||
-- If `x` and `y` are arbitrary real numbers, `x < y`, prove that there exists
|
||||
-- at least one rational number `r` satisfying `x < r < y`, and hence infinitely
|
||||
-- many. This property is often described by saying that the rational numbers
|
||||
-- are *dense* in the real-number system.
|
||||
-- ========================================
|
||||
|
||||
-- # TODO
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 7
|
||||
--
|
||||
-- If `x` is rational, `x ≠ 0`, and `y` irrational, prove that `x + y`, `x - y`,
|
||||
-- `xy`, `x / y`, and `y / x` are all irrational.
|
||||
-- ========================================
|
||||
|
||||
-- # TODO
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 8
|
||||
--
|
||||
-- Is the sum or product of two irrational numbers always irrational?
|
||||
-- ========================================
|
||||
|
||||
-- # TODO
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 9
|
||||
--
|
||||
-- If `x` and `y` are arbitrary real numbers, `x < y`, prove that there exists
|
||||
-- at least one irrational number `z` satisfying `x < z < y`, and hence
|
||||
-- infinitely many.
|
||||
-- ========================================
|
||||
|
||||
-- # TODO
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 10
|
||||
--
|
||||
-- An integer `n` is called *even* if `n = 2m` for some integer `m`, and *odd*
|
||||
-- if `n + 1` is even. Prove the following statements:
|
||||
--
|
||||
-- (e) Every rational number can be expressed in the form `a / b`, where `a` and
|
||||
-- `b` are integers, at least one of which is odd.
|
||||
-- ========================================
|
||||
|
||||
def is_even (n : ℤ) := ∃ m : ℤ, n = 2 * m
|
||||
|
||||
def is_odd (n : ℤ) := is_even (n + 1)
|
||||
|
||||
-- ----------------------------------------
|
||||
-- (a) An integer cannot be both even and odd.
|
||||
-- ----------------------------------------
|
||||
|
||||
-- # TODO
|
||||
|
||||
-- ----------------------------------------
|
||||
-- (b) Every integer is either even or odd.
|
||||
-- ----------------------------------------
|
||||
|
||||
-- # TODO
|
||||
|
||||
-- ----------------------------------------
|
||||
-- (c) The sum or product of two even integers is even. What can you say about
|
||||
-- the sum or product of two odd integers?
|
||||
-- ----------------------------------------
|
||||
|
||||
-- # TODO
|
||||
|
||||
-- ----------------------------------------
|
||||
-- (d) If `n²` is even, so is `n`. If `a² = 2b²`, where `a` and `b` are
|
||||
-- integers, then both `a` and `b` are even.
|
||||
-- ----------------------------------------
|
||||
|
||||
-- # TODO
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 11
|
||||
--
|
||||
-- Prove that there is no rational number whose square is `2`.
|
||||
--
|
||||
-- [Hint: Argue by contradiction. Assume `(a / b)² = 2`, where `a` and `b` are
|
||||
-- integers, at least one of which is odd. Use parts of Exercise 10 to deduce a
|
||||
-- contradiction.]
|
||||
-- ========================================
|
||||
|
||||
-- # TODO
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 12
|
||||
--
|
||||
-- The Archimedean property of the real-number system was deduced as a
|
||||
-- consequence of the least-upper-bound axiom. Prove that the set of rational
|
||||
-- numbers satisfies the Archimedean property but not the least-upper-bound
|
||||
-- property. This shows that the Archimedean property does not imply the
|
||||
-- least-upper-bound axiom.
|
||||
-- ========================================
|
||||
|
||||
-- # TODO
|
||||
|
|
@ -1,4 +1,3 @@
|
|||
-- Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
|
||||
import Exercises.Avigad.Chapter2
|
||||
import Exercises.Avigad.Chapter3
|
||||
import Exercises.Avigad.Chapter4
|
||||
|
|
|
|||
|
|
@ -1,14 +1,14 @@
|
|||
/-
|
||||
Chapter 2
|
||||
/-! # Exercises.Avigad.Chapter2
|
||||
|
||||
Dependent Type Theory
|
||||
-/
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 1
|
||||
--
|
||||
-- Define the function `Do_Twice`, as described in Section 2.4.
|
||||
-- ========================================
|
||||
/-! #### Exercise 1
|
||||
|
||||
Define the function `Do_Twice`, as described in Section 2.4.
|
||||
-/
|
||||
|
||||
namespace Exercises.Avigad.Chapter2
|
||||
|
||||
namespace ex1
|
||||
|
||||
|
|
@ -20,11 +20,10 @@ def doTwiceTwice (f : (Nat → Nat) → (Nat → Nat)) (x : Nat → Nat) := f (f
|
|||
|
||||
end ex1
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 2
|
||||
--
|
||||
-- Define the functions `curry` and `uncurry`, as described in Section 2.4.
|
||||
-- ========================================
|
||||
/-! #### Exercise 2
|
||||
|
||||
Define the functions `curry` and `uncurry`, as described in Section 2.4.
|
||||
-/
|
||||
|
||||
namespace ex2
|
||||
|
||||
|
|
@ -36,17 +35,15 @@ def uncurry (f : α → β → γ) : (α × β → γ) :=
|
|||
|
||||
end ex2
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 3
|
||||
--
|
||||
-- Above, we used the example `vec α n` for vectors of elements of type `α` of
|
||||
-- length `n`. Declare a constant `vec_add` that could represent a function that
|
||||
-- adds two vectors of natural numbers of the same length, and a constant
|
||||
-- `vec_reverse` that can represent a function that reverses its argument. Use
|
||||
-- implicit arguments for parameters that can be inferred. Declare some
|
||||
-- variables and check some expressions involving the constants that you have
|
||||
-- declared.
|
||||
-- ========================================
|
||||
/-! #### Exercise 3
|
||||
|
||||
Above, we used the example `vec α n` for vectors of elements of type `α` of
|
||||
length `n`. Declare a constant `vec_add` that could represent a function that
|
||||
adds two vectors of natural numbers of the same length, and a constant
|
||||
`vec_reverse` that can represent a function that reverses its argument. Use
|
||||
implicit arguments for parameters that can be inferred. Declare some variables
|
||||
nd check some expressions involving the constants that you have declared.
|
||||
-/
|
||||
|
||||
namespace ex3
|
||||
|
||||
|
|
@ -73,16 +70,14 @@ variable (c d : vec Prop 2)
|
|||
|
||||
end ex3
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 4
|
||||
--
|
||||
-- Similarly, declare a constant `matrix` so that `matrix α m n` could represent
|
||||
-- the type of `m` by `n` matrices. Declare some constants to represent
|
||||
-- functions on this type, such as matrix addition and multiplication, and
|
||||
-- (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.
|
||||
-- ========================================
|
||||
/-! #### Exercise 4
|
||||
|
||||
Similarly, declare a constant `matrix` so that `matrix α m n` could represent
|
||||
the type of `m` by `n` matrices. Declare some constants to represent functions
|
||||
on this type, such as matrix addition and multiplication, and (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.
|
||||
-/
|
||||
|
||||
namespace ex4
|
||||
|
||||
|
|
@ -110,3 +105,5 @@ variable (d : ex3.vec Prop 3)
|
|||
#check matrix.app c d
|
||||
|
||||
end ex4
|
||||
|
||||
end Exercises.Avigad.Chapter2
|
||||
|
|
@ -1,14 +1,14 @@
|
|||
/-
|
||||
Chapter 3
|
||||
/-! # Exercises.Avigad.Chapter3
|
||||
|
||||
Propositions and Proofs
|
||||
-/
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 1
|
||||
--
|
||||
-- Prove the following identities.
|
||||
-- ========================================
|
||||
/-! #### Exercise 1
|
||||
|
||||
Prove the following identities.
|
||||
-/
|
||||
|
||||
namespace Exercises.Avigad.Chapter3
|
||||
|
||||
namespace ex1
|
||||
|
||||
|
|
@ -17,23 +17,23 @@ open or
|
|||
variable (p q r : Prop)
|
||||
|
||||
-- Commutativity of ∧ and ∨
|
||||
example : p ∧ q ↔ q ∧ p :=
|
||||
theorem and_comm' : p ∧ q ↔ q ∧ p :=
|
||||
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 :=
|
||||
theorem or_comm' : p ∨ q ↔ q ∨ p :=
|
||||
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) :=
|
||||
theorem and_assoc : (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) :=
|
||||
theorem or_assoc' : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
|
||||
Iff.intro
|
||||
(fun h₁ => h₁.elim
|
||||
(fun h₂ => h₂.elim Or.inl (Or.inr ∘ Or.inl))
|
||||
|
|
@ -43,14 +43,14 @@ example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
|
|||
(fun h₂ => h₂.elim (Or.inl ∘ Or.inr) Or.inr))
|
||||
|
||||
-- Distributivity
|
||||
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
|
||||
theorem and_or_left : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
|
||||
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) :=
|
||||
theorem or_and_left : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
|
||||
Iff.intro
|
||||
(fun h => h.elim
|
||||
(fun hp => ⟨Or.inl hp, Or.inl hp⟩)
|
||||
|
|
@ -60,12 +60,12 @@ example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
|
|||
(fun hq => h₂.elim Or.inl (fun hr => Or.inr ⟨hq, hr⟩)))
|
||||
|
||||
-- Other properties
|
||||
example : (p → (q → r)) ↔ (p ∧ q → r) :=
|
||||
theorem imp_imp_iff_and_imp : (p → (q → r)) ↔ (p ∧ q → r) :=
|
||||
Iff.intro
|
||||
(fun h ⟨hp, hq⟩ => h hp hq)
|
||||
(fun h hp hq => h ⟨hp, hq⟩)
|
||||
|
||||
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
|
||||
theorem or_imp : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
|
||||
Iff.intro
|
||||
(fun h =>
|
||||
have h₁ : p → r := h ∘ Or.inl
|
||||
|
|
@ -73,42 +73,41 @@ example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
|
|||
show (p → r) ∧ (q → r) from ⟨h₁, h₂⟩)
|
||||
(fun ⟨h₁, h₂⟩ h => h.elim h₁ h₂)
|
||||
|
||||
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
|
||||
theorem nor_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
|
||||
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) :=
|
||||
theorem not_and_or_mpr : ¬p ∨ ¬q → ¬(p ∧ q) :=
|
||||
fun h₁ h₂ => h₁.elim (absurd h₂.left ·) (absurd h₂.right ·)
|
||||
|
||||
example : ¬(p ∧ ¬p) :=
|
||||
theorem and_not_self : ¬(p ∧ ¬p) :=
|
||||
fun h => absurd h.left h.right
|
||||
|
||||
example : p ∧ ¬q → ¬(p → q) :=
|
||||
theorem not_imp_o_and_not : p ∧ ¬q → ¬(p → q) :=
|
||||
fun ⟨hp, nq⟩ hpq => absurd (hpq hp) nq
|
||||
|
||||
example : ¬p → (p → q) :=
|
||||
theorem false_elim_self : ¬p → (p → q) :=
|
||||
fun np hp => absurd hp np
|
||||
|
||||
example : (¬p ∨ q) → (p → q) :=
|
||||
theorem not_or_imp_imp : (¬p ∨ q) → (p → q) :=
|
||||
fun npq hp => npq.elim (absurd hp ·) id
|
||||
|
||||
example : p ∨ False ↔ p :=
|
||||
theorem or_false_iff : p ∨ False ↔ p :=
|
||||
Iff.intro (fun hpf => hpf.elim id False.elim) Or.inl
|
||||
|
||||
example : p ∧ False ↔ False :=
|
||||
theorem and_false_iff : p ∧ False ↔ False :=
|
||||
Iff.intro (fun ⟨_, hf⟩ => hf) False.elim
|
||||
|
||||
example : (p → q) → (¬q → ¬p) :=
|
||||
theorem imp_imp_not_imp_not : (p → q) → (¬q → ¬p) :=
|
||||
fun hpq nq hp => absurd (hpq hp) nq
|
||||
|
||||
end ex1
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 2
|
||||
--
|
||||
-- Prove the following identities. These require classical reasoning.
|
||||
-- ========================================
|
||||
/-! #### Exercise 2
|
||||
|
||||
Prove the following identities. These require classical reasoning.
|
||||
-/
|
||||
|
||||
namespace ex2
|
||||
|
||||
|
|
@ -116,34 +115,34 @@ open Classical
|
|||
|
||||
variable (p q r s : Prop)
|
||||
|
||||
example (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
|
||||
theorem imp_or_mp (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
|
||||
fun h => (h hp).elim
|
||||
(fun hr => Or.inl (fun _ => hr))
|
||||
(fun hs => Or.inr (fun _ => hs))
|
||||
|
||||
example : ¬(p ∧ q) → ¬p ∨ ¬q :=
|
||||
theorem not_and_iff_or_not : ¬(p ∧ q) → ¬p ∨ ¬q :=
|
||||
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 :=
|
||||
theorem not_imp_mp : ¬(p → q) → p ∧ ¬q :=
|
||||
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) :=
|
||||
theorem not_or_of_imp : (p → q) → (¬p ∨ q) :=
|
||||
fun hpq => (em p).elim (fun hp => Or.inr (hpq hp)) Or.inl
|
||||
|
||||
example : (¬q → ¬p) → (p → q) :=
|
||||
theorem not_imp_not_imp_imp : (¬q → ¬p) → (p → q) :=
|
||||
fun h hp => byContradiction
|
||||
fun nq => absurd hp (h nq)
|
||||
|
||||
example : p ∨ ¬p := em p
|
||||
theorem or_not : p ∨ ¬p := em p
|
||||
|
||||
example : (((p → q) → p) → p) :=
|
||||
theorem imp_imp_imp : (((p → q) → p) → p) :=
|
||||
fun h => byContradiction
|
||||
fun np =>
|
||||
suffices hp : p from absurd hp np
|
||||
|
|
@ -151,17 +150,18 @@ example : (((p → q) → p) → p) :=
|
|||
|
||||
end ex2
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 3
|
||||
--
|
||||
-- Prove `¬(p ↔ ¬p)` without using classical logic.
|
||||
-- ========================================
|
||||
/-! #### Exercise 3
|
||||
|
||||
Prove `¬(p ↔ ¬p)` without using classical logic.
|
||||
-/
|
||||
|
||||
namespace ex3
|
||||
|
||||
variable (p : Prop)
|
||||
|
||||
example (hp : p) : ¬(p ↔ ¬p) :=
|
||||
theorem iff_not_self (hp : p) : ¬(p ↔ ¬p) :=
|
||||
fun h => absurd hp (Iff.mp h hp)
|
||||
|
||||
end ex3
|
||||
|
||||
end Exercises.Avigad.Chapter3
|
||||
|
|
@ -1,32 +1,35 @@
|
|||
/-
|
||||
Chapter 4
|
||||
/-! # Exercises.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.
|
||||
-- ========================================
|
||||
/-! #### Exercise 1
|
||||
|
||||
Prove these equivalences. You should also try to understand why the reverse
|
||||
implication is not derivable in the last example.
|
||||
-/
|
||||
|
||||
namespace Exercises.Avigad.Chapter4
|
||||
|
||||
namespace ex1
|
||||
|
||||
variable (α : Type _)
|
||||
variable (p q : α → Prop)
|
||||
|
||||
example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
|
||||
theorem forall_and
|
||||
: (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q 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) :=
|
||||
theorem forall_imp_distrib
|
||||
: (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
|
||||
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 :=
|
||||
theorem forall_or_distrib
|
||||
: (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
|
||||
fun h₁ x => h₁.elim
|
||||
(fun h₂ => Or.inl (h₂ x))
|
||||
(fun h₂ => Or.inr (h₂ x))
|
||||
|
|
@ -37,13 +40,12 @@ example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
|
|||
|
||||
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).
|
||||
-- ========================================
|
||||
/-! #### 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).
|
||||
-/
|
||||
|
||||
namespace ex2
|
||||
|
||||
|
|
@ -51,14 +53,14 @@ variable (α : Type _)
|
|||
variable (p q : α → Prop)
|
||||
variable (r : Prop)
|
||||
|
||||
example : α → ((∀ _ : α, r) ↔ r) :=
|
||||
theorem self_imp_forall : α → ((∀ _ : α, r) ↔ r) :=
|
||||
fun a => Iff.intro (fun h => h a) (fun hr _ => hr)
|
||||
|
||||
section
|
||||
|
||||
open Classical
|
||||
|
||||
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
|
||||
theorem forall_or_right : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
|
||||
Iff.intro
|
||||
(fun h₁ => (em r).elim
|
||||
Or.inr
|
||||
|
|
@ -69,20 +71,19 @@ example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
|
|||
|
||||
end
|
||||
|
||||
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
|
||||
theorem forall_swap : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
|
||||
Iff.intro
|
||||
(fun h hr hx => h hx hr)
|
||||
(fun h hx hr => h hr hx)
|
||||
|
||||
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.
|
||||
-- ========================================
|
||||
/-! #### 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.
|
||||
-/
|
||||
|
||||
namespace ex3
|
||||
|
||||
|
|
@ -92,7 +93,7 @@ variable (men : Type _)
|
|||
variable (barber : men)
|
||||
variable (shaves : men → men → Prop)
|
||||
|
||||
example (h : ∀ x : men, shaves barber x ↔ ¬shaves x x) : False :=
|
||||
theorem barber_paradox (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'))
|
||||
|
|
@ -100,18 +101,16 @@ example (h : ∀ x : men, shaves barber x ↔ ¬shaves x x) : False :=
|
|||
|
||||
end ex3
|
||||
|
||||
-- ========================================
|
||||
-- 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.
|
||||
-- ========================================
|
||||
/-! #### 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.
|
||||
-/
|
||||
|
||||
namespace ex4
|
||||
|
||||
|
|
@ -144,11 +143,10 @@ def Fermat'sLastTheorem : Prop :=
|
|||
|
||||
end ex4
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 5
|
||||
--
|
||||
-- Prove as many of the identities listed in Section 4.4 as you can.
|
||||
-- ========================================
|
||||
/-! #### Exercise 5
|
||||
|
||||
Prove as many of the identities listed in Section 4.4 as you can.
|
||||
-/
|
||||
|
||||
namespace ex5
|
||||
|
||||
|
|
@ -158,18 +156,18 @@ variable (α : Type _)
|
|||
variable (p q : α → Prop)
|
||||
variable (r s : Prop)
|
||||
|
||||
example : (∃ _ : α, r) → r :=
|
||||
theorem exists_imp : (∃ _ : α, r) → r :=
|
||||
fun ⟨_, hr⟩ => hr
|
||||
|
||||
example (a : α) : r → (∃ _ : α, r) :=
|
||||
theorem exists_intro (a : α) : r → (∃ _ : α, r) :=
|
||||
fun hr => ⟨a, hr⟩
|
||||
|
||||
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
|
||||
theorem exists_and_right : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
|
||||
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) :=
|
||||
theorem exists_or : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
|
||||
Iff.intro
|
||||
(fun ⟨hx, hpq⟩ => hpq.elim
|
||||
(fun hp => Or.inl ⟨hx, hp⟩)
|
||||
|
|
@ -178,19 +176,19 @@ example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
|
|||
(fun ⟨hx, hp⟩ => ⟨hx, Or.inl hp⟩)
|
||||
(fun ⟨hx, hq⟩ => ⟨hx, Or.inr hq⟩))
|
||||
|
||||
example : (∀ x, p x) ↔ ¬(∃ x, ¬p x) :=
|
||||
theorem forall_iff_not_exists : (∀ 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) :=
|
||||
theorem exists_iff_not_forall : (∃ 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) :=
|
||||
theorem not_exists : (¬∃ x, p x) ↔ (∀ x, ¬p x) :=
|
||||
Iff.intro
|
||||
(fun h hx hp => h ⟨hx, hp⟩)
|
||||
(fun h ⟨hx, hp⟩ => absurd hp (h hx))
|
||||
|
|
@ -202,15 +200,15 @@ theorem forall_negation : (¬∀ x, p x) ↔ (∃ x, ¬p x) :=
|
|||
fun np => h' ⟨x, np⟩))
|
||||
(fun ⟨hx, np⟩ h => absurd (h hx) np)
|
||||
|
||||
example : (¬∀ x, p x) ↔ (∃ x, ¬p x) :=
|
||||
theorem not_forall : (¬∀ x, p x) ↔ (∃ x, ¬p x) :=
|
||||
forall_negation α p
|
||||
|
||||
example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
|
||||
theorem forall_iff_exists_imp : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
|
||||
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 :=
|
||||
theorem exists_iff_forall_imp (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
|
||||
Iff.intro
|
||||
(fun ⟨hx, hp⟩ h => hp (h hx))
|
||||
(fun h₁ => (em (∀ x, p x)).elim
|
||||
|
|
@ -220,7 +218,7 @@ example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
|
|||
match h₃ with
|
||||
| ⟨hx, hp⟩ => ⟨hx, fun hp' => absurd hp' hp⟩))
|
||||
|
||||
example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
|
||||
theorem exists_self_iff_self_exists (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
|
||||
Iff.intro
|
||||
(fun ⟨hx, hrp⟩ hr => ⟨hx, hrp hr⟩)
|
||||
(fun h => (em r).elim
|
||||
|
|
@ -230,11 +228,10 @@ example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
|
|||
|
||||
end ex5
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 6
|
||||
--
|
||||
-- Give a calculational proof of the theorem `log_mul` below.
|
||||
-- ========================================
|
||||
/-! #### Exercise 6
|
||||
|
||||
Give a calculational proof of the theorem `log_mul` below.
|
||||
-/
|
||||
|
||||
namespace ex6
|
||||
|
||||
|
|
@ -244,16 +241,21 @@ 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)
|
||||
|
||||
example (x y z : Float) : exp (x + y + z) = exp x * exp y * exp z :=
|
||||
theorem exp_add_mul_exp (x y z : Float)
|
||||
: 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
|
||||
theorem exp_log_eq_self (y : Float) (h : y > 0)
|
||||
: exp (log y) = y := exp_log_eq h
|
||||
|
||||
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 ex6
|
||||
|
||||
end Exercises.Avigad.Chapter4
|
||||
|
|
@ -1,35 +1,33 @@
|
|||
/-
|
||||
Chapter 5
|
||||
/-! # Exercises.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.
|
||||
-- ========================================
|
||||
/-! #### 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
|
||||
|
||||
namespace ex1
|
||||
|
||||
-- ----------------------------------------
|
||||
-- Exercises 3.1
|
||||
-- ----------------------------------------
|
||||
/-! ##### Exercises 3.1 -/
|
||||
|
||||
section ex3_1
|
||||
|
||||
variable (p q r : Prop)
|
||||
|
||||
-- Commutativity of ∧ and ∨
|
||||
example : p ∧ q ↔ q ∧ p := by
|
||||
theorem and_comm' : 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 := by
|
||||
theorem or_comm' : p ∨ q ↔ q ∨ p := by
|
||||
apply Iff.intro
|
||||
· intro
|
||||
| Or.inl hp => exact Or.inr hp
|
||||
|
|
@ -39,14 +37,14 @@ example : p ∨ q ↔ q ∨ p := by
|
|||
| Or.inr hp => exact Or.inl hp
|
||||
|
||||
-- Associativity of ∧ and ∨
|
||||
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := by
|
||||
theorem and_assoc : (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) := by
|
||||
theorem or_assoc' : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
|
||||
apply Iff.intro
|
||||
· intro
|
||||
| Or.inl (Or.inl hp) => exact Or.inl hp
|
||||
|
|
@ -58,7 +56,7 @@ example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
|
|||
| Or.inr (Or.inr hr) => exact Or.inr hr
|
||||
|
||||
-- Distributivity
|
||||
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
|
||||
theorem and_or_left : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
|
||||
apply Iff.intro
|
||||
· intro
|
||||
| ⟨hp, Or.inl hq⟩ => exact Or.inl ⟨hp, hq⟩
|
||||
|
|
@ -67,7 +65,7 @@ example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
|
|||
| 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) := by
|
||||
theorem or_and_left : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by
|
||||
apply Iff.intro
|
||||
· intro
|
||||
| Or.inl hp => exact ⟨Or.inl hp, Or.inl hp⟩
|
||||
|
|
@ -78,14 +76,14 @@ example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by
|
|||
| ⟨Or.inr hq, Or.inr hr⟩ => exact Or.inr ⟨hq, hr⟩
|
||||
|
||||
-- Other properties
|
||||
example : (p → (q → r)) ↔ (p ∧ q → r) := by
|
||||
theorem imp_imp_iff_and_imp : (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) := by
|
||||
theorem or_imp : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := by
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
apply And.intro
|
||||
|
|
@ -100,7 +98,7 @@ example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := by
|
|||
· intro hq
|
||||
exact hqr hq
|
||||
|
||||
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by
|
||||
theorem nor_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
apply And.intro
|
||||
|
|
@ -113,29 +111,29 @@ example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by
|
|||
| Or.inl hp => exact absurd hp np
|
||||
| Or.inr hq => exact absurd hq nq
|
||||
|
||||
example : ¬p ∨ ¬q → ¬(p ∧ q) := by
|
||||
theorem not_and_or_mpr : ¬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) := by
|
||||
theorem and_not_self : ¬(p ∧ ¬p) := by
|
||||
intro ⟨hp, np⟩
|
||||
exact absurd hp np
|
||||
|
||||
example : p ∧ ¬q → ¬(p → q) := by
|
||||
theorem not_imp_o_and_not : p ∧ ¬q → ¬(p → q) := by
|
||||
intro ⟨hp, nq⟩ h
|
||||
exact absurd (h hp) nq
|
||||
|
||||
example : ¬p → (p → q) := by
|
||||
theorem false_elim_self : ¬p → (p → q) := by
|
||||
intro np hp
|
||||
exact absurd hp np
|
||||
|
||||
example : (¬p ∨ q) → (p → q) := by
|
||||
theorem not_or_imp_imp : (¬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 := by
|
||||
theorem or_false_iff : p ∨ False ↔ p := by
|
||||
apply Iff.intro
|
||||
· intro
|
||||
| Or.inl hp => exact hp
|
||||
|
|
@ -143,22 +141,20 @@ example : p ∨ False ↔ p := by
|
|||
· intro hp
|
||||
exact Or.inl hp
|
||||
|
||||
example : p ∧ False ↔ False := by
|
||||
theorem and_false_iff : p ∧ False ↔ False := by
|
||||
apply Iff.intro
|
||||
· intro ⟨_, ff⟩
|
||||
exact ff
|
||||
· intro ff
|
||||
exact False.elim ff
|
||||
|
||||
example : (p → q) → (¬q → ¬p) := by
|
||||
theorem imp_imp_not_imp_not : (p → q) → (¬q → ¬p) := by
|
||||
intro hpq nq hp
|
||||
exact absurd (hpq hp) nq
|
||||
|
||||
end ex3_1
|
||||
|
||||
-- ----------------------------------------
|
||||
-- Exercises 3.2
|
||||
-- ----------------------------------------
|
||||
/-! ##### Exercises 3.2 -/
|
||||
|
||||
section ex3_2
|
||||
|
||||
|
|
@ -166,7 +162,7 @@ open Classical
|
|||
|
||||
variable (p q r s : Prop)
|
||||
|
||||
example (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) := by
|
||||
theorem imp_or_mp (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) := by
|
||||
intro h
|
||||
apply (h hp).elim
|
||||
· intro hr
|
||||
|
|
@ -174,7 +170,7 @@ example (hp : p) : (p → r ∨ s) → ((p → r) ∨ (p → s)) := by
|
|||
· intro hs
|
||||
exact Or.inr (fun _ => hs)
|
||||
|
||||
example : ¬(p ∧ q) → ¬p ∨ ¬q := by
|
||||
theorem not_and_iff_or_not : ¬(p ∧ q) → ¬p ∨ ¬q := by
|
||||
intro h
|
||||
apply (em p).elim
|
||||
· intro hp
|
||||
|
|
@ -186,7 +182,7 @@ example : ¬(p ∧ q) → ¬p ∨ ¬q := by
|
|||
· intro np
|
||||
exact Or.inl np
|
||||
|
||||
example : ¬(p → q) → p ∧ ¬q := by
|
||||
theorem not_imp_mp : ¬(p → q) → p ∧ ¬q := by
|
||||
intro h
|
||||
apply And.intro
|
||||
· apply byContradiction
|
||||
|
|
@ -199,7 +195,7 @@ example : ¬(p → q) → p ∧ ¬q := by
|
|||
intro _
|
||||
exact hq
|
||||
|
||||
example : (p → q) → (¬p ∨ q) := by
|
||||
theorem not_or_of_imp : (p → q) → (¬p ∨ q) := by
|
||||
intro hpq
|
||||
apply (em p).elim
|
||||
· intro hp
|
||||
|
|
@ -207,15 +203,15 @@ example : (p → q) → (¬p ∨ q) := by
|
|||
· intro np
|
||||
exact Or.inl np
|
||||
|
||||
example : (¬q → ¬p) → (p → q) := by
|
||||
theorem not_imp_not_imp_imp : (¬q → ¬p) → (p → q) := by
|
||||
intro hqp hp
|
||||
apply byContradiction
|
||||
intro nq
|
||||
exact absurd hp (hqp nq)
|
||||
|
||||
example : p ∨ ¬p := by apply em
|
||||
theorem or_not : p ∨ ¬p := by apply em
|
||||
|
||||
example : (((p → q) → p) → p) := by
|
||||
theorem imp_imp_imp : (((p → q) → p) → p) := by
|
||||
intro h
|
||||
apply (em p).elim
|
||||
· intro hp
|
||||
|
|
@ -227,30 +223,26 @@ example : (((p → q) → p) → p) := by
|
|||
|
||||
end ex3_2
|
||||
|
||||
-- ----------------------------------------
|
||||
-- Exercises 3.3
|
||||
-- ----------------------------------------
|
||||
/-! ##### Exercises 3.3 -/
|
||||
|
||||
section ex3_3
|
||||
|
||||
variable (p : Prop)
|
||||
|
||||
example (hp : p) : ¬(p ↔ ¬p) := by
|
||||
theorem iff_not_self (hp : p) : ¬(p ↔ ¬p) := by
|
||||
intro h
|
||||
exact absurd hp (h.mp hp)
|
||||
|
||||
end ex3_3
|
||||
|
||||
-- ----------------------------------------
|
||||
-- Exercises 4.1
|
||||
-- ----------------------------------------
|
||||
/-! ##### Exercises 4.1 -/
|
||||
|
||||
section ex4_1
|
||||
|
||||
variable (α : Type _)
|
||||
variable (p q : α → Prop)
|
||||
|
||||
example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := by
|
||||
theorem forall_and : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := by
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
apply And.intro
|
||||
|
|
@ -261,20 +253,18 @@ example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := by
|
|||
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
|
||||
theorem forall_imp_distrib : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) := by
|
||||
intro h₁ h₂ hx
|
||||
exact h₁ hx (h₂ hx)
|
||||
|
||||
example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := by
|
||||
theorem forall_or_distrib : (∀ 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 ex4_1
|
||||
|
||||
-- ----------------------------------------
|
||||
-- Exercises 4.2
|
||||
-- ----------------------------------------
|
||||
/-! ##### Exercises 4.2 -/
|
||||
|
||||
section ex4_2
|
||||
|
||||
|
|
@ -282,7 +272,7 @@ variable (α : Type _)
|
|||
variable (p q : α → Prop)
|
||||
variable (r : Prop)
|
||||
|
||||
example : α → ((∀ _ : α, r) ↔ r) := by
|
||||
theorem self_imp_forall : α → ((∀ _ : α, r) ↔ r) := by
|
||||
intro ha
|
||||
apply Iff.intro
|
||||
· intro har
|
||||
|
|
@ -295,7 +285,7 @@ section
|
|||
|
||||
open Classical
|
||||
|
||||
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := by
|
||||
theorem forall_or_right : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := by
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
apply (em r).elim
|
||||
|
|
@ -317,7 +307,7 @@ example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := by
|
|||
|
||||
end
|
||||
|
||||
example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := by
|
||||
theorem forall_swap : (∀ x, r → p x) ↔ (r → ∀ x, p x) := by
|
||||
apply Iff.intro
|
||||
· intro h hr hx
|
||||
exact h hx hr
|
||||
|
|
@ -326,9 +316,7 @@ example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := by
|
|||
|
||||
end ex4_2
|
||||
|
||||
-- ----------------------------------------
|
||||
-- Exercises 4.3
|
||||
-- ----------------------------------------
|
||||
/-! ##### Exercises 4.3 -/
|
||||
|
||||
section ex4_3
|
||||
|
||||
|
|
@ -338,7 +326,8 @@ variable (men : Type _)
|
|||
variable (barber : men)
|
||||
variable (shaves : men → men → Prop)
|
||||
|
||||
example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := by
|
||||
theorem barber_paradox (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)
|
||||
|
|
@ -347,9 +336,7 @@ example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := by
|
|||
|
||||
end ex4_3
|
||||
|
||||
-- ----------------------------------------
|
||||
-- Exercises 4.5
|
||||
-- ----------------------------------------
|
||||
/-! ##### Exercises 4.5 -/
|
||||
|
||||
section ex4_5
|
||||
|
||||
|
|
@ -359,22 +346,22 @@ variable (α : Type _)
|
|||
variable (p q : α → Prop)
|
||||
variable (r s : Prop)
|
||||
|
||||
example : (∃ _ : α, r) → r := by
|
||||
theorem exists_imp : (∃ _ : α, r) → r := by
|
||||
intro ⟨_, hr⟩
|
||||
exact hr
|
||||
|
||||
example (a : α) : r → (∃ _ : α, r) := by
|
||||
theorem exists_intro (a : α) : r → (∃ _ : α, r) := by
|
||||
intro hr
|
||||
exact ⟨a, hr⟩
|
||||
|
||||
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r := by
|
||||
theorem exists_and_right : (∃ 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) := by
|
||||
theorem exists_or : (∃ 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⟩
|
||||
|
|
@ -383,7 +370,7 @@ example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) := by
|
|||
| 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) := by
|
||||
theorem forall_iff_not_exists : (∀ x, p x) ↔ ¬(∃ x, ¬p x) := by
|
||||
apply Iff.intro
|
||||
· intro ha ⟨hx, np⟩
|
||||
exact absurd (ha hx) np
|
||||
|
|
@ -392,7 +379,7 @@ example : (∀ x, p x) ↔ ¬(∃ x, ¬p x) := by
|
|||
intro np
|
||||
exact he ⟨hx, np⟩
|
||||
|
||||
example : (∃ x, p x) ↔ ¬(∀ x, ¬p x) := by
|
||||
theorem exists_iff_not_forall : (∃ x, p x) ↔ ¬(∀ x, ¬p x) := by
|
||||
apply Iff.intro
|
||||
· intro ⟨hx, hp⟩ h
|
||||
exact absurd hp (h hx)
|
||||
|
|
@ -403,7 +390,7 @@ example : (∃ x, p x) ↔ ¬(∀ x, ¬p x) := by
|
|||
intro hx hp
|
||||
exact h₂ ⟨hx, hp⟩
|
||||
|
||||
example : (¬∃ x, p x) ↔ (∀ x, ¬p x) := by
|
||||
theorem not_exists : (¬∃ x, p x) ↔ (∀ x, ¬p x) := by
|
||||
apply Iff.intro
|
||||
· intro h hx hp
|
||||
exact h ⟨hx, hp⟩
|
||||
|
|
@ -422,16 +409,16 @@ theorem forall_negation : (¬∀ x, p x) ↔ (∃ x, ¬p x) := by
|
|||
· intro ⟨hx, np⟩ h
|
||||
exact absurd (h hx) np
|
||||
|
||||
example : (¬∀ x, p x) ↔ (∃ x, ¬p x) := forall_negation α p
|
||||
theorem not_forall : (¬∀ x, p x) ↔ (∃ x, ¬p x) := forall_negation α p
|
||||
|
||||
example : (∀ x, p x → r) ↔ (∃ x, p x) → r := by
|
||||
theorem forall_iff_exists_imp : (∀ 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
|
||||
theorem exists_iff_forall_imp (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r := by
|
||||
apply Iff.intro
|
||||
· intro ⟨hx, hp⟩ h
|
||||
apply hp
|
||||
|
|
@ -444,7 +431,8 @@ example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r := by
|
|||
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
|
||||
theorem exists_self_iff_self_exists (a : α)
|
||||
: (∃ x, r → p x) ↔ (r → ∃ x, p x) := by
|
||||
apply Iff.intro
|
||||
· intro ⟨hx, h⟩ hr
|
||||
exact ⟨hx, h hr⟩
|
||||
|
|
@ -460,15 +448,17 @@ end ex4_5
|
|||
|
||||
end ex1
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 2
|
||||
--
|
||||
-- Use tactic combinators to obtain a one line proof of the following:
|
||||
-- ========================================
|
||||
/-! #### Exercise 2
|
||||
|
||||
Use tactic combinators to obtain a one line proof of the following:
|
||||
-/
|
||||
|
||||
namespace ex2
|
||||
|
||||
example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) :=
|
||||
by simp [*]
|
||||
theorem or_and_or_and_or (p q r : Prop) (hp : p)
|
||||
: (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := by
|
||||
simp [*]
|
||||
|
||||
end ex2
|
||||
|
||||
end Exercises.Avigad.Chapter5
|
||||
|
|
@ -1,22 +1,22 @@
|
|||
/-
|
||||
Chapter 7
|
||||
/-! # Exercises.Avigad.Chapter7
|
||||
|
||||
Inductive Types
|
||||
-/
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 1
|
||||
--
|
||||
-- Try defining other operations on the natural numbers, such as multiplication,
|
||||
-- the predecessor function (with `pred 0 = 0`), truncated subtraction (with
|
||||
-- `n - m = 0` when `m` is greater than or equal to `n`), and exponentiation.
|
||||
-- Then try proving some of their basic properties, building on the theorems we
|
||||
-- have already proved.
|
||||
--
|
||||
-- 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 Exercises.Avigad.Chapter7
|
||||
|
||||
/-! #### Exercise 1
|
||||
|
||||
Try defining other operations on the natural numbers, such as multiplication,
|
||||
the predecessor function (with `pred 0 = 0`), truncated subtraction (with
|
||||
`n - m = 0` when `m` is greater than or equal to `n`), and exponentiation. Then
|
||||
try proving some of their basic properties, building on the theorems we have
|
||||
already proved.
|
||||
|
||||
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 ex1
|
||||
|
||||
|
|
@ -77,16 +77,17 @@ end Nat
|
|||
|
||||
end ex1
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 2
|
||||
--
|
||||
-- Define some operations on lists, like a `length` function or the `reverse`
|
||||
-- function. Prove some properties, such as the following:
|
||||
--
|
||||
-- a. `length (s ++ t) = length s + length t`
|
||||
-- b. `length (reverse t) = length t`
|
||||
-- c. `reverse (reverse t) = t`
|
||||
-- ========================================
|
||||
/-! #### Exercise 2
|
||||
|
||||
Define some operations on lists, like a `length` function or the `reverse`
|
||||
function. Prove some properties, such as the following:
|
||||
|
||||
a. `length (s ++ t) = length s + length t`
|
||||
|
||||
b. `length (reverse t) = length t`
|
||||
|
||||
c. `reverse (reverse t) = t`
|
||||
-/
|
||||
|
||||
namespace ex2
|
||||
|
||||
|
|
@ -177,20 +178,22 @@ theorem reverse_reverse (t : List α)
|
|||
|
||||
end ex2
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 3
|
||||
--
|
||||
-- Define an inductive data type consisting of terms built up from the following
|
||||
-- constructors:
|
||||
--
|
||||
-- • `const n`, a constant denoting the natural number `n`
|
||||
-- • `var n`, a variable, numbered `n`
|
||||
-- • `plus s t`, denoting the sum of `s` and `t`
|
||||
-- • `times s t`, denoting the product of `s` and `t`
|
||||
--
|
||||
-- Recursively define a function that evaluates any such term with respect to an
|
||||
-- assignment of values to the variables.
|
||||
-- ========================================
|
||||
/-! #### Exercise 3
|
||||
|
||||
Define an inductive data type consisting of terms built up from the following
|
||||
constructors:
|
||||
|
||||
• `const n`, a constant denoting the natural number `n`
|
||||
|
||||
• `var n`, a variable, numbered `n`
|
||||
|
||||
• `plus s t`, denoting the sum of `s` and `t`
|
||||
|
||||
• `times s t`, denoting the product of `s` and `t`
|
||||
|
||||
Recursively define a function that evaluates any such term with respect to an
|
||||
assignment of values to the variables.
|
||||
-/
|
||||
|
||||
namespace ex3
|
||||
|
||||
|
|
@ -213,3 +216,5 @@ def eval_foo : Foo → List Nat → Nat
|
|||
| (Foo.times m n), vs => eval_foo m vs * eval_foo n vs
|
||||
|
||||
end ex3
|
||||
|
||||
end Exercises.Avigad.Chapter7
|
||||
|
|
@ -1,17 +1,17 @@
|
|||
/-
|
||||
Chapter 8
|
||||
/-! # Exercises.Avigad.Chapter8
|
||||
|
||||
Induction and Recursion
|
||||
-/
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 1
|
||||
--
|
||||
-- Open a namespace `Hidden` to avoid naming conflicts, and use the equation
|
||||
-- compiler to define addition, multiplication, and exponentiation on the
|
||||
-- natural numbers. Then use the equation compiler to derive some of their basic
|
||||
-- properties.
|
||||
-- ========================================
|
||||
namespace Exercises.Avigad.Chapter8
|
||||
|
||||
/-! #### Exercise 1
|
||||
|
||||
Open a namespace `Hidden` to avoid naming conflicts, and use the equation
|
||||
compiler to define addition, multiplication, and exponentiation on the natural
|
||||
numbers. Then use the equation compiler to derive some of their basic
|
||||
properties.
|
||||
-/
|
||||
|
||||
namespace ex1
|
||||
|
||||
|
|
@ -29,13 +29,12 @@ def exp : Nat → Nat → Nat
|
|||
|
||||
end ex1
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 2
|
||||
--
|
||||
-- Similarly, use the equation compiler to define some basic operations on lists
|
||||
-- (like the reverse function) and prove theorems about lists by induction (such
|
||||
-- as the fact that `reverse (reverse xs) = xs` for any list `xs`).
|
||||
-- ========================================
|
||||
/-! #### Exercise 2
|
||||
|
||||
Similarly, use the equation compiler to define some basic operations on lists
|
||||
(like the reverse function) and prove theorems about lists by induction (such as
|
||||
the fact that `reverse (reverse xs) = xs` for any list `xs`).
|
||||
-/
|
||||
|
||||
namespace ex2
|
||||
|
||||
|
|
@ -49,13 +48,12 @@ def reverse : List α → List α
|
|||
|
||||
end ex2
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 3
|
||||
--
|
||||
-- Define your own function to carry out course-of-value recursion on the
|
||||
-- natural numbers. Similarly, see if you can figure out how to define
|
||||
-- `WellFounded.fix` on your own.
|
||||
-- ========================================
|
||||
/-! #### Exercise 3
|
||||
|
||||
Define your own function to carry out course-of-value recursion on the natural
|
||||
numbers. Similarly, see if you can figure out how to define `WellFounded.fix` on
|
||||
your own.
|
||||
-/
|
||||
|
||||
namespace ex3
|
||||
|
||||
|
|
@ -88,13 +86,12 @@ noncomputable def brecOn {motive : Nat → Sort u}
|
|||
|
||||
end ex3
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 4
|
||||
--
|
||||
-- Following the examples in Section Dependent Pattern Matching, define a
|
||||
-- function that will append two vectors. This is tricky; you will have to
|
||||
-- define an auxiliary function.
|
||||
-- ========================================
|
||||
/-! #### Exercise 4
|
||||
|
||||
Following the examples in Section Dependent Pattern Matching, define a function
|
||||
that will append two vectors. This is tricky; you will have to define an
|
||||
auxiliary function.
|
||||
-/
|
||||
|
||||
namespace ex4
|
||||
|
||||
|
|
@ -116,11 +113,10 @@ end Vector
|
|||
|
||||
end ex4
|
||||
|
||||
-- ========================================
|
||||
-- Exercise 5
|
||||
--
|
||||
-- Consider the following type of arithmetic expressions. The ideSure, looks like RDS w
|
||||
-- ========================================
|
||||
/-! #### Exercise 5
|
||||
|
||||
Consider the following type of arithmetic expressions.
|
||||
-/
|
||||
|
||||
namespace ex5
|
||||
|
||||
|
|
@ -153,12 +149,13 @@ def sampleVal : Nat → Nat
|
|||
-- Try it out. You should get 47 here.
|
||||
#eval eval sampleVal sampleExpr
|
||||
|
||||
-- ----------------------------------------
|
||||
-- Implement "constant fusion," a procedure that simplifies subterms like
|
||||
-- `5 + 7` to `12`. Using the auxiliary function `simpConst`, define a function
|
||||
-- "fuse": to simplify a plus or a times, first simplify the arguments
|
||||
-- recursively, and then apply `simpConst` to try to simplify the result.
|
||||
-- ----------------------------------------
|
||||
/-! ##### Constant Fusion
|
||||
|
||||
Implement "constant fusion," a procedure that simplifies subterms like `5 + 7
|
||||
to `12`. Using the auxiliary function `simpConst`, define a function "fuse": to
|
||||
simplify a plus or a times, first simplify the arguments recursively, and then
|
||||
apply `simpConst` to try to simplify the result.
|
||||
-/
|
||||
|
||||
def simpConst : Expr → Expr
|
||||
| plus (const n₁) (const n₂) => const (n₁ + n₂)
|
||||
|
|
@ -208,3 +205,5 @@ theorem fuse_eq (v : Nat → Nat)
|
|||
-- The last two theorems show that the definitions preserve the value.
|
||||
|
||||
end ex5
|
||||
|
||||
end Exercises.Avigad.Chapter8
|
||||
|
|
@ -1,3 +1 @@
|
|||
-- Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
|
||||
-- Harcourt/Academic Press, 2001.
|
||||
import Exercises.Enderton.Chapter0
|
||||
|
|
@ -1,10 +1,11 @@
|
|||
/-
|
||||
Chapter 0
|
||||
import Bookshelf.LTuple.Basic
|
||||
|
||||
/-! # Exercises.Enderton.Chapter0
|
||||
|
||||
Useful Facts About Sets
|
||||
-/
|
||||
|
||||
import Bookshelf.LTuple.Basic
|
||||
namespace Exercises.Enderton.Chapter0
|
||||
|
||||
/--
|
||||
The following describes a so-called "generic" tuple. Like an `LTuple`, a generic
|
||||
|
|
@ -45,9 +46,7 @@ namespace GTuple
|
|||
|
||||
open scoped LTuple
|
||||
|
||||
-- ========================================
|
||||
-- Normalization
|
||||
-- ========================================
|
||||
/-! ## Normalization -/
|
||||
|
||||
/--
|
||||
Converts an `GTuple` into "normal form".
|
||||
|
|
@ -104,9 +103,7 @@ theorem norm_snoc_eq_concat {t₁ : GTuple α (p, q)} {t₂ : LTuple α n}
|
|||
: norm (snoc t₁ t₂) = LTuple.concat t₁.norm t₂ := by
|
||||
conv => lhs; unfold norm
|
||||
|
||||
-- ========================================
|
||||
-- Equality
|
||||
-- ========================================
|
||||
/-! ## Equality -/
|
||||
|
||||
/--
|
||||
Implements Boolean equality for `GTuple α n` provided `α` has decidable
|
||||
|
|
@ -115,9 +112,7 @@ equality.
|
|||
instance BEq [DecidableEq α] : BEq (GTuple α n) where
|
||||
beq t₁ t₂ := t₁.norm == t₂.norm
|
||||
|
||||
-- ========================================
|
||||
-- Basic API
|
||||
-- ========================================
|
||||
/-! ## Basic API -/
|
||||
|
||||
/--
|
||||
Returns the number of entries in the `GTuple`.
|
||||
|
|
@ -176,12 +171,7 @@ def snd : GTuple α (m, n) → LTuple α n
|
|||
|
||||
end GTuple
|
||||
|
||||
-- ========================================
|
||||
-- Lemma 0A
|
||||
--
|
||||
-- Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Then
|
||||
-- `x₁ = ⟨y₁, ..., yₖ₊₁⟩`.
|
||||
-- ========================================
|
||||
/-! ## Lemma 0A -/
|
||||
|
||||
section
|
||||
|
||||
|
|
@ -238,8 +228,7 @@ private def cast_fst : GTuple α (n, m - 1) → LTuple α (k + 1)
|
|||
private def cast_take (ys : LTuple α (m + k)) :=
|
||||
cast (by rw [min_comm_succ_eq p]) (ys.take (k + 1))
|
||||
|
||||
/--
|
||||
Lemma 0A
|
||||
/-- #### Lemma 0A
|
||||
|
||||
Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Then
|
||||
`x₁ = ⟨y₁, ..., yₖ₊₁⟩`.
|
||||
|
|
@ -284,4 +273,6 @@ theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k))
|
|||
(show LTuple α (min (n + (m - 1)) n) = LTuple α n by simp)
|
||||
h₂
|
||||
|
||||
end
|
||||
end
|
||||
|
||||
end Exercises.Enderton.Chapter0
|
||||
|
|
@ -1,2 +1 @@
|
|||
-- Fraleigh, John B. A First Course in Abstract Algebra, n.d.
|
||||
import Exercises.Fraleigh.Chapter1
|
||||
|
|
@ -1,18 +1,24 @@
|
|||
/-
|
||||
Chapter 1
|
||||
import Mathlib.Data.Complex.Basic
|
||||
|
||||
/-! # Exercises.Fraleign.Chapter1
|
||||
|
||||
Introduction and Examples
|
||||
-/
|
||||
|
||||
import Mathlib.Data.Complex.Basic
|
||||
namespace Exercises.Fraleign.Chapter1
|
||||
|
||||
open Complex
|
||||
open HPow
|
||||
|
||||
-- In Exercises 1 through 9 compute the given arithmetic expression and give the
|
||||
-- answer in the form $a + bi$ for $a, b ∈ ℝ$.
|
||||
/-! ## Exercises 1 Through 9
|
||||
|
||||
theorem ex1_1 : I^3 = 0 + (-1) * I := calc
|
||||
In Exercises 1 through 9 compute the given arithmetic expression and give the
|
||||
answer in the form `a + bi` for `a, b ∈ ℝ`.
|
||||
-/
|
||||
|
||||
theorem exercise1 : I^3 = 0 + (-1) * I := calc
|
||||
I^3
|
||||
= I * (I * hPow I 1) := rfl
|
||||
_ = 0 + (-1) * I := by simp
|
||||
|
||||
end Exercises.Fraleign.Chapter1
|
||||
Loading…
Reference in New Issue