List books being worked through.

README.md

@@ -1,14 +1,15 @@
-# bookshelf-lean
+# bookshelf
 
-A collection of proofs and answers to exercises to books I'm studying.
+A collection on the study of the books listed below. I aim to use [Lean](https://leanprover.github.io/)
+when possible (with respect to my current level of ability) and fallback to
+LaTeX when not.
 
-## Updates
-
-Lean's tooling is a fickle beast. If looking to update e.g. `Mathlib`, pin a new
-version to the `lake-manifest.json` file and start a new build from scratch:
-
-```bash
-> lake update
-> lake clean
-> lake build
-```
+- [ ] Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
+- [ ] Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+- [ ] Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in Mathematics. Cham: Springer International Publishing, 2015.
+- [ ] Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 3rd ed. Cambridge, Mass: MIT Press, 2009.
+- [ ] Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.
+- [ ] Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+- [ ] Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020.
+- [ ] Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.
+- [ ] Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.

bookshelf/Bookshelf.lean

@@ -1,4 +0,0 @@
-import Bookshelf.Sequence.Arithmetic
-import Bookshelf.Sequence.Geometric
-import Bookshelf.Tuple
-import Bookshelf.Vector

bookshelf/Bookshelf/Vector.lean

@@ -1,53 +0,0 @@
-import Mathlib.Tactic.Ring
-
-/--
-A list-like structure with its size encoded in the type.
-
-For a `Vector`-like type with opposite "endian", refer to `Tuple`.
--/
-inductive Vector (α : Type u) : (size : Nat) → Type u where
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n + 1)
-
-syntax (priority := high) "v[" term,* "]" : term
-
-macro_rules
-  | `(v[]) => `(Vector.nil)
-  | `(v[$x]) => `(Vector.cons $x v[])
-  | `(v[$x, $xs:term,*]) => `(Vector.cons $x v[$xs,*])
-
-namespace Vector
-
-/--
-Returns the number of entries in the `Vector`.
--/
-def size (_ : Vector α n) : Nat := n
-
-/--
-Returns the first entry of the `Vector`.
--/
-def head : Vector α (n + 1) → α
-  | cons v _ => v
-
-/--
-Returns the last entry of the `Vector`.
--/
-def last : Vector α (n + 1) → α
-  | cons v vs => if _ : n = 0 then v else
-      match n with
-      | _ + 1 => vs.last
-
-/--
-Returns all but the `head` of the `Vector`.
--/
-def tail : Vector α (n + 1) → Vector α n
-  | cons _ vs => vs
-
-/--
-Appends an entry to the end of the `Vector`.
--/
-def snoc : Vector α n → α → Vector α (n + 1)
-  | nil, a => v[a]
-  | cons v vs, a => cons v (snoc vs a)
-
-end Vector

common/Common.lean

@@ -0,0 +1,3 @@
+import Common.Sequence.Arithmetic
+import Common.Sequence.Geometric
+import Common.Tuple

common/Common/Sequence/Arithmetic.lean

@@ -1,10 +1,3 @@
-/-
-# References
-
-1. Levin, Oscar. Discrete Mathematics: An Open Introduction. 3rd ed., n.d.
-   https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf.
--/
-
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.Ring
 

common/Common/Sequence/Geometric.lean

@@ -1,10 +1,3 @@
-/-
-# References
-
-1. Levin, Oscar. Discrete Mathematics: An Open Introduction. 3rd ed., n.d.
-   https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf.
--/
-
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.Ring
 

common/Common/Tuple.lean

@@ -1,10 +1,3 @@
-/-
-# References
-
-1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
-   Harcourt/Academic Press, 2001.
--/
-
 import Mathlib.Tactic.Ring
 
 /--
@@ -29,9 +22,9 @@ macro_rules
 
 namespace Tuple
 
-/- -------------------------------------
- - Coercions
- - -------------------------------------/
+-- ========================================
+-- Coercions
+-- ========================================
 
 scoped instance : CoeOut (Tuple α (min (m + n) m)) (Tuple α m) where
   coe := cast (by simp)
@@ -54,9 +47,9 @@ scoped instance : Coe (Tuple α (min m n + 1)) (Tuple α (min (m + 1) (n + 1)))
 scoped instance : Coe (Tuple α m) (Tuple α (min (m + n) m)) where
   coe := cast (by simp)
 
-/- -------------------------------------
- - Equality
- - -------------------------------------/
+-- ========================================
+-- Equality
+-- ========================================
 
 theorem eq_nil : @Tuple.nil α = t[] := rfl
 
