From 4b32563cee5d775f9c9c32f24ba9dd5414824ef2 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 4 May 2023 16:37:54 -0600 Subject: [PATCH] Add documentation throughout modules. --- Bookshelf/Combinator/Aviary.lean | 83 +++++---- Bookshelf/LTuple/Basic.lean | 120 +++++++------ Bookshelf/List/Basic.lean | 83 +++++---- Bookshelf/Real/Basic.lean | 18 +- Bookshelf/Real/Function/Step.lean | 5 + Bookshelf/Real/Geometry/Area.lean | 9 + Bookshelf/Real/Geometry/Basic.lean | 21 ++- Bookshelf/Real/Geometry/Rectangle.lean | 16 ++ Bookshelf/Real/Rational.lean | 10 +- Bookshelf/Real/Sequence/Arithmetic.lean | 6 + Bookshelf/Real/Sequence/Geometric.lean | 6 + Bookshelf/Real/Set/Basic.lean | 7 +- Bookshelf/Real/Set/Interval.lean | 6 + Bookshelf/Real/Set/Partition.lean | 12 +- Exercises/Apostol.lean | 3 - Exercises/Apostol/Chapter_I_3.lean | 218 +++++++++++++++++++----- Exercises/Apostol/Exercises_I_3_12.lean | 195 --------------------- Exercises/Avigad.lean | 1 - Exercises/Avigad/Chapter2.lean | 63 ++++--- Exercises/Avigad/Chapter3.lean | 84 ++++----- Exercises/Avigad/Chapter4.lean | 138 +++++++-------- Exercises/Avigad/Chapter5.lean | 148 ++++++++-------- Exercises/Avigad/Chapter7.lean | 83 ++++----- Exercises/Avigad/Chapter8.lean | 83 +++++---- Exercises/Enderton.lean | 2 - Exercises/Enderton/Chapter0.lean | 33 ++-- Exercises/Fraleigh.lean | 1 - Exercises/Fraleigh/Chapter1.lean | 18 +- 28 files changed, 754 insertions(+), 718 deletions(-) delete mode 100644 Exercises/Apostol/Exercises_I_3_12.lean diff --git a/Bookshelf/Combinator/Aviary.lean b/Bookshelf/Combinator/Aviary.lean index 341640f..2288e59 100644 --- a/Bookshelf/Combinator/Aviary.lean +++ b/Bookshelf/Combinator/Aviary.lean @@ -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` -/ diff --git a/Bookshelf/LTuple/Basic.lean b/Bookshelf/LTuple/Basic.lean index d925bce..c698b37 100644 --- a/Bookshelf/LTuple/Basic.lean +++ b/Bookshelf/LTuple/Basic.lean @@ -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 \ No newline at end of file diff --git a/Bookshelf/List/Basic.lean b/Bookshelf/List/Basic.lean index 9ceeb03..194cea4 100644 --- a/Bookshelf/List/Basic.lean +++ b/Bookshelf/List/Basic.lean @@ -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₂, diff --git a/Bookshelf/Real/Basic.lean b/Bookshelf/Real/Basic.lean index 2b2d76d..c94c522 100644 --- a/Bookshelf/Real/Basic.lean +++ b/Bookshelf/Real/Basic.lean @@ -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 \ No newline at end of file diff --git a/Bookshelf/Real/Function/Step.lean b/Bookshelf/Real/Function/Step.lean index 03d9a2a..1bb3f23 100644 --- a/Bookshelf/Real/Function/Step.lean +++ b/Bookshelf/Real/Function/Step.lean @@ -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 diff --git a/Bookshelf/Real/Geometry/Area.lean b/Bookshelf/Real/Geometry/Area.lean index 5d80233..bb18f9b 100644 --- a/Bookshelf/Real/Geometry/Area.lean +++ b/Bookshelf/Real/Geometry/Area.lean @@ -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 /-- diff --git a/Bookshelf/Real/Geometry/Basic.lean b/Bookshelf/Real/Geometry/Basic.lean index 7e35c25..6eabafa 100644 --- a/Bookshelf/Real/Geometry/Basic.lean +++ b/Bookshelf/Real/Geometry/Basic.lean @@ -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 diff --git a/Bookshelf/Real/Geometry/Rectangle.lean b/Bookshelf/Real/Geometry/Rectangle.lean index 7dbc33a..8d86195 100644 --- a/Bookshelf/Real/Geometry/Rectangle.lean +++ b/Bookshelf/Real/Geometry/Rectangle.lean @@ -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 diff --git a/Bookshelf/Real/Rational.lean b/Bookshelf/Real/Rational.lean index ee08068..5a1feaa 100644 --- a/Bookshelf/Real/Rational.lean +++ b/Bookshelf/Real/Rational.lean @@ -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 diff --git a/Bookshelf/Real/Sequence/Arithmetic.lean b/Bookshelf/Real/Sequence/Arithmetic.lean index a334d20..4a8667f 100644 --- a/Bookshelf/Real/Sequence/Arithmetic.lean +++ b/Bookshelf/Real/Sequence/Arithmetic.lean @@ -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 /-- diff --git a/Bookshelf/Real/Sequence/Geometric.lean b/Bookshelf/Real/Sequence/Geometric.lean index 31da033..25076e8 100644 --- a/Bookshelf/Real/Sequence/Geometric.lean +++ b/Bookshelf/Real/Sequence/Geometric.lean @@ -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 /-- diff --git a/Bookshelf/Real/Set/Basic.lean b/Bookshelf/Real/Set/Basic.lean index d9666f9..8b2f39f 100644 --- a/Bookshelf/Real/Set/Basic.lean +++ b/Bookshelf/Real/Set/Basic.lean @@ -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 diff --git a/Bookshelf/Real/Set/Interval.lean b/Bookshelf/Real/Set/Interval.lean index 6f24d9c..6e297d1 100644 --- a/Bookshelf/Real/Set/Interval.lean +++ b/Bookshelf/Real/Set/Interval.lean @@ -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. -/ diff --git a/Bookshelf/Real/Set/Partition.lean b/Bookshelf/Real/Set/Partition.lean index 462f6b1..e6e8ed2 100644 --- a/Bookshelf/Real/Set/Partition.lean +++ b/Bookshelf/Real/Set/Partition.lean @@ -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 diff --git a/Exercises/Apostol.lean b/Exercises/Apostol.lean index c8d7411..d4fda4b 100644 --- a/Exercises/Apostol.lean +++ b/Exercises/Apostol.lean @@ -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 diff --git a/Exercises/Apostol/Chapter_I_3.lean b/Exercises/Apostol/Chapter_I_3.lean index 536f98e..fc5243c 100644 --- a/Exercises/Apostol/Chapter_I_3.lean +++ b/Exercises/Apostol/Chapter_I_3.lean @@ -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 \ No newline at end of file diff --git a/Exercises/Apostol/Exercises_I_3_12.lean b/Exercises/Apostol/Exercises_I_3_12.lean deleted file mode 100644 index 16743d4..0000000 --- a/Exercises/Apostol/Exercises_I_3_12.lean +++ /dev/null @@ -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 diff --git a/Exercises/Avigad.lean b/Exercises/Avigad.lean index 2bae288..86a247f 100644 --- a/Exercises/Avigad.lean +++ b/Exercises/Avigad.lean @@ -1,4 +1,3 @@ --- Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. import Exercises.Avigad.Chapter2 import Exercises.Avigad.Chapter3 import Exercises.Avigad.Chapter4 diff --git a/Exercises/Avigad/Chapter2.lean b/Exercises/Avigad/Chapter2.lean index 7add927..0220b03 100644 --- a/Exercises/Avigad/Chapter2.lean +++ b/Exercises/Avigad/Chapter2.lean @@ -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 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter3.lean b/Exercises/Avigad/Chapter3.lean index 98c325c..08bd45e 100644 --- a/Exercises/Avigad/Chapter3.lean +++ b/Exercises/Avigad/Chapter3.lean @@ -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 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter4.lean b/Exercises/Avigad/Chapter4.lean index f0223da..5066bc3 100644 --- a/Exercises/Avigad/Chapter4.lean +++ b/Exercises/Avigad/Chapter4.lean @@ -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 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter5.lean b/Exercises/Avigad/Chapter5.lean index f34fb4b..bf743ec 100644 --- a/Exercises/Avigad/Chapter5.lean +++ b/Exercises/Avigad/Chapter5.lean @@ -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 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter7.lean b/Exercises/Avigad/Chapter7.lean index c556ec7..2620361 100644 --- a/Exercises/Avigad/Chapter7.lean +++ b/Exercises/Avigad/Chapter7.lean @@ -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 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter8.lean b/Exercises/Avigad/Chapter8.lean index 532d180..49bf41b 100644 --- a/Exercises/Avigad/Chapter8.lean +++ b/Exercises/Avigad/Chapter8.lean @@ -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 \ No newline at end of file diff --git a/Exercises/Enderton.lean b/Exercises/Enderton.lean index cbc3de6..0fcf796 100644 --- a/Exercises/Enderton.lean +++ b/Exercises/Enderton.lean @@ -1,3 +1 @@ --- Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: --- Harcourt/Academic Press, 2001. import Exercises.Enderton.Chapter0 \ No newline at end of file diff --git a/Exercises/Enderton/Chapter0.lean b/Exercises/Enderton/Chapter0.lean index c15f625..5fb58a9 100644 --- a/Exercises/Enderton/Chapter0.lean +++ b/Exercises/Enderton/Chapter0.lean @@ -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 \ No newline at end of file +end + +end Exercises.Enderton.Chapter0 \ No newline at end of file diff --git a/Exercises/Fraleigh.lean b/Exercises/Fraleigh.lean index 6d561ac..8126b2f 100644 --- a/Exercises/Fraleigh.lean +++ b/Exercises/Fraleigh.lean @@ -1,2 +1 @@ --- Fraleigh, John B. A First Course in Abstract Algebra, n.d. import Exercises.Fraleigh.Chapter1 \ No newline at end of file diff --git a/Exercises/Fraleigh/Chapter1.lean b/Exercises/Fraleigh/Chapter1.lean index f0f0df8..8b2f2b1 100644 --- a/Exercises/Fraleigh/Chapter1.lean +++ b/Exercises/Fraleigh/Chapter1.lean @@ -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 \ No newline at end of file