Reorganize project once more, consolidating more into `Bookshelf`.

Bookshelf.lean

@@ -1,2 +1,3 @@
+import Bookshelf.Combinator
 import Bookshelf.List
 import Bookshelf.Real

Bookshelf/Combinator.lean

@@ -0,0 +1 @@
+import Bookshelf.Combinator.Aviary

Bookshelf/Combinator/Aviary.tex

@@ -10,7 +10,8 @@
 \label{sec:aviary}
 
 A list of birds as defined in \textit{To Mock a Mockingbird}.
-Refer to \href{../../../MockMockingbird/Aviary.html}{MockMockingbird/Aviary} for implementation examples.
+Refer to \href{../../../../Bookshelf/Combinator/Aviary.html}{Bookshelf/Combinator/Aviary}
+for implementation examples.
 
 \begin{itemize}
   \bird{Bald Eagle} $\hat{E}xy_1y_2y_3z_1z_2z_3 = x(y_1y_2y_3)(z_1z_2z_3)$

Bookshelf/LTuple.lean

@@ -0,0 +1 @@
+import Bookshelf.LTuple.Basic

Bookshelf/LTuple/Basic.lean

@@ -1,14 +1,11 @@
 import Mathlib.Tactic.Ring
 
 /--
-A representation of a tuple. In particular, `n`-tuples are defined recursively
-as follows:
+A representation of a possibly empty left-biased tuple. `n`-tuples are defined
+recursively as follows:
 
   `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩`
 
-We allow empty tuples. For a `Tuple`-like type with opposite "endian", refer to
-`Mathlib.Data.Vector`.
-
 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
@@ -20,56 +17,49 @@ Keep in mind a tuple in Lean already exists but it differs in two ways:
 In general, prefer using `Prod` over this `Tuple` definition. This exists solely
 for proving theorems outlined in Enderton's book.
 -/
-inductive Tuple : (α : Type u) → (size : Nat) → Type u where
-  | nil : Tuple α 0
-  | snoc : Tuple α n → α → Tuple α (n + 1)
+inductive LTuple : (α : Type u) → (size : Nat) → Type u where
+  | nil : LTuple α 0
+  | snoc : LTuple α n → α → LTuple α (n + 1)
 
-syntax (priority := high) "t[" term,* "]" : term
-
-macro_rules
-  | `(t[]) => `(Tuple.nil)
-  | `(t[$x]) => `(Tuple.snoc t[] $x)
-  | `(t[$xs:term,*, $x]) => `(Tuple.snoc t[$xs,*] $x)
-
-namespace Tuple
+namespace LTuple
 
 -- ========================================
 -- Coercions
 -- ========================================
 
-scoped instance : CoeOut (Tuple α (min (m + n) m)) (Tuple α m) where
+scoped instance : CoeOut (LTuple α (min (m + n) m)) (LTuple α m) where
   coe := cast (by simp)
 
-scoped instance : Coe (Tuple α 0) (Tuple α (min n 0)) where
+scoped instance : Coe (LTuple α 0) (LTuple α (min n 0)) where
   coe := cast (by rw [Nat.min_zero])
 
-scoped instance : Coe (Tuple α 0) (Tuple α (min 0 n)) where
+scoped instance : Coe (LTuple α 0) (LTuple α (min 0 n)) where
   coe := cast (by rw [Nat.zero_min])
 
-scoped instance : Coe (Tuple α n) (Tuple α (min n n)) where
+scoped instance : Coe (LTuple α n) (LTuple α (min n n)) where
   coe := cast (by simp)
 
-scoped instance : Coe (Tuple α n) (Tuple α (0 + n)) where
+scoped instance : Coe (LTuple α n) (LTuple α (0 + n)) where
   coe := cast (by simp)
 
-scoped instance : Coe (Tuple α (min m n + 1)) (Tuple α (min (m + 1) (n + 1))) where
+scoped instance : Coe (LTuple α (min m n + 1)) (LTuple α (min (m + 1) (n + 1))) where
   coe := cast (by rw [Nat.min_succ_succ])
 
-scoped instance : Coe (Tuple α m) (Tuple α (min (m + n) m)) where
+scoped instance : Coe (LTuple α m) (LTuple α (min (m + n) m)) where
   coe := cast (by simp)
 
 -- ========================================
 -- Equality
 -- ========================================
 
-theorem eq_nil : @Tuple.nil α = t[] := rfl
+theorem eq_nil : @LTuple.nil α = nil := rfl
 
-theorem eq_iff_singleton : (a = b) ↔ (t[a] = t[b]) := by
+theorem eq_iff_singleton : (a = b) ↔ (snoc a nil = snoc b nil) := by
   apply Iff.intro
   · intro h; rw [h]
   · intro h; injection h
 
-theorem eq_iff_snoc {t₁ t₂ : Tuple α n}
+theorem eq_iff_snoc {t₁ t₂ : LTuple α n}
   : (a = b ∧ t₁ = t₂) ↔ (snoc t₁ a = snoc t₂ b) := by
   apply Iff.intro
   · intro ⟨h₁, h₂ ⟩; rw [h₁, h₂]
@@ -81,12 +71,12 @@ theorem eq_iff_snoc {t₁ t₂ : Tuple α n}
 Implements decidable equality for `Tuple α m`, provided `a` has decidable
 equality. 
 -/
-protected def hasDecEq [DecidableEq α] (t₁ t₂ : Tuple α n)
+protected def hasDecEq [DecidableEq α] (t₁ t₂ : LTuple α n)
   : Decidable (Eq t₁ t₂) :=
   match t₁, t₂ with
-  | t[], t[] => isTrue eq_nil
+  | nil, nil => isTrue eq_nil
   | snoc as a, snoc bs b =>
-    match Tuple.hasDecEq as bs with
+    match LTuple.hasDecEq as bs with
     | isFalse np => isFalse (fun h => absurd (eq_iff_snoc.mpr h).right np)
     | isTrue hp =>
       if hq : a = b then
