From ad9684f53ec2eee7371f39e8d2f632806ee4e941 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 4 May 2023 15:05:13 -0600 Subject: [PATCH] Reorganize project once more, consolidating more into `Bookshelf`. --- src/Bookshelf.lean => Bookshelf.lean | 1 + Bookshelf/Combinator.lean | 1 + .../Combinator}/Aviary.lean | 0 .../Combinator}/Aviary.tex | 3 +- Bookshelf/LTuple.lean | 1 + .../Tuple => Bookshelf/LTuple}/Basic.lean | 102 +++---- {src/Bookshelf => Bookshelf}/List.lean | 0 {src/Bookshelf => Bookshelf}/List/Basic.lean | 0 {src/Bookshelf => Bookshelf}/Real.lean | 2 + {src/Bookshelf => Bookshelf}/Real/Basic.lean | 0 Bookshelf/Real/Function.lean | 1 + .../Real/Function/Step.lean | 2 +- Bookshelf/Real/Geometry.lean | 3 + .../Real/Geometry/Area.lean | 9 +- .../Real/Geometry/Basic.lean | 0 .../Real/Geometry/Rectangle.lean | 2 +- .../Real/Rational.lean | 0 .../Real/Sequence.lean | 0 .../Bookshelf => Bookshelf}/Real/Sequence.tex | 4 +- .../Real/Sequence/Arithmetic.lean | 0 .../Real/Sequence/Geometric.lean | 0 Bookshelf/Real/Set.lean | 3 + .../Real/Set/Basic.lean | 0 .../Real/Set/Interval.lean | 0 .../Real/Set/Partition.lean | 0 Exercises.lean | 4 + Exercises/Apostol.lean | 4 + .../Apostol/Chapter_I_3.lean | 0 .../Apostol/Chapter_I_3.tex | 2 +- .../Apostol/Exercises_I_3_12.lean | 2 +- Exercises/Avigad.lean | 7 + .../Avigad/Chapter2.lean | 2 + .../Avigad/Chapter3.lean | 0 .../Avigad/Chapter4.lean | 0 .../Avigad/Chapter5.lean | 0 .../Avigad/Chapter7.lean | 0 .../Avigad/Chapter8.lean | 0 Exercises/Enderton.lean | 3 + Exercises/Enderton/Chapter0.lean | 287 ++++++++++++++++++ .../Enderton/Chapter0.tex | 2 +- Exercises/Fraleigh.lean | 2 + .../Fraleigh/Chapter1.lean | 0 lake-manifest.json | 4 +- lakefile.lean | 12 +- src/Bookshelf/Real/Set.lean | 2 - src/FirstCourseAbstractAlgebra.lean | 1 - src/FirstCourseAbstractAlgebra/Fraleigh.lean | 1 - src/FirstCourseAbstractAlgebra/README.md | 3 - src/MathematicalIntroductionLogic.lean | 2 - .../Enderton.lean | 1 - .../Enderton/Chapter0.lean | 106 ------- src/MathematicalIntroductionLogic/README.md | 4 - src/MathematicalIntroductionLogic/Tuple.lean | 2 - .../Tuple/Generic.lean | 164 ---------- src/MockMockingbird.lean | 1 - src/OneVariableCalculus.lean | 2 - src/OneVariableCalculus/Apostol.lean | 2 - src/OneVariableCalculus/README.md | 4 - src/OneVariableCalculus/Real.lean | 3 - src/OneVariableCalculus/Real/Function.lean | 1 - src/OneVariableCalculus/Real/Geometry.lean | 3 - src/OneVariableCalculus/Real/Set.lean | 1 - src/TheoremProvingInLean.lean | 1 - src/TheoremProvingInLean/Avigad.lean | 6 - src/TheoremProvingInLean/README.md | 3 - 65 files changed, 382 insertions(+), 396 deletions(-) rename src/Bookshelf.lean => Bookshelf.lean (61%) create mode 100644 Bookshelf/Combinator.lean rename {src/MockMockingbird => Bookshelf/Combinator}/Aviary.lean (100%) rename {src/MockMockingbird => Bookshelf/Combinator}/Aviary.tex (93%) create mode 100644 Bookshelf/LTuple.lean rename {src/MathematicalIntroductionLogic/Tuple => Bookshelf/LTuple}/Basic.lean (66%) rename {src/Bookshelf => Bookshelf}/List.lean (100%) rename {src/Bookshelf => Bookshelf}/List/Basic.lean (100%) rename {src/Bookshelf => Bookshelf}/Real.lean (65%) rename {src/Bookshelf => Bookshelf}/Real/Basic.lean (100%) create mode 100644 Bookshelf/Real/Function.lean rename {src/OneVariableCalculus => Bookshelf}/Real/Function/Step.lean (96%) create mode 100644 Bookshelf/Real/Geometry.lean rename {src/OneVariableCalculus => Bookshelf}/Real/Geometry/Area.lean (96%) rename {src/OneVariableCalculus => Bookshelf}/Real/Geometry/Basic.lean (100%) rename {src/OneVariableCalculus => Bookshelf}/Real/Geometry/Rectangle.lean (98%) rename {src/Bookshelf => Bookshelf}/Real/Rational.lean (100%) rename {src/Bookshelf => Bookshelf}/Real/Sequence.lean (100%) rename {src/Bookshelf => Bookshelf}/Real/Sequence.tex (79%) rename {src/Bookshelf => Bookshelf}/Real/Sequence/Arithmetic.lean (100%) rename {src/Bookshelf => Bookshelf}/Real/Sequence/Geometric.lean (100%) create mode 100644 Bookshelf/Real/Set.lean rename {src/Bookshelf => Bookshelf}/Real/Set/Basic.lean (100%) rename {src/Bookshelf => Bookshelf}/Real/Set/Interval.lean (100%) rename {src/OneVariableCalculus => Bookshelf}/Real/Set/Partition.lean (100%) create mode 100644 Exercises.lean create mode 100644 Exercises/Apostol.lean rename {src/OneVariableCalculus => Exercises}/Apostol/Chapter_I_3.lean (100%) rename {src/OneVariableCalculus => Exercises}/Apostol/Chapter_I_3.tex (96%) rename {src/OneVariableCalculus => Exercises}/Apostol/Exercises_I_3_12.lean (99%) create mode 100644 Exercises/Avigad.lean rename {src/TheoremProvingInLean => Exercises}/Avigad/Chapter2.lean (99%) rename {src/TheoremProvingInLean => Exercises}/Avigad/Chapter3.lean (100%) rename {src/TheoremProvingInLean => Exercises}/Avigad/Chapter4.lean (100%) rename {src/TheoremProvingInLean => Exercises}/Avigad/Chapter5.lean (100%) rename {src/TheoremProvingInLean => Exercises}/Avigad/Chapter7.lean (100%) rename {src/TheoremProvingInLean => Exercises}/Avigad/Chapter8.lean (100%) create mode 100644 Exercises/Enderton.lean create mode 100644 Exercises/Enderton/Chapter0.lean rename {src/MathematicalIntroductionLogic => Exercises}/Enderton/Chapter0.tex (76%) create mode 100644 Exercises/Fraleigh.lean rename {src/FirstCourseAbstractAlgebra => Exercises}/Fraleigh/Chapter1.lean (100%) delete mode 100644 src/Bookshelf/Real/Set.lean delete mode 100644 src/FirstCourseAbstractAlgebra.lean delete mode 100644 src/FirstCourseAbstractAlgebra/Fraleigh.lean delete mode 100644 src/FirstCourseAbstractAlgebra/README.md delete mode 100644 src/MathematicalIntroductionLogic.lean delete mode 100644 src/MathematicalIntroductionLogic/Enderton.lean delete mode 100644 src/MathematicalIntroductionLogic/Enderton/Chapter0.lean delete mode 100644 src/MathematicalIntroductionLogic/README.md delete mode 100644 src/MathematicalIntroductionLogic/Tuple.lean delete mode 100644 src/MathematicalIntroductionLogic/Tuple/Generic.lean delete mode 100644 src/MockMockingbird.lean delete mode 100644 src/OneVariableCalculus.lean delete mode 100644 src/OneVariableCalculus/Apostol.lean delete mode 100644 src/OneVariableCalculus/README.md delete mode 100644 src/OneVariableCalculus/Real.lean delete mode 100644 src/OneVariableCalculus/Real/Function.lean delete mode 100644 src/OneVariableCalculus/Real/Geometry.lean delete mode 100644 src/OneVariableCalculus/Real/Set.lean delete mode 100644 src/TheoremProvingInLean.lean delete mode 100644 src/TheoremProvingInLean/Avigad.lean delete mode 100644 src/TheoremProvingInLean/README.md diff --git a/src/Bookshelf.lean b/Bookshelf.lean similarity index 61% rename from src/Bookshelf.lean rename to Bookshelf.lean index 71ccb30..4cd3a3c 100644 --- a/src/Bookshelf.lean +++ b/Bookshelf.lean @@ -1,2 +1,3 @@ +import Bookshelf.Combinator import Bookshelf.List import Bookshelf.Real diff --git a/Bookshelf/Combinator.lean b/Bookshelf/Combinator.lean new file mode 100644 index 0000000..fc825e4 --- /dev/null +++ b/Bookshelf/Combinator.lean @@ -0,0 +1 @@ +import Bookshelf.Combinator.Aviary \ No newline at end of file diff --git a/src/MockMockingbird/Aviary.lean b/Bookshelf/Combinator/Aviary.lean similarity index 100% rename from src/MockMockingbird/Aviary.lean rename to Bookshelf/Combinator/Aviary.lean diff --git a/src/MockMockingbird/Aviary.tex b/Bookshelf/Combinator/Aviary.tex similarity index 93% rename from src/MockMockingbird/Aviary.tex rename to Bookshelf/Combinator/Aviary.tex index fa9d65d..8529a85 100644 --- a/src/MockMockingbird/Aviary.tex +++ b/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)$ diff --git a/Bookshelf/LTuple.lean b/Bookshelf/LTuple.lean new file mode 100644 index 0000000..3eadafb --- /dev/null +++ b/Bookshelf/LTuple.lean @@ -0,0 +1 @@ +import Bookshelf.LTuple.Basic \ No newline at end of file diff --git a/src/MathematicalIntroductionLogic/Tuple/Basic.lean b/Bookshelf/LTuple/Basic.lean similarity index 66% rename from src/MathematicalIntroductionLogic/Tuple/Basic.lean rename to Bookshelf/LTuple/Basic.lean index 84d6056..d925bce 100644 --- a/src/MathematicalIntroductionLogic/Tuple/Basic.lean +++ b/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 diff --git a/src/Bookshelf/List.lean b/Bookshelf/List.lean similarity index 100% rename from src/Bookshelf/List.lean rename to Bookshelf/List.lean diff --git a/src/Bookshelf/List/Basic.lean b/Bookshelf/List/Basic.lean similarity index 100% rename from src/Bookshelf/List/Basic.lean rename to Bookshelf/List/Basic.lean diff --git a/src/Bookshelf/Real.lean b/Bookshelf/Real.lean similarity index 65% rename from src/Bookshelf/Real.lean rename to Bookshelf/Real.lean index e118fed..b9ab721 100644 --- a/src/Bookshelf/Real.lean +++ b/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 diff --git a/src/Bookshelf/Real/Basic.lean b/Bookshelf/Real/Basic.lean similarity index 100% rename from src/Bookshelf/Real/Basic.lean rename to Bookshelf/Real/Basic.lean diff --git a/Bookshelf/Real/Function.lean b/Bookshelf/Real/Function.lean new file mode 100644 index 0000000..f08462d --- /dev/null +++ b/Bookshelf/Real/Function.lean @@ -0,0 +1 @@ +import Bookshelf.Real.Function.Step \ No newline at end of file diff --git a/src/OneVariableCalculus/Real/Function/Step.lean b/Bookshelf/Real/Function/Step.lean similarity index 96% rename from src/OneVariableCalculus/Real/Function/Step.lean rename to Bookshelf/Real/Function/Step.lean index d11e031..03d9a2a 100644 --- a/src/OneVariableCalculus/Real/Function/Step.lean +++ b/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 diff --git a/Bookshelf/Real/Geometry.lean b/Bookshelf/Real/Geometry.lean new file mode 100644 index 0000000..e890849 --- /dev/null +++ b/Bookshelf/Real/Geometry.lean @@ -0,0 +1,3 @@ +import Bookshelf.Real.Geometry.Area +import Bookshelf.Real.Geometry.Basic +import Bookshelf.Real.Geometry.Rectangle \ No newline at end of file diff --git a/src/OneVariableCalculus/Real/Geometry/Area.lean b/Bookshelf/Real/Geometry/Area.lean similarity index 96% rename from src/OneVariableCalculus/Real/Geometry/Area.lean rename to Bookshelf/Real/Geometry/Area.lean index 0286eeb..5d80233 100644 --- a/src/OneVariableCalculus/Real/Geometry/Area.lean +++ b/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 diff --git a/src/OneVariableCalculus/Real/Geometry/Basic.lean b/Bookshelf/Real/Geometry/Basic.lean similarity index 100% rename from src/OneVariableCalculus/Real/Geometry/Basic.lean rename to Bookshelf/Real/Geometry/Basic.lean diff --git a/src/OneVariableCalculus/Real/Geometry/Rectangle.lean b/Bookshelf/Real/Geometry/Rectangle.lean similarity index 98% rename from src/OneVariableCalculus/Real/Geometry/Rectangle.lean rename to Bookshelf/Real/Geometry/Rectangle.lean index 6d6c7ef..7dbc33a 100644 --- a/src/OneVariableCalculus/Real/Geometry/Rectangle.lean +++ b/Bookshelf/Real/Geometry/Rectangle.lean @@ -1,4 +1,4 @@ -import OneVariableCalculus.Real.Geometry.Basic +import Bookshelf.Real.Geometry.Basic namespace Real diff --git a/src/Bookshelf/Real/Rational.lean b/Bookshelf/Real/Rational.lean similarity index 100% rename from src/Bookshelf/Real/Rational.lean rename to Bookshelf/Real/Rational.lean diff --git a/src/Bookshelf/Real/Sequence.lean b/Bookshelf/Real/Sequence.lean similarity index 100% rename from src/Bookshelf/Real/Sequence.lean rename to Bookshelf/Real/Sequence.lean diff --git a/src/Bookshelf/Real/Sequence.tex b/Bookshelf/Real/Sequence.tex similarity index 79% rename from src/Bookshelf/Real/Sequence.tex rename to Bookshelf/Real/Sequence.tex index ee233ce..149244f 100644 --- a/src/Bookshelf/Real/Sequence.tex +++ b/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} diff --git a/src/Bookshelf/Real/Sequence/Arithmetic.lean b/Bookshelf/Real/Sequence/Arithmetic.lean similarity index 100% rename from src/Bookshelf/Real/Sequence/Arithmetic.lean rename to Bookshelf/Real/Sequence/Arithmetic.lean diff --git a/src/Bookshelf/Real/Sequence/Geometric.lean b/Bookshelf/Real/Sequence/Geometric.lean similarity index 100% rename from src/Bookshelf/Real/Sequence/Geometric.lean rename to Bookshelf/Real/Sequence/Geometric.lean diff --git a/Bookshelf/Real/Set.lean b/Bookshelf/Real/Set.lean new file mode 100644 index 0000000..9c77974 --- /dev/null +++ b/Bookshelf/Real/Set.lean @@ -0,0 +1,3 @@ +import Bookshelf.Real.Set.Basic +import Bookshelf.Real.Set.Interval +import Bookshelf.Real.Set.Partition \ No newline at end of file diff --git a/src/Bookshelf/Real/Set/Basic.lean b/Bookshelf/Real/Set/Basic.lean similarity index 100% rename from src/Bookshelf/Real/Set/Basic.lean rename to Bookshelf/Real/Set/Basic.lean diff --git a/src/Bookshelf/Real/Set/Interval.lean b/Bookshelf/Real/Set/Interval.lean similarity index 100% rename from src/Bookshelf/Real/Set/Interval.lean rename to Bookshelf/Real/Set/Interval.lean diff --git a/src/OneVariableCalculus/Real/Set/Partition.lean b/Bookshelf/Real/Set/Partition.lean similarity index 100% rename from src/OneVariableCalculus/Real/Set/Partition.lean rename to Bookshelf/Real/Set/Partition.lean diff --git a/Exercises.lean b/Exercises.lean new file mode 100644 index 0000000..68cc8dd --- /dev/null +++ b/Exercises.lean @@ -0,0 +1,4 @@ +import Exercises.Apostol +import Exercises.Avigad +import Exercises.Enderton +import Exercises.Fraleigh diff --git a/Exercises/Apostol.lean b/Exercises/Apostol.lean new file mode 100644 index 0000000..c8d7411 --- /dev/null +++ b/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 diff --git a/src/OneVariableCalculus/Apostol/Chapter_I_3.lean b/Exercises/Apostol/Chapter_I_3.lean similarity index 100% rename from src/OneVariableCalculus/Apostol/Chapter_I_3.lean rename to Exercises/Apostol/Chapter_I_3.lean diff --git a/src/OneVariableCalculus/Apostol/Chapter_I_3.tex b/Exercises/Apostol/Chapter_I_3.tex similarity index 96% rename from src/OneVariableCalculus/Apostol/Chapter_I_3.tex rename to Exercises/Apostol/Chapter_I_3.tex index 183b80a..d992d7d 100644 --- a/src/OneVariableCalculus/Apostol/Chapter_I_3.tex +++ b/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} diff --git a/src/OneVariableCalculus/Apostol/Exercises_I_3_12.lean b/Exercises/Apostol/Exercises_I_3_12.lean similarity index 99% rename from src/OneVariableCalculus/Apostol/Exercises_I_3_12.lean rename to Exercises/Apostol/Exercises_I_3_12.lean index ce41d99..16743d4 100644 --- a/src/OneVariableCalculus/Apostol/Exercises_I_3_12.lean +++ b/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 diff --git a/Exercises/Avigad.lean b/Exercises/Avigad.lean new file mode 100644 index 0000000..2bae288 --- /dev/null +++ b/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 diff --git a/src/TheoremProvingInLean/Avigad/Chapter2.lean b/Exercises/Avigad/Chapter2.lean similarity index 99% rename from src/TheoremProvingInLean/Avigad/Chapter2.lean rename to Exercises/Avigad/Chapter2.lean index bfa62a3..7add927 100644 --- a/src/TheoremProvingInLean/Avigad/Chapter2.lean +++ b/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 : α × β → γ) : (α → β → γ) := diff --git a/src/TheoremProvingInLean/Avigad/Chapter3.lean b/Exercises/Avigad/Chapter3.lean similarity index 100% rename from src/TheoremProvingInLean/Avigad/Chapter3.lean rename to Exercises/Avigad/Chapter3.lean diff --git a/src/TheoremProvingInLean/Avigad/Chapter4.lean b/Exercises/Avigad/Chapter4.lean similarity index 100% rename from src/TheoremProvingInLean/Avigad/Chapter4.lean rename to Exercises/Avigad/Chapter4.lean diff --git a/src/TheoremProvingInLean/Avigad/Chapter5.lean b/Exercises/Avigad/Chapter5.lean similarity index 100% rename from src/TheoremProvingInLean/Avigad/Chapter5.lean rename to Exercises/Avigad/Chapter5.lean diff --git a/src/TheoremProvingInLean/Avigad/Chapter7.lean b/Exercises/Avigad/Chapter7.lean similarity index 100% rename from src/TheoremProvingInLean/Avigad/Chapter7.lean rename to Exercises/Avigad/Chapter7.lean diff --git a/src/TheoremProvingInLean/Avigad/Chapter8.lean b/Exercises/Avigad/Chapter8.lean similarity index 100% rename from src/TheoremProvingInLean/Avigad/Chapter8.lean rename to Exercises/Avigad/Chapter8.lean diff --git a/Exercises/Enderton.lean b/Exercises/Enderton.lean new file mode 100644 index 0000000..cbc3de6 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/Exercises/Enderton/Chapter0.lean b/Exercises/Enderton/Chapter0.lean new file mode 100644 index 0000000..c15f625 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/MathematicalIntroductionLogic/Enderton/Chapter0.tex b/Exercises/Enderton/Chapter0.tex similarity index 76% rename from src/MathematicalIntroductionLogic/Enderton/Chapter0.tex rename to Exercises/Enderton/Chapter0.tex index baa5b10..56da410 100644 --- a/src/MathematicalIntroductionLogic/Enderton/Chapter0.tex +++ b/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} diff --git a/Exercises/Fraleigh.lean b/Exercises/Fraleigh.lean new file mode 100644 index 0000000..6d561ac --- /dev/null +++ b/Exercises/Fraleigh.lean @@ -0,0 +1,2 @@ +-- Fraleigh, John B. A First Course in Abstract Algebra, n.d. +import Exercises.Fraleigh.Chapter1 \ No newline at end of file diff --git a/src/FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean b/Exercises/Fraleigh/Chapter1.lean similarity index 100% rename from src/FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean rename to Exercises/Fraleigh/Chapter1.lean diff --git a/lake-manifest.json b/lake-manifest.json index ba74076..1088b4c 100644 --- a/lake-manifest.json +++ b/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, diff --git a/lakefile.lean b/lakefile.lean index b473370..f66e9f4 100644 --- a/lakefile.lean +++ b/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] } /-- diff --git a/src/Bookshelf/Real/Set.lean b/src/Bookshelf/Real/Set.lean deleted file mode 100644 index e939cfe..0000000 --- a/src/Bookshelf/Real/Set.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Bookshelf.Real.Set.Basic -import Bookshelf.Real.Set.Interval \ No newline at end of file diff --git a/src/FirstCourseAbstractAlgebra.lean b/src/FirstCourseAbstractAlgebra.lean deleted file mode 100644 index 17778be..0000000 --- a/src/FirstCourseAbstractAlgebra.lean +++ /dev/null @@ -1 +0,0 @@ -import FirstCourseAbstractAlgebra.Fraleigh \ No newline at end of file diff --git a/src/FirstCourseAbstractAlgebra/Fraleigh.lean b/src/FirstCourseAbstractAlgebra/Fraleigh.lean deleted file mode 100644 index c0d0c22..0000000 --- a/src/FirstCourseAbstractAlgebra/Fraleigh.lean +++ /dev/null @@ -1 +0,0 @@ -import FirstCourseAbstractAlgebra.Fraleigh.Chapter1 \ No newline at end of file diff --git a/src/FirstCourseAbstractAlgebra/README.md b/src/FirstCourseAbstractAlgebra/README.md deleted file mode 100644 index 21cacc2..0000000 --- a/src/FirstCourseAbstractAlgebra/README.md +++ /dev/null @@ -1,3 +0,0 @@ -# A First Course in Abstract Algebra - -Fraleigh, John B. A First Course in Abstract Algebra, n.d. diff --git a/src/MathematicalIntroductionLogic.lean b/src/MathematicalIntroductionLogic.lean deleted file mode 100644 index bb841aa..0000000 --- a/src/MathematicalIntroductionLogic.lean +++ /dev/null @@ -1,2 +0,0 @@ -import MathematicalIntroductionLogic.Enderton -import MathematicalIntroductionLogic.Tuple \ No newline at end of file diff --git a/src/MathematicalIntroductionLogic/Enderton.lean b/src/MathematicalIntroductionLogic/Enderton.lean deleted file mode 100644 index c2fb97c..0000000 --- a/src/MathematicalIntroductionLogic/Enderton.lean +++ /dev/null @@ -1 +0,0 @@ -import MathematicalIntroductionLogic.Enderton.Chapter0 \ No newline at end of file diff --git a/src/MathematicalIntroductionLogic/Enderton/Chapter0.lean b/src/MathematicalIntroductionLogic/Enderton/Chapter0.lean deleted file mode 100644 index e0ec96a..0000000 --- a/src/MathematicalIntroductionLogic/Enderton/Chapter0.lean +++ /dev/null @@ -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₂ diff --git a/src/MathematicalIntroductionLogic/README.md b/src/MathematicalIntroductionLogic/README.md deleted file mode 100644 index abcd6ee..0000000 --- a/src/MathematicalIntroductionLogic/README.md +++ /dev/null @@ -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. diff --git a/src/MathematicalIntroductionLogic/Tuple.lean b/src/MathematicalIntroductionLogic/Tuple.lean deleted file mode 100644 index 21e54af..0000000 --- a/src/MathematicalIntroductionLogic/Tuple.lean +++ /dev/null @@ -1,2 +0,0 @@ -import MathematicalIntroductionLogic.Tuple.Basic -import MathematicalIntroductionLogic.Tuple.Generic diff --git a/src/MathematicalIntroductionLogic/Tuple/Generic.lean b/src/MathematicalIntroductionLogic/Tuple/Generic.lean deleted file mode 100644 index 77fd19a..0000000 --- a/src/MathematicalIntroductionLogic/Tuple/Generic.lean +++ /dev/null @@ -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 diff --git a/src/MockMockingbird.lean b/src/MockMockingbird.lean deleted file mode 100644 index accd31b..0000000 --- a/src/MockMockingbird.lean +++ /dev/null @@ -1 +0,0 @@ -import MockMockingbird.Aviary \ No newline at end of file diff --git a/src/OneVariableCalculus.lean b/src/OneVariableCalculus.lean deleted file mode 100644 index 95d20f4..0000000 --- a/src/OneVariableCalculus.lean +++ /dev/null @@ -1,2 +0,0 @@ -import OneVariableCalculus.Apostol -import OneVariableCalculus.Real \ No newline at end of file diff --git a/src/OneVariableCalculus/Apostol.lean b/src/OneVariableCalculus/Apostol.lean deleted file mode 100644 index f1c820b..0000000 --- a/src/OneVariableCalculus/Apostol.lean +++ /dev/null @@ -1,2 +0,0 @@ -import OneVariableCalculus.Apostol.Chapter_I_3 -import OneVariableCalculus.Apostol.Exercises_I_3_12 diff --git a/src/OneVariableCalculus/README.md b/src/OneVariableCalculus/README.md deleted file mode 100644 index 3fdafc8..0000000 --- a/src/OneVariableCalculus/README.md +++ /dev/null @@ -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. \ No newline at end of file diff --git a/src/OneVariableCalculus/Real.lean b/src/OneVariableCalculus/Real.lean deleted file mode 100644 index 47da635..0000000 --- a/src/OneVariableCalculus/Real.lean +++ /dev/null @@ -1,3 +0,0 @@ -import OneVariableCalculus.Real.Function -import OneVariableCalculus.Real.Geometry -import OneVariableCalculus.Real.Set \ No newline at end of file diff --git a/src/OneVariableCalculus/Real/Function.lean b/src/OneVariableCalculus/Real/Function.lean deleted file mode 100644 index 9680650..0000000 --- a/src/OneVariableCalculus/Real/Function.lean +++ /dev/null @@ -1 +0,0 @@ -import OneVariableCalculus.Real.Function.Step \ No newline at end of file diff --git a/src/OneVariableCalculus/Real/Geometry.lean b/src/OneVariableCalculus/Real/Geometry.lean deleted file mode 100644 index 157ca14..0000000 --- a/src/OneVariableCalculus/Real/Geometry.lean +++ /dev/null @@ -1,3 +0,0 @@ -import OneVariableCalculus.Real.Geometry.Area -import OneVariableCalculus.Real.Geometry.Basic -import OneVariableCalculus.Real.Geometry.Rectangle \ No newline at end of file diff --git a/src/OneVariableCalculus/Real/Set.lean b/src/OneVariableCalculus/Real/Set.lean deleted file mode 100644 index 286f6db..0000000 --- a/src/OneVariableCalculus/Real/Set.lean +++ /dev/null @@ -1 +0,0 @@ -import OneVariableCalculus.Real.Set.Partition \ No newline at end of file diff --git a/src/TheoremProvingInLean.lean b/src/TheoremProvingInLean.lean deleted file mode 100644 index 07435c6..0000000 --- a/src/TheoremProvingInLean.lean +++ /dev/null @@ -1 +0,0 @@ -import TheoremProvingInLean.Avigad diff --git a/src/TheoremProvingInLean/Avigad.lean b/src/TheoremProvingInLean/Avigad.lean deleted file mode 100644 index 7b091f1..0000000 --- a/src/TheoremProvingInLean/Avigad.lean +++ /dev/null @@ -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 diff --git a/src/TheoremProvingInLean/README.md b/src/TheoremProvingInLean/README.md deleted file mode 100644 index e370109..0000000 --- a/src/TheoremProvingInLean/README.md +++ /dev/null @@ -1,3 +0,0 @@ -# Theorem Proving in Lean - -Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.