@@ -90,9 +83,9 @@ protected def hasDecEq [DecidableEq α] (t₁ t₂ : Tuple α n) : Decidable (Eq
 
 instance [DecidableEq α] : DecidableEq (Tuple α n) := Tuple.hasDecEq
 
-/- -------------------------------------
- - Basic API
- - -------------------------------------/
+-- ========================================
+-- Basic API
+-- ========================================
 
 /--
 Returns the number of entries of the `Tuple`.
@@ -118,9 +111,9 @@ def cons : Tuple α n → α → Tuple α (n + 1)
   | t[], a => t[a]
   | snoc ts t, a => snoc (cons ts a) t
 
-/- -------------------------------------
- - Concatenation
- - -------------------------------------/
+-- ========================================
+-- Concatenation
+-- ========================================
 
 /--
 Join two `Tuple`s together end to end.
@@ -179,9 +172,9 @@ theorem snoc_eq_init_concat_last (as : Tuple α m) : snoc as a = concat as t[a]
     rfl
     (fun _ _ => by 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

common/lakefile.lean

@@ -1,13 +1,11 @@
 import Lake
 open Lake DSL
 
-package «Bookshelf»
+package «Common»
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @
     "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"
 
 @[default_target]
-lean_lib «Bookshelf» {
-  -- add library configuration options here
-}
+lean_lib «Common»

first-course-abstract-algebra/lake-manifest.json

@@ -1,8 +1,7 @@
 {"version": 4,
  "packagesDir": "lake-packages",
  "packages":
- [{"path": {"name": "Bookshelf", "dir": "./../bookshelf"}},
-  {"git":
+ [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
     "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a",
@@ -25,4 +24,5 @@
     "subDir?": null,
     "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2",
     "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "main"}},
+  {"path": {"name": "Common", "dir": "./../common"}}]}

first-course-abstract-algebra/lakefile.lean

@@ -3,7 +3,7 @@ open Lake DSL
 
 package «first-course-abstract-algebra»
 
-require Bookshelf from "../bookshelf"
+require Common from "../common"
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @
     "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"

mathematical-introduction-logic/Enderton/Chapter0.lean

@@ -4,15 +4,15 @@ Chapter 0
 Useful Facts About Sets
 -/
 
-import Bookshelf.Tuple
+import Common.Tuple
 
 /--
-The following describes a so-called "generic" tuple. Like in `Bookshelf.Tuple`,
-an `n`-tuple is defined recursively like so:
+The following describes a so-called "generic" tuple. Like in `Common.Tuple`, an
+`n`-tuple is defined recursively like so:
 
   `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩`
 
-Unlike `Bookshelf.Tuple`, a "generic" tuple bends the syntax above further. For
+Unlike `Common.Tuple`, a "generic" tuple bends the syntax above further. For
 example, both tuples above are equivalent to:
 
   `⟨⟨x₁, ..., xₘ⟩, xₘ₊₁, ..., xₙ⟩`
@@ -20,7 +20,7 @@ example, both tuples above are equivalent to:
 for some `1 ≤ m ≤ n`. This distinction is purely syntactic, but necessary to
 prove certain theorems found in [1] (e.g. `lemma_0a`).
 
-In general, prefer `Bookshelf.Tuple`.
+In general, prefer `Common.Tuple`.
 -/
 inductive XTuple : (α : Type u) → (size : Nat × Nat) → Type u where
   | nil : XTuple α (0, 0)
@@ -38,9 +38,9 @@ namespace XTuple
 
 open scoped Tuple
 
-/- -------------------------------------
- - Normalization
- - -------------------------------------/
+-- ========================================
+-- Normalization
+-- ========================================
 
 /--
 Converts an `XTuple` into "normal form".
@@ -97,9 +97,9 @@ theorem norm_snoc_eq_concat {t₁ : XTuple α (p, q)} {t₂ : Tuple α n}
   : norm (snoc t₁ t₂) = Tuple.concat t₁.norm t₂ := by
   conv => lhs; unfold norm
 
-/- -------------------------------------
- - Equality
- - -------------------------------------/
+-- ========================================
+-- Equality
+-- ========================================
 
 /--
 Implements Boolean equality for `XTuple α n` provided `α` has decidable
@@ -108,9 +108,9 @@ equality.
 instance BEq [DecidableEq α] : BEq (XTuple α n) where
   beq t₁ t₂ := t₁.norm == t₂.norm
 
-/- -------------------------------------
- - Basic API
- - -------------------------------------/
+-- ========================================
+-- Basic API
+-- ========================================
 
 /--
 Returns the number of entries in the `XTuple`.
@@ -163,9 +163,9 @@ def snd : XTuple α (m, n) → Tuple α n
   | x[] => t[]
   | snoc _ ts => ts
 
-/- -------------------------------------
- - Lemma 0A
- - -------------------------------------/
+-- ========================================
+-- Lemma 0A
+-- ========================================
 
 section
 

mathematical-introduction-logic/lake-manifest.json

@@ -1,8 +1,7 @@
 {"version": 4,
  "packagesDir": "lake-packages",
  "packages":
- [{"path": {"name": "Bookshelf", "dir": "./../bookshelf"}},
-  {"git":
+ [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
     "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a",
@@ -25,4 +24,5 @@
     "subDir?": null,
     "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2",
     "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "main"}},
+  {"path": {"name": "Common", "dir": "./../common"}}]}

mathematical-introduction-logic/lakefile.lean

@@ -3,9 +3,7 @@ open Lake DSL
 
 package «mathematical-introduction-logic»
 
-require Bookshelf from "../bookshelf"
+require Common from "../common"
 
 @[default_target]
-lean_lib «enderton» {
-  -- add library configuration options here
-}
+lean_lib «enderton»

theorem-proving-in-lean/Avigad/Chapter2.lean

@@ -4,9 +4,11 @@ Chapter 2
 Dependent Type Theory
 -/
 
+-- ========================================
 -- Exercise 1
 --
 -- Define the function `Do_Twice`, as described in Section 2.4.
+-- ========================================
 namespace ex1
 
 def double (x : Nat) := x + x
@@ -17,9 +19,11 @@ 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.
+-- ========================================
 namespace ex2
 
 def curry (f : α × β → γ) : (α → β → γ) :=
@@ -30,6 +34,7 @@ def uncurry (f : α → β → γ) : (α × β → γ) :=
 
 end ex2
 
+-- ========================================
 -- Exercise 3
 --
 -- Above, we used the example `vec α n` for vectors of elements of type `α` of
@@ -39,6 +44,8 @@ end ex2
 -- implicit arguments for parameters that can be inferred. Declare some
 -- variables and check some expressions involving the constants that you have
 -- declared.
+-- ========================================
+
 namespace ex3
 
 universe u
@@ -64,6 +71,7 @@ variable (c d : vec Prop 2)
 
 end ex3
 
+-- ========================================
 -- Exercise 4
 --
 -- Similarly, declare a constant `matrix` so that `matrix α m n` could represent
@@ -72,6 +80,8 @@ end ex3
 -- (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
 
 universe u

theorem-proving-in-lean/Avigad/Chapter3.lean

@@ -4,10 +4,13 @@ Chapter 3
 Propositions and Proofs
 -/
 
+-- ========================================
 -- Exercise 1
 --
 -- Prove the following identities, replacing the "sorry" placeholders with
 -- actual proofs.
+-- ========================================
+
 namespace ex1
 
 open or
@@ -102,10 +105,13 @@ example : (p → q) → (¬q → ¬p) :=
 
 end ex1
 
--- Example 2
+-- ========================================
+-- Exercise 2
 --
 -- Prove the following identities, replacing the “sorry” placeholders with
 -- actual proofs. These require classical reasoning.
+-- ========================================
+
 namespace ex2
 
 open Classical
@@ -147,9 +153,12 @@ example : (((p → q) → p) → p) :=
 
 end ex2
 
--- Example 3
+-- ========================================
+-- Exercise 3
 --
 -- Prove `¬(p ↔ ¬p)` without using classical logic.
+-- ========================================
+
 namespace ex3
 
 variable (p : Prop)

theorem-proving-in-lean/Avigad/Chapter4.lean

@@ -4,10 +4,13 @@ Chapter 4
 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.
+-- ========================================
+
 namespace ex1
 
 variable (α : Type _)
@@ -34,11 +37,14 @@ 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).
+-- ========================================
+
 namespace ex2
 
 variable (α : Type _)
@@ -70,11 +76,14 @@ example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
 
 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.
+-- ========================================
+
 namespace ex3
 
 open Classical
@@ -91,6 +100,7 @@ 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
@@ -101,6 +111,8 @@ end ex3
 -- 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
 
 def even (a : Nat) := ∃ b, a = 2 * b
@@ -132,9 +144,12 @@ def Fermat'sLastTheorem : Prop :=
 
 end ex4
 
+-- ========================================
 -- Exercise 5
 --
 -- Prove as many of the identities listed in Section 4.4 as you can.
+-- ========================================
+
 namespace ex5
 
 open Classical
@@ -215,9 +230,12 @@ example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
 
 end ex5
 
+-- ========================================
 -- Exercise 6
 --
 -- Give a calculational proof of the theorem `log_mul` below.
+-- ========================================
+
 namespace ex6
 
 variable (log exp : Float → Float)

theorem-proving-in-lean/Avigad/Chapter5.lean

@@ -4,13 +4,18 @@ Chapter 5
 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.
+-- ========================================
+
 namespace ex1
 
+-- ----------------------------------------
 -- Exercises 3.1
+-- ----------------------------------------
 
 section ex3_1
 
@@ -151,7 +156,9 @@ example : (p → q) → (¬q → ¬p) := by
 
 end ex3_1
 
+-- ----------------------------------------
 -- Exercises 3.2
+-- ----------------------------------------
 
 section ex3_2
 
@@ -220,7 +227,9 @@ example : (((p → q) → p) → p) := by
 
 end ex3_2
 
+-- ----------------------------------------
 -- Exercises 3.3
+-- ----------------------------------------
 
 section ex3_3
 
@@ -232,7 +241,9 @@ example (hp : p) : ¬(p ↔ ¬p) := by
 
 end ex3_3
 
+-- ----------------------------------------
 -- Exercises 4.1
+-- ----------------------------------------
 
 section ex4_1
 
@@ -261,7 +272,9 @@ example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := by
 
 end ex4_1
 
+-- ----------------------------------------
 -- Exercises 4.2
+-- ----------------------------------------
 
 section ex4_2
 
@@ -313,7 +326,9 @@ example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := by
 
 end ex4_2
 
+-- ----------------------------------------
 -- Exercises 4.3
+-- ----------------------------------------
 
 section ex4_3
 
@@ -332,7 +347,9 @@ example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := by
 
 end ex4_3
 
+-- ----------------------------------------
 -- Exercises 4.5
+-- ----------------------------------------
 
 section ex4_5
 
@@ -443,9 +460,12 @@ end ex4_5
 
 end ex1
 
+-- ========================================
 -- 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) :=

theorem-proving-in-lean/Avigad/Chapter7.lean

@@ -4,6 +4,7 @@ Chapter 7
 Inductive Types
 -/
 
+-- ========================================
 -- Exercise 1
 --
 -- Try defining other operations on the natural numbers, such as multiplication,
@@ -15,6 +16,8 @@ Inductive Types
 -- 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
 
 -- As defined in the book.
@@ -74,6 +77,7 @@ end Nat
 
 end ex1
 
+-- ========================================
 -- Exercise 2
 --
 -- Define some operations on lists, like a `length` function or the `reverse`
@@ -82,6 +86,8 @@ end ex1
 -- a. `length (s ++ t) = length s + length t`
 -- b. `length (reverse t) = length t`
 -- c. `reverse (reverse t) = t`
+-- ========================================
+
 namespace ex2
 
 variable {α : Type _}
@@ -171,6 +177,7 @@ theorem reverse_reverse (t : List α)
 
 end ex2
 
+-- ========================================
 -- Exercise 3
 --
 -- Define an inductive data type consisting of terms built up from the following
@@ -183,6 +190,8 @@ end ex2
 --
 -- Recursively define a function that evaluates any such term with respect to an
 -- assignment of values to the variables.
+-- ========================================
+
 namespace ex3
 
 inductive Foo : Type _

theorem-proving-in-lean/Avigad/Chapter8.lean

@@ -4,12 +4,15 @@ Chapter 8
 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 ex1
 
 def add : Nat → Nat → Nat
@@ -26,11 +29,14 @@ 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`).
+-- ========================================
+
 namespace ex2
 
 variable {α : Type _}
@@ -43,11 +49,14 @@ 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.
+-- ========================================
+
 namespace ex3
 
 def below {motive : Nat → Type} : Nat → Type
@@ -58,11 +67,14 @@ def below {motive : Nat → Type} : Nat → Type
 
 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.
+-- ========================================
+
 namespace ex4
 
 inductive Vector (α : Type u) : Nat → Type u
@@ -77,11 +89,14 @@ end Vector
 
 end ex4
 
+-- ========================================
 -- Exercise 5
 --
 -- Consider the following type of arithmetic expressions. The idea is that
 -- `var n` is a variable, `vₙ`, and `const n` is the constant whose value is
 -- `n`.
+-- ========================================
+
 namespace ex5
 
 inductive Expr where
@@ -113,10 +128,12 @@ 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.
+-- ----------------------------------------
 
 def simpConst : Expr → Expr
   | plus (const n₁) (const n₂)  => const (n₁ + n₂)