@@ -94,7 +84,7 @@ protected def hasDecEq [DecidableEq α] (t₁ t₂ : Tuple α n)
       else
         isFalse (fun h => absurd (eq_iff_snoc.mpr h).left hq)
 
-instance [DecidableEq α] : DecidableEq (Tuple α n) := Tuple.hasDecEq
+instance [DecidableEq α] : DecidableEq (LTuple α n) := LTuple.hasDecEq
 
 -- ========================================
 -- Basic API
@@ -103,25 +93,25 @@ instance [DecidableEq α] : DecidableEq (Tuple α n) := Tuple.hasDecEq
 /--
 Returns the number of entries of the `Tuple`.
 -/
-def size (_ : Tuple α n) : Nat := n
+def size (_ : LTuple α n) : Nat := n
 
 /--
 Returns all but the last entry of the `Tuple`.
 -/
-def init : (t : Tuple α (n + 1)) → Tuple α n
+def init : (t : LTuple α (n + 1)) → LTuple α n
   | snoc vs _ => vs
 
 /--
 Returns the last entry of the `Tuple`.
 -/
-def last : Tuple α (n + 1) → α
+def last : LTuple α (n + 1) → α
   | snoc _ v => v
 
 /--
 Prepends an entry to the start of the `Tuple`.
 -/
-def cons : Tuple α n → α → Tuple α (n + 1)
-  | t[], a => t[a]
+def cons : LTuple α n → α → LTuple α (n + 1)
+  | nil, a => snoc nil a
   | snoc ts t, a => snoc (cons ts a) t
 
 -- ========================================
@@ -131,55 +121,55 @@ def cons : Tuple α n → α → Tuple α (n + 1)
 /--
 Join two `Tuple`s together end to end.
 -/
-def concat : Tuple α m → Tuple α n → Tuple α (m + n)
-  | is, t[] => is
+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`.
 -/
-theorem self_concat_nil_eq_self (t : Tuple α m) : concat t t[] = t :=
+theorem self_concat_nil_eq_self (t : LTuple α m) : concat t nil = t :=
   match t with
-  | t[] => rfl
+  | nil => rfl
   | snoc _ _ => rfl
 
 /--
 Concatenating `nil` with a `Tuple` yields the `Tuple`.
 -/
-theorem nil_concat_self_eq_self (t : Tuple α m) : concat t[] t = t := by
+theorem nil_concat_self_eq_self (t : LTuple α m) : concat nil t = t := by
   induction t with
   | nil => unfold concat; simp
   | @snoc n as a ih =>
     unfold concat
     rw [ih]
-    suffices HEq (snoc (cast (_ : Tuple α n = Tuple α (0 + n)) as) a) ↑(snoc as a)
+    suffices HEq (snoc (cast (_ : LTuple α n = LTuple α (0 + n)) as) a) ↑(snoc as a)
       from eq_of_heq this
     have h₁ := Eq.recOn
       (motive := fun x h => HEq
-        (snoc (cast (show Tuple α n = Tuple α x by rw [h]) as) a)
+        (snoc (cast (show LTuple α n = LTuple α x by rw [h]) as) a)
         (snoc as a))
       (show n = 0 + n by simp)
       HEq.rfl
     exact Eq.recOn
       (motive := fun x h => HEq
-        (snoc (cast (_ : Tuple α n = Tuple α (0 + n)) as) a)
+        (snoc (cast (_ : LTuple α n = LTuple α (0 + n)) as) a)
         (cast h (snoc as a)))
-      (show Tuple α (n + 1) = Tuple α (0 + (n + 1)) by simp)
+      (show LTuple α (n + 1) = LTuple α (0 + (n + 1)) by simp)
       h₁
 
 /--
 Concatenating a `Tuple` to a nonempty `Tuple` moves `concat` calls closer to
 expression leaves.
 -/
-theorem concat_snoc_snoc_concat {bs : Tuple α n}
+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.
 -/
-theorem snoc_eq_init_concat_last (as : Tuple α m)
-  : snoc as a = concat as t[a] := by
+theorem snoc_eq_init_concat_last (as : LTuple α m)
+  : snoc as a = concat as (snoc nil a) := by
   cases as with
   | nil => rfl
   | snoc _ _ => simp; unfold concat concat; rfl
@@ -192,12 +182,12 @@ theorem snoc_eq_init_concat_last (as : Tuple α m)
 Take the first `k` entries from the `Tuple` to form a new `Tuple`, or the entire
 `Tuple` if `k` exceeds the number of entries.
 -/
-def take (t : Tuple α n) (k : Nat) : Tuple α (min n k) :=
+def take (t : LTuple α n) (k : Nat) : LTuple α (min n k) :=
   if h : n ≤ k then
     cast (by rw [min_eq_left h]) t
   else
     match t with
-    | t[] => t[]
+    | nil => nil
     | @snoc _ n' as a => cast (by rw [min_lt_succ_eq h]) (take as k)
  where
   min_lt_succ_eq {m : Nat} (h : ¬m + 1 ≤ k) : min m k = min (m + 1) k := by
@@ -208,7 +198,7 @@ def take (t : Tuple α n) (k : Nat) : Tuple α (min n k) :=
 /--
 Taking no entries from any `Tuple` should yield an empty one.
 -/
-theorem self_take_zero_eq_nil (t : Tuple α n) : take t 0 = @nil α := by
+theorem self_take_zero_eq_nil (t : LTuple α n) : take t 0 = @nil α := by
   induction t with
   | nil => simp; rfl
   | snoc as a ih => unfold take; simp; rw [ih]; simp
@@ -222,7 +212,7 @@ theorem nil_take_zero_eq_nil (k : Nat) : (take (@nil α) k) = @nil α := by
 /--
 Taking `n` entries from a `Tuple` of size `n` should yield the same `Tuple`.
 -/
-theorem self_take_size_eq_self (t : Tuple α n) : take t n = t := by
+theorem self_take_size_eq_self (t : LTuple α n) : take t n = t := by
   cases t with
   | nil => simp; rfl
   | snoc as a => unfold take; simp
@@ -231,7 +221,7 @@ theorem self_take_size_eq_self (t : Tuple α n) : take t n = t := by
 Taking all but the last entry of a `Tuple` is the same result, regardless of the
 value of the last entry.
 -/
-theorem take_subst_last {as : Tuple α n} (a₁ a₂ : α)
+theorem take_subst_last {as : LTuple α n} (a₁ a₂ : α)
   : take (snoc as a₁) n = take (snoc as a₂) n := by
   unfold take
   simp
@@ -239,7 +229,7 @@ theorem take_subst_last {as : Tuple α n} (a₁ a₂ : α)
 /--
 Taking `n` elements from a tuple of size `n + 1` is the same as invoking `init`.
 -/
-theorem init_eq_take_pred (t : Tuple α (n + 1)) : take t n = init t := by
+theorem init_eq_take_pred (t : LTuple α (n + 1)) : take t n = init t := by
   cases t with
   | snoc as a =>
     unfold init take
@@ -251,7 +241,7 @@ theorem init_eq_take_pred (t : Tuple α (n + 1)) : take t n = init t := by
 If two `Tuple`s are equal, then any initial sequences of those two `Tuple`s are
 also equal.
 -/
-theorem eq_tuple_eq_take {t₁ t₂ : Tuple α n}
+theorem eq_tuple_eq_take {t₁ t₂ : LTuple α n}
   : (t₁ = t₂) → (t₁.take k = t₂.take k) := by
   intro h
   rw [h]
@@ -260,7 +250,7 @@ theorem eq_tuple_eq_take {t₁ t₂ : Tuple α n}
 Given a `Tuple` of size `k`, concatenating an arbitrary `Tuple` and taking `k`
 elements yields the original `Tuple`.
 -/
-theorem eq_take_concat {t₁ : Tuple α m} {t₂ : Tuple α n}
+theorem eq_take_concat {t₁ : LTuple α m} {t₂ : LTuple α n}
   : take (concat t₁ t₂) m = t₁ := by
   induction t₂ with
   | nil =>
@@ -274,4 +264,4 @@ theorem eq_take_concat {t₁ : Tuple α m} {t₂ : Tuple α n}
     rw [ih]
     simp
 
-end Tuple
+end LTuple

Bookshelf/Real.lean

@@ -1,4 +1,6 @@
 import Bookshelf.Real.Basic
+import Bookshelf.Real.Function
+import Bookshelf.Real.Geometry
 import Bookshelf.Real.Rational
 import Bookshelf.Real.Sequence
 import Bookshelf.Real.Set

Bookshelf/Real/Function.lean

@@ -0,0 +1 @@
+import Bookshelf.Real.Function.Step

Bookshelf/Real/Function/Step.lean

@@ -1,5 +1,5 @@
 import Bookshelf.Real.Basic
-import OneVariableCalculus.Real.Set.Partition
+import Bookshelf.Real.Set.Partition
 
 namespace Real.Function
 

Bookshelf/Real/Geometry.lean

@@ -0,0 +1,3 @@
+import Bookshelf.Real.Geometry.Area
+import Bookshelf.Real.Geometry.Basic
+import Bookshelf.Real.Geometry.Rectangle

Bookshelf/Real/Geometry/Area.lean

@@ -1,10 +1,5 @@
-/-
-Chapter 1.6
-
-The concept of area as a set function
--/
-import OneVariableCalculus.Real.Function.Step
-import OneVariableCalculus.Real.Geometry.Rectangle
+import Bookshelf.Real.Function.Step
+import Bookshelf.Real.Geometry.Rectangle
 
 namespace Real.Geometry.Area
 

Bookshelf/Real/Geometry/Rectangle.lean

@@ -1,4 +1,4 @@
-import OneVariableCalculus.Real.Geometry.Basic
+import Bookshelf.Real.Geometry.Basic
 
 namespace Real
 

Bookshelf/Real/Sequence.tex

@@ -2,8 +2,8 @@
 
 \input{preamble}
 
-\newcommand{\linkA}[1]{\href{../../../../Bookshelf/Real/Sequence/Arithmetic.html\##1}{#1}}
-\newcommand{\linkG}[1]{\href{../../../../Bookshelf/Real/Sequence/Geometric.html\##1}{#1}}
+\newcommand{\linkA}[1]{\href{../../../Bookshelf/Real/Sequence/Arithmetic.html\##1}{#1}}
+\newcommand{\linkG}[1]{\href{../../../Bookshelf/Real/Sequence/Geometric.html\##1}{#1}}
 
 \begin{document}
 

Bookshelf/Real/Set.lean

@@ -0,0 +1,3 @@
+import Bookshelf.Real.Set.Basic
+import Bookshelf.Real.Set.Interval
+import Bookshelf.Real.Set.Partition

Exercises.lean

@@ -0,0 +1,4 @@
+import Exercises.Apostol
+import Exercises.Avigad
+import Exercises.Enderton
+import Exercises.Fraleigh

Exercises/Apostol.lean

@@ -0,0 +1,4 @@
+-- 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

Exercises/Apostol/Chapter_I_3.tex

@@ -3,7 +3,7 @@
 
 \input{preamble}
 
-\newcommand{\link}[1]{\href{../../../../OneVariableCalculus/Apostol/Chapter_I_3.html\##1}{#1}}
+\newcommand{\link}[1]{\href{../../../../Exercises/Apostol/Chapter_I_3.html\##1}{#1}}
 
 \begin{document}
 

Exercises/Apostol/Exercises_I_3_12.lean

@@ -10,7 +10,7 @@ import Mathlib.Data.Real.Sqrt
 import Mathlib.Tactic.LibrarySearch
 
 import Bookshelf.Real.Rational
-import OneVariableCalculus.Apostol.Chapter_I_3
+import Exercises.Apostol.Chapter_I_3
 
 -- ========================================
 -- Exercise 1

Exercises/Avigad.lean

@@ -0,0 +1,7 @@
+-- Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+import Exercises.Avigad.Chapter2
+import Exercises.Avigad.Chapter3
+import Exercises.Avigad.Chapter4
+import Exercises.Avigad.Chapter5
+import Exercises.Avigad.Chapter7
+import Exercises.Avigad.Chapter8

Exercises/Avigad/Chapter2.lean

@@ -9,6 +9,7 @@ Dependent Type Theory
 --
 -- Define the function `Do_Twice`, as described in Section 2.4.
 -- ========================================
+
 namespace ex1
 
 def double (x : Nat) := x + x
@@ -24,6 +25,7 @@ end ex1
 --
 -- Define the functions `curry` and `uncurry`, as described in Section 2.4.
 -- ========================================
+
 namespace ex2
 
 def curry (f : α × β → γ) : (α → β → γ) :=

Exercises/Enderton.lean

@@ -0,0 +1,3 @@
+-- Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
+-- Harcourt/Academic Press, 2001.
+import Exercises.Enderton.Chapter0

Exercises/Enderton/Chapter0.lean

@@ -0,0 +1,287 @@
+/-
+Chapter 0
+
+Useful Facts About Sets
+-/
+
+import Bookshelf.LTuple.Basic
+
+/--
+The following describes a so-called "generic" tuple. Like an `LTuple`, a generic
+`n`-tuple is defined recursively like so:
+
+  `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩`
+
+Unlike `LTuple`, this tuple bends the syntax above further. For example,
+both tuples above are equivalent to:
+
+  `⟨⟨x₁, ..., xₘ⟩, xₘ₊₁, ..., xₙ⟩`
+
+for some `1 ≤ m ≤ n`. This distinction is purely syntactic, and introduced
+solely to prove `lemma_0a`. In other words, `LTuple` is an always-normalized
+variant of an `GTuple`. In general, prefer it over this when working within
+Enderton's book.
+-/
+inductive GTuple : (α : Type u) → (size : Nat × Nat) → Type u where
+  | nil : GTuple α (0, 0)
+  | snoc : GTuple α (p, q) → LTuple α r → GTuple α (p + q, r)
+
+syntax (priority := high) "t[" term,* "]" : term
+
+macro_rules
+  | `(t[]) => `(LTuple.nil)
+  | `(t[$x]) => `(LTuple.snoc t[] $x)
+  | `(t[$xs:term,*, $x]) => `(LTuple.snoc t[$xs,*] $x)
+
+syntax (priority := high) "g[" term,* "]" : term
+
+macro_rules
+  | `(g[]) => `(GTuple.nil)
+  | `(g[$x]) => `(GTuple.snoc g[] t[$x])
+  | `(g[g[$xs:term,*], $ys:term,*]) => `(GTuple.snoc g[$xs,*] t[$ys,*])
+  | `(g[$x, $xs:term,*]) => `(GTuple.snoc g[] t[$x, $xs,*])
+
+namespace GTuple
+
+open scoped LTuple
+
+-- ========================================
+-- Normalization
+-- ========================================
+
+/--
+Converts an `GTuple` into "normal form".
+-/
+def norm : GTuple α (m, n) → LTuple α (m + n)
+  |         g[] => t[]
+  | snoc  is ts => LTuple.concat is.norm ts
+
+/--
+Normalization of an empty `GTuple` yields an empty `Tuple`.
+-/
+theorem norm_nil_eq_nil : @norm α 0 0 nil = LTuple.nil :=
+  rfl
+
+/--
+Normalization of a pseudo-empty `GTuple` yields an empty `Tuple`.
+-/
+theorem norm_snoc_nil_nil_eq_nil : @norm α 0 0 (snoc g[] t[]) = t[] := by
+  unfold norm norm
+  rfl
+
+/--
+Normalization elimates `snoc` when the `snd` component is `nil`.
+-/
+theorem norm_snoc_nil_elim {t : GTuple α (p, q)}
+  : norm (snoc t t[]) = norm t := by
+  cases t with
+  | nil => simp; unfold norm norm; rfl
+  | snoc tf tl =>
+      simp
+      conv => lhs; unfold norm
+
+/--
+Normalization eliminates `snoc` when the `fst` component is `nil`.
+-/
+theorem norm_nil_snoc_elim {ts : LTuple α n}
+  : norm (snoc g[] ts) = cast (by simp) ts := by
+  unfold norm norm
+  rw [LTuple.nil_concat_self_eq_self]
+
+/--
+Normalization distributes across `Tuple.snoc` calls.
+-/
+theorem norm_snoc_snoc_norm
+  : norm (snoc as (LTuple.snoc bs b)) = LTuple.snoc (norm (snoc as bs)) b := by
+  unfold norm
+  rw [← LTuple.concat_snoc_snoc_concat]
+
+/--
+Normalizing an `GTuple` is equivalent to concatenating the normalized `fst`
+component with the `snd`.
+-/
+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
+-- ========================================
+
+/--
+Implements Boolean equality for `GTuple α n` provided `α` has decidable
+equality.
+-/
+instance BEq [DecidableEq α] : BEq (GTuple α n) where
+  beq t₁ t₂ := t₁.norm == t₂.norm
+
+-- ========================================
+-- Basic API
+-- ========================================
+
+/--
+Returns the number of entries in the `GTuple`.
+-/
+def size (_ : GTuple α n) := n
+
+/--
+Returns the number of entries in the "shallowest" portion of the `GTuple`. For
+example, the length of `x[x[1, 2], 3, 4]` is `3`, despite its size being `4`.
+-/
+def length : GTuple α n → Nat
+  |         g[] => 0
+  | snoc g[] ts => ts.size
+  | snoc   _ ts => 1 + ts.size
+
+/--
+Returns the first component of our `GTuple`. For example, the first component of
+tuple `x[x[1, 2], 3, 4]` is `t[1, 2]`.
+-/
+def fst : GTuple α (m, n) → LTuple α m
+  | g[] => t[]
+  | snoc ts _ => ts.norm
+
+/--
+Given `GTuple α (m, n)`, the `fst` component is equal to an initial segment of
+size `k` of the tuple in normal form.
+-/
+theorem self_fst_eq_norm_take (t : GTuple α (m, n)) : t.fst = t.norm.take m :=
+  match t with
+  | g[] => by
+    unfold fst
+    rw [LTuple.self_take_zero_eq_nil]
+    simp
+  | snoc tf tl => by
+    unfold fst
+    conv => rhs; unfold norm
+    rw [LTuple.eq_take_concat]
+    simp
+
+/--
+If the normal form of an `GTuple` is equal to a `Tuple`, the `fst` component
+must be a prefix of the `Tuple`.
+-/
+theorem norm_eq_fst_eq_take {t₁ : GTuple α (m, n)} {t₂ : LTuple α (m + n)}
+  : (t₁.norm = t₂) → (t₁.fst = t₂.take m) := by
+  intro h
+  rw [self_fst_eq_norm_take, h]
+
+/--
+Returns the first component of our `GTuple`. For example, the first component of
+tuple `x[x[1, 2], 3, 4]` is `t[3, 4]`.
+-/
+def snd : GTuple α (m, n) → LTuple α n
+  | g[] => t[]
+  | snoc _ ts => ts
+
+end GTuple
+
+-- ========================================
+-- Lemma 0A
+--
+-- Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Then
+-- `x₁ = ⟨y₁, ..., yₖ₊₁⟩`.
+-- ========================================
+
+section
+
+variable {k m n : Nat}
+variable (p : 1 ≤ m)
+variable (q : n + (m - 1) = m + k)
+
+private lemma n_eq_succ_k : n = k + 1 := by
+  let ⟨m', h⟩ := Nat.exists_eq_succ_of_ne_zero $ show m ≠ 0 by
+    intro h
+    have ff : 1 ≤ 0 := h ▸ p
+    ring_nf at ff
+    exact ff.elim
+  calc
+    n = n + (m - 1) - (m - 1) := by rw [Nat.add_sub_cancel]
+    _ = m' + 1 + k - (m' + 1 - 1) := by rw [q, h]
+    _ = m' + 1 + k - m' := by simp
+    _ = 1 + k + m' - m' := by rw [Nat.add_assoc, Nat.add_comm]
+    _ = 1 + k := by simp
+    _ = k + 1 := by rw [Nat.add_comm]
+
+private lemma n_pred_eq_k : n - 1 = k := by
+  have h : k + 1 - 1 = k + 1 - 1 := rfl
+  conv at h => lhs; rw [←n_eq_succ_k p q]
+  simp at h
+  exact h
+
+private lemma n_geq_one : 1 ≤ n := by
+  rw [n_eq_succ_k p q]
+  simp
+
+private lemma min_comm_succ_eq : min (m + k) (k + 1) = k + 1 :=
+  Nat.recOn k
+    (by simp; exact p)
+    (fun k' ih => calc min (m + (k' + 1)) (k' + 1 + 1)
+      _ = min (m + k' + 1) (k' + 1 + 1) := by conv => rw [Nat.add_assoc]
+      _ = min (m + k') (k' + 1) + 1 := Nat.min_succ_succ (m + k') (k' + 1)
+      _ = k' + 1 + 1 := by rw [ih])
+
+private lemma n_eq_min_comm_succ : n = min (m + k) (k + 1) := by
+  rw [min_comm_succ_eq p]
+  exact n_eq_succ_k p q
+
+private lemma n_pred_m_eq_m_k : n + (m - 1) = m + k := by
+  rw [←Nat.add_sub_assoc p, Nat.add_comm, Nat.add_sub_assoc (n_geq_one p q)]
+  conv => lhs; rw [n_pred_eq_k p q]
+
+private def cast_norm : GTuple α (n, m - 1) → LTuple α (m + k)
+  | xs => cast (by rw [q]) xs.norm
+
+private def cast_fst : GTuple α (n, m - 1) → LTuple α (k + 1)
+  | xs => cast (by rw [n_eq_succ_k p q]) xs.fst
+
+private def cast_take (ys : LTuple α (m + k)) :=
+  cast (by rw [min_comm_succ_eq p]) (ys.take (k + 1))
+
+/--
+Lemma 0A
+
+Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Then
+`x₁ = ⟨y₁, ..., yₖ₊₁⟩`.
+-/
+theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k))
+  : (cast_norm q xs = ys) → (cast_fst p q xs = cast_take p ys) := by
+  intro h
+  suffices HEq
+    (cast (_ : LTuple α n = LTuple α (k + 1)) xs.fst)
+    (cast (_ : LTuple α (min (m + k) (k + 1)) = LTuple α (k + 1)) (LTuple.take ys (k + 1)))
+    from eq_of_heq this
+  congr
+  · exact n_eq_min_comm_succ p q
+  · rfl
+  · exact n_eq_min_comm_succ p q
+  · exact HEq.rfl
+  · exact Eq.recOn
+      (motive := fun _ h => HEq
+        (_ : n + (n - 1) = n + k)
+        (cast h (show n + (n - 1) = n + k by rw [n_pred_eq_k p q])))
+      (show (n + (n - 1) = n + k) = (min (m + k) (k + 1) + (n - 1) = n + k) by
+        rw [n_eq_min_comm_succ p q])
+      HEq.rfl
+  · exact n_geq_one p q
+  · exact n_pred_eq_k p q
+  · exact Eq.symm (n_eq_min_comm_succ p q)
+  · exact n_pred_eq_k p q
+  · rw [GTuple.self_fst_eq_norm_take]
+    unfold cast_norm at h
+    simp at h
+    rw [←h, ←n_eq_succ_k p q]
+    have h₂ := Eq.recOn
+      (motive := fun x h => HEq
+        (LTuple.take xs.norm n)
+        (LTuple.take (cast (show LTuple α (n + (m - 1)) = LTuple α x by rw [h]) xs.norm) n))
+      (show n + (m - 1) = m + k by rw [n_pred_m_eq_m_k p q])
+      HEq.rfl
+    exact Eq.recOn
+      (motive := fun x h => HEq
+        (cast h (LTuple.take xs.norm n))
+        (LTuple.take (cast (_ : LTuple α (n + (m - 1)) = LTuple α (m + k)) xs.norm) n))
+      (show LTuple α (min (n + (m - 1)) n) = LTuple α n by simp)
+      h₂
+
+end

Exercises/Enderton/Chapter0.tex

@@ -2,7 +2,7 @@
 
 \input{preamble}
 
-\newcommand{\link}[1]{\href{../../../MathematicalIntroductionLogic/Enderton/Chapter0.html\##1}{#1}}
+\newcommand{\link}[1]{\href{../../../../Exercises/Enderton/Chapter0.html\##1}{#1}}
 
 \begin{document}
 

Exercises/Fraleigh.lean

@@ -0,0 +1,2 @@
+-- Fraleigh, John B. A First Course in Abstract Algebra, n.d.
+import Exercises.Fraleigh.Chapter1

lake-manifest.json

@@ -16,9 +16,9 @@
   {"git":
    {"url": "https://github.com/jrpotter/bookshelf-docgen.git",
     "subDir?": null,
-    "rev": "1de3481afd987d6b6dbd76245ed3c3eba1d6e680",
+    "rev": "8e2df427700e42610ddb51137698a105555d381d",
     "name": "doc-gen4",
-    "inputRev?": "1de3481afd987d6b6dbd76245ed3c3eba1d6e680"}},
+    "inputRev?": "8e2df427700e42610ddb51137698a105555d381d"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli",
     "subDir?": null,

lakefile.lean

@@ -12,19 +12,11 @@ require std4 from git
     "6006307d2ceb8743fea7e00ba0036af8654d0347"
 require «doc-gen4» from git
   "https://github.com/jrpotter/bookshelf-docgen.git" @
-    "1de3481afd987d6b6dbd76245ed3c3eba1d6e680"
+    "8e2df427700e42610ddb51137698a105555d381d"
 
 @[default_target]
 lean_lib «Bookshelf» {
-  srcDir := "src",
-  roots := #[
-    `Bookshelf,
-    `FirstCourseAbstractAlgebra,
-    `MathematicalIntroductionLogic,
-    `MockMockingbird,
-    `OneVariableCalculus,
-    `TheoremProvingInLean
-  ]
+  roots := #[`Bookshelf, `Exercises]
 }
 
 /--

src/Bookshelf/Real/Set.lean

@@ -1,2 +0,0 @@
-import Bookshelf.Real.Set.Basic
-import Bookshelf.Real.Set.Interval

src/FirstCourseAbstractAlgebra.lean

@@ -1 +0,0 @@
-import FirstCourseAbstractAlgebra.Fraleigh

src/FirstCourseAbstractAlgebra/Fraleigh.lean

@@ -1 +0,0 @@
-import FirstCourseAbstractAlgebra.Fraleigh.Chapter1

src/FirstCourseAbstractAlgebra/README.md

@@ -1,3 +0,0 @@
-# A First Course in Abstract Algebra
-
-Fraleigh, John B. A First Course in Abstract Algebra, n.d.

src/MathematicalIntroductionLogic.lean

@@ -1,2 +0,0 @@
-import MathematicalIntroductionLogic.Enderton
-import MathematicalIntroductionLogic.Tuple

src/MathematicalIntroductionLogic/Enderton.lean

@@ -1 +0,0 @@
-import MathematicalIntroductionLogic.Enderton.Chapter0

src/MathematicalIntroductionLogic/Enderton/Chapter0.lean

@@ -1,106 +0,0 @@
-/-
-Chapter 0
-
-Useful Facts About Sets
--/
-
-import MathematicalIntroductionLogic.Tuple.Generic
-
-variable {k m n : Nat}
-variable (p : 1 ≤ m)
-variable (q : n + (m - 1) = m + k)
-
-private lemma n_eq_succ_k : n = k + 1 := by
-  let ⟨m', h⟩ := Nat.exists_eq_succ_of_ne_zero $ show m ≠ 0 by
-    intro h
-    have ff : 1 ≤ 0 := h ▸ p
-    ring_nf at ff
-    exact ff.elim
-  calc
-    n = n + (m - 1) - (m - 1) := by rw [Nat.add_sub_cancel]
-    _ = m' + 1 + k - (m' + 1 - 1) := by rw [q, h]
-    _ = m' + 1 + k - m' := by simp
-    _ = 1 + k + m' - m' := by rw [Nat.add_assoc, Nat.add_comm]
-    _ = 1 + k := by simp
-    _ = k + 1 := by rw [Nat.add_comm]
-
-private lemma n_pred_eq_k : n - 1 = k := by
-  have h : k + 1 - 1 = k + 1 - 1 := rfl
-  conv at h => lhs; rw [←n_eq_succ_k p q]
-  simp at h
-  exact h
-
-private lemma n_geq_one : 1 ≤ n := by
-  rw [n_eq_succ_k p q]
-  simp
-
-private lemma min_comm_succ_eq : min (m + k) (k + 1) = k + 1 :=
-  Nat.recOn k
-    (by simp; exact p)
-    (fun k' ih => calc min (m + (k' + 1)) (k' + 1 + 1)
-      _ = min (m + k' + 1) (k' + 1 + 1) := by conv => rw [Nat.add_assoc]
-      _ = min (m + k') (k' + 1) + 1 := Nat.min_succ_succ (m + k') (k' + 1)
-      _ = k' + 1 + 1 := by rw [ih])
-
-private lemma n_eq_min_comm_succ : n = min (m + k) (k + 1) := by
-  rw [min_comm_succ_eq p]
-  exact n_eq_succ_k p q
-
-private lemma n_pred_m_eq_m_k : n + (m - 1) = m + k := by
-  rw [←Nat.add_sub_assoc p, Nat.add_comm, Nat.add_sub_assoc (n_geq_one p q)]
-  conv => lhs; rw [n_pred_eq_k p q]
-
-private def cast_norm : GTuple α (n, m - 1) → Tuple α (m + k)
-  | xs => cast (by rw [q]) xs.norm
-
-private def cast_fst : GTuple α (n, m - 1) → Tuple α (k + 1)
-  | xs => cast (by rw [n_eq_succ_k p q]) xs.fst
-
-private def cast_take (ys : Tuple α (m + k)) :=
-  cast (by rw [min_comm_succ_eq p]) (ys.take (k + 1))
-
-/--
-Lemma 0A
-
-Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Then
-`x₁ = ⟨y₁, ..., yₖ₊₁⟩`.
--/
-theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : Tuple α (m + k))
-  : (cast_norm q xs = ys) → (cast_fst p q xs = cast_take p ys) := by
-  intro h
-  suffices HEq
-    (cast (_ : Tuple α n = Tuple α (k + 1)) xs.fst)
-    (cast (_ : Tuple α (min (m + k) (k + 1)) = Tuple α (k + 1)) (Tuple.take ys (k + 1)))
-    from eq_of_heq this
-  congr
-  · exact n_eq_min_comm_succ p q
-  · rfl
-  · exact n_eq_min_comm_succ p q
-  · exact HEq.rfl
-  · exact Eq.recOn
-      (motive := fun _ h => HEq
-        (_ : n + (n - 1) = n + k)
-        (cast h (show n + (n - 1) = n + k by rw [n_pred_eq_k p q])))
-      (show (n + (n - 1) = n + k) = (min (m + k) (k + 1) + (n - 1) = n + k) by
-        rw [n_eq_min_comm_succ p q])
-      HEq.rfl
-  · exact n_geq_one p q
-  · exact n_pred_eq_k p q
-  · exact Eq.symm (n_eq_min_comm_succ p q)
-  · exact n_pred_eq_k p q
-  · rw [GTuple.self_fst_eq_norm_take]
-    unfold cast_norm at h
-    simp at h
-    rw [←h, ←n_eq_succ_k p q]
-    have h₂ := Eq.recOn
-      (motive := fun x h => HEq
-        (Tuple.take xs.norm n)
-        (Tuple.take (cast (show Tuple α (n + (m - 1)) = Tuple α x by rw [h]) xs.norm) n))
-      (show n + (m - 1) = m + k by rw [n_pred_m_eq_m_k p q])
-      HEq.rfl
-    exact Eq.recOn
-      (motive := fun x h => HEq
-        (cast h (Tuple.take xs.norm n))
-        (Tuple.take (cast (_ : Tuple α (n + (m - 1)) = Tuple α (m + k)) xs.norm) n))
-      (show Tuple α (min (n + (m - 1)) n) = Tuple α n by simp)
-      h₂

src/MathematicalIntroductionLogic/README.md

@@ -1,4 +0,0 @@
-# A Mathematical Introduction to Logic
-
-Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego:
-Harcourt/Academic Press, 2001.

src/MathematicalIntroductionLogic/Tuple.lean

@@ -1,2 +0,0 @@
-import MathematicalIntroductionLogic.Tuple.Basic
-import MathematicalIntroductionLogic.Tuple.Generic

src/MathematicalIntroductionLogic/Tuple/Generic.lean

@@ -1,164 +0,0 @@
-import MathematicalIntroductionLogic.Tuple.Basic
-
-/--
-The following describes a so-called "generic" tuple. Like a `Tuple`, an
-`n`-tuple is defined recursively like so:
-
-  `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩`
-
-Unlike `Tuple`, a "generic" tuple bends the syntax above further. For example,
-both tuples above are equivalent to:
-
-  `⟨⟨x₁, ..., xₘ⟩, xₘ₊₁, ..., xₙ⟩`
-
-for some `1 ≤ m ≤ n`. This distinction is purely syntactic, but necessary to
-prove certain theorems (e.g. `Chapter0.lemma_0a`). In other words, `Tuple` is an
-always-normalized variant of an `GTuple`. In general, prefer it over this when
-working within Enderton's book.
--/
-inductive GTuple : (α : Type u) → (size : Nat × Nat) → Type u where
-  | nil : GTuple α (0, 0)
-  | snoc : GTuple α (p, q) → Tuple α r → GTuple α (p + q, r)
-
-syntax (priority := high) "g[" term,* "]" : term
-
-macro_rules
-  | `(g[]) => `(GTuple.nil)
-  | `(g[$x]) => `(GTuple.snoc g[] t[$x])
-  | `(g[g[$xs:term,*], $ys:term,*]) => `(GTuple.snoc g[$xs,*] t[$ys,*])
-  | `(g[$x, $xs:term,*]) => `(GTuple.snoc g[] t[$x, $xs,*])
-
-namespace GTuple
-
-open scoped Tuple
-
--- ========================================
--- Normalization
--- ========================================
-
-/--
-Converts an `GTuple` into "normal form".
--/
-def norm : GTuple α (m, n) → Tuple α (m + n)
-  |         g[] => t[]
-  | snoc  is ts => Tuple.concat is.norm ts
-
-/--
-Normalization of an empty `GTuple` yields an empty `Tuple`.
--/
-theorem norm_nil_eq_nil : @norm α 0 0 nil = Tuple.nil :=
-  rfl
-
-/--
-Normalization of a pseudo-empty `GTuple` yields an empty `Tuple`.
--/
-theorem norm_snoc_nil_nil_eq_nil : @norm α 0 0 (snoc g[] t[]) = t[] := by
-  unfold norm norm
-  rfl
-
-/--
-Normalization elimates `snoc` when the `snd` component is `nil`.
--/
-theorem norm_snoc_nil_elim {t : GTuple α (p, q)}
-  : norm (snoc t t[]) = norm t := by
-  cases t with
-  | nil => simp; unfold norm norm; rfl
-  | snoc tf tl =>
-      simp
-      conv => lhs; unfold norm
-
-/--
-Normalization eliminates `snoc` when the `fst` component is `nil`.
--/
-theorem norm_nil_snoc_elim {ts : Tuple α n}
-  : norm (snoc g[] ts) = cast (by simp) ts := by
-  unfold norm norm
-  rw [Tuple.nil_concat_self_eq_self]
-
-/--
-Normalization distributes across `Tuple.snoc` calls.
--/
-theorem norm_snoc_snoc_norm
-  : norm (snoc as (Tuple.snoc bs b)) = Tuple.snoc (norm (snoc as bs)) b := by
-  unfold norm
-  rw [←Tuple.concat_snoc_snoc_concat]
-
-/--
-Normalizing an `GTuple` is equivalent to concatenating the normalized `fst`
-component with the `snd`.
--/
-theorem norm_snoc_eq_concat {t₁ : GTuple α (p, q)} {t₂ : Tuple α n}
-  : norm (snoc t₁ t₂) = Tuple.concat t₁.norm t₂ := by
-  conv => lhs; unfold norm
-
--- ========================================
--- Equality
--- ========================================
-
-/--
-Implements Boolean equality for `GTuple α n` provided `α` has decidable
-equality.
--/
-instance BEq [DecidableEq α] : BEq (GTuple α n) where
-  beq t₁ t₂ := t₁.norm == t₂.norm
-
--- ========================================
--- Basic API
--- ========================================
-
-/--
-Returns the number of entries in the `GTuple`.
--/
-def size (_ : GTuple α n) := n
-
-/--
-Returns the number of entries in the "shallowest" portion of the `GTuple`. For
-example, the length of `x[x[1, 2], 3, 4]` is `3`, despite its size being `4`.
--/
-def length : GTuple α n → Nat
-  |         g[] => 0
-  | snoc g[] ts => ts.size
-  | snoc   _ ts => 1 + ts.size
-
-/--
-Returns the first component of our `GTuple`. For example, the first component of
-tuple `x[x[1, 2], 3, 4]` is `t[1, 2]`.
--/
-def fst : GTuple α (m, n) → Tuple α m
-  | g[] => t[]
-  | snoc ts _ => ts.norm
-
-/--
-Given `GTuple α (m, n)`, the `fst` component is equal to an initial segment of
-size `k` of the tuple in normal form.
--/
-theorem self_fst_eq_norm_take (t : GTuple α (m, n)) : t.fst = t.norm.take m :=
-  match t with
-  | g[] => by
-    unfold fst
-    rw [Tuple.self_take_zero_eq_nil]
-    simp
-  | snoc tf tl => by
-    unfold fst
-    conv => rhs; unfold norm
-    rw [Tuple.eq_take_concat]
-    simp
-
-/--
-If the normal form of an `GTuple` is equal to a `Tuple`, the `fst` component
-must be a prefix of the `Tuple`.
--/
-theorem norm_eq_fst_eq_take {t₁ : GTuple α (m, n)} {t₂ : Tuple α (m + n)}
-  : (t₁.norm = t₂) → (t₁.fst = t₂.take m) := by
-  intro h
-  rw [self_fst_eq_norm_take, h]
-
-/--
-Returns the first component of our `GTuple`. For example, the first component of
-tuple `x[x[1, 2], 3, 4]` is `t[3, 4]`.
--/
-def snd : GTuple α (m, n) → Tuple α n
-  | g[] => t[]
-  | snoc _ ts => ts
-
-end GTuple

src/MockMockingbird.lean

@@ -1 +0,0 @@
-import MockMockingbird.Aviary

src/OneVariableCalculus.lean

@@ -1,2 +0,0 @@
-import OneVariableCalculus.Apostol
-import OneVariableCalculus.Real

src/OneVariableCalculus/Apostol.lean

@@ -1,2 +0,0 @@
-import OneVariableCalculus.Apostol.Chapter_I_3
-import OneVariableCalculus.Apostol.Exercises_I_3_12

src/OneVariableCalculus/README.md

@@ -1,4 +0,0 @@
-# One-Variable Calculus, with an Introduction to Linear Algebra
-
-Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to
-Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.

src/OneVariableCalculus/Real.lean

@@ -1,3 +0,0 @@
-import OneVariableCalculus.Real.Function
-import OneVariableCalculus.Real.Geometry
-import OneVariableCalculus.Real.Set

src/OneVariableCalculus/Real/Function.lean

@@ -1 +0,0 @@
-import OneVariableCalculus.Real.Function.Step

src/OneVariableCalculus/Real/Geometry.lean

@@ -1,3 +0,0 @@
-import OneVariableCalculus.Real.Geometry.Area
-import OneVariableCalculus.Real.Geometry.Basic
-import OneVariableCalculus.Real.Geometry.Rectangle

src/OneVariableCalculus/Real/Set.lean

@@ -1 +0,0 @@
-import OneVariableCalculus.Real.Set.Partition

src/TheoremProvingInLean.lean

@@ -1 +0,0 @@
-import TheoremProvingInLean.Avigad

src/TheoremProvingInLean/Avigad.lean

@@ -1,6 +0,0 @@
-import TheoremProvingInLean.Avigad.Chapter2
-import TheoremProvingInLean.Avigad.Chapter3
-import TheoremProvingInLean.Avigad.Chapter4
-import TheoremProvingInLean.Avigad.Chapter5
-import TheoremProvingInLean.Avigad.Chapter7
-import TheoremProvingInLean.Avigad.Chapter8

src/TheoremProvingInLean/README.md

@@ -1,3 +0,0 @@
-# Theorem Proving in Lean
-
-Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.