From fe6cb7e07440df92452262aaccb4745e0f17de8d Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 8 May 2023 13:43:54 -0600 Subject: [PATCH] Rename `Exercises` to `Bookshelf`. --- Bookshelf.lean | 4 ++++ Bookshelf/Apostol.lean | 2 ++ {Exercises => Bookshelf}/Apostol/Chapter_1_07.tex | 0 {Exercises => Bookshelf}/Apostol/Chapter_1_11.lean | 6 +++--- {Exercises => Bookshelf}/Apostol/Chapter_1_11.tex | 6 +++--- {Exercises => Bookshelf}/Apostol/Chapter_I_03.lean | 6 +++--- {Exercises => Bookshelf}/Apostol/Chapter_I_03.tex | 0 .../Apostol/images/right-triangle.png | Bin .../Apostol/images/trapezoid-cases.png | Bin Bookshelf/Avigad.lean | 6 ++++++ {Exercises => Bookshelf}/Avigad/Chapter2.lean | 6 +++--- {Exercises => Bookshelf}/Avigad/Chapter3.lean | 6 +++--- {Exercises => Bookshelf}/Avigad/Chapter4.lean | 6 +++--- {Exercises => Bookshelf}/Avigad/Chapter5.lean | 6 +++--- {Exercises => Bookshelf}/Avigad/Chapter7.lean | 6 +++--- {Exercises => Bookshelf}/Avigad/Chapter8.lean | 6 +++--- Bookshelf/Enderton.lean | 1 + {Exercises => Bookshelf}/Enderton/Chapter0.lean | 6 +++--- {Exercises => Bookshelf}/Enderton/Chapter0.tex | 4 ++-- Bookshelf/Fraleigh.lean | 1 + {Exercises => Bookshelf}/Fraleigh/Chapter1.lean | 6 +++--- Exercises.lean | 4 ---- Exercises/Apostol.lean | 2 -- Exercises/Avigad.lean | 6 ------ Exercises/Enderton.lean | 1 - Exercises/Fraleigh.lean | 1 - lakefile.lean | 2 +- 27 files changed, 50 insertions(+), 50 deletions(-) create mode 100644 Bookshelf.lean create mode 100644 Bookshelf/Apostol.lean rename {Exercises => Bookshelf}/Apostol/Chapter_1_07.tex (100%) rename {Exercises => Bookshelf}/Apostol/Chapter_1_11.lean (93%) rename {Exercises => Bookshelf}/Apostol/Chapter_1_11.tex (96%) rename {Exercises => Bookshelf}/Apostol/Chapter_I_03.lean (99%) rename {Exercises => Bookshelf}/Apostol/Chapter_I_03.tex (100%) rename {Exercises => Bookshelf}/Apostol/images/right-triangle.png (100%) rename {Exercises => Bookshelf}/Apostol/images/trapezoid-cases.png (100%) create mode 100644 Bookshelf/Avigad.lean rename {Exercises => Bookshelf}/Avigad/Chapter2.lean (96%) rename {Exercises => Bookshelf}/Avigad/Chapter3.lean (97%) rename {Exercises => Bookshelf}/Avigad/Chapter4.lean (98%) rename {Exercises => Bookshelf}/Avigad/Chapter5.lean (99%) rename {Exercises => Bookshelf}/Avigad/Chapter7.lean (98%) rename {Exercises => Bookshelf}/Avigad/Chapter8.lean (98%) create mode 100644 Bookshelf/Enderton.lean rename {Exercises => Bookshelf}/Enderton/Chapter0.lean (98%) rename {Exercises => Bookshelf}/Enderton/Chapter0.tex (84%) create mode 100644 Bookshelf/Fraleigh.lean rename {Exercises => Bookshelf}/Fraleigh/Chapter1.lean (78%) delete mode 100644 Exercises.lean delete mode 100644 Exercises/Apostol.lean delete mode 100644 Exercises/Avigad.lean delete mode 100644 Exercises/Enderton.lean delete mode 100644 Exercises/Fraleigh.lean diff --git a/Bookshelf.lean b/Bookshelf.lean new file mode 100644 index 0000000..071c927 --- /dev/null +++ b/Bookshelf.lean @@ -0,0 +1,4 @@ +import Bookshelf.Apostol +import Bookshelf.Avigad +import Bookshelf.Enderton +import Bookshelf.Fraleigh diff --git a/Bookshelf/Apostol.lean b/Bookshelf/Apostol.lean new file mode 100644 index 0000000..1f245ca --- /dev/null +++ b/Bookshelf/Apostol.lean @@ -0,0 +1,2 @@ +import Bookshelf.Apostol.Chapter_I_03 +import Bookshelf.Apostol.Chapter_1_11 \ No newline at end of file diff --git a/Exercises/Apostol/Chapter_1_07.tex b/Bookshelf/Apostol/Chapter_1_07.tex similarity index 100% rename from Exercises/Apostol/Chapter_1_07.tex rename to Bookshelf/Apostol/Chapter_1_07.tex diff --git a/Exercises/Apostol/Chapter_1_11.lean b/Bookshelf/Apostol/Chapter_1_11.lean similarity index 93% rename from Exercises/Apostol/Chapter_1_11.lean rename to Bookshelf/Apostol/Chapter_1_11.lean index d406cc6..31b2387 100644 --- a/Exercises/Apostol/Chapter_1_11.lean +++ b/Bookshelf/Apostol/Chapter_1_11.lean @@ -2,9 +2,9 @@ import Mathlib.Data.Real.Basic import Common.Real.Int -/-! # Exercises.Apostol.Exercises_1_11 -/ +/-! # Apostol.Chapter_1_11 -/ -namespace Exercises.Apostol.Exercises_1_11 +namespace Apostol.Chapter_1_11 /-! ## Exercise 4 @@ -73,4 +73,4 @@ Exercises 4(a) and (b) to the bracket on the right. -/ theorem exercise_7b : True := sorry -end Exercises.Apostol.Exercises_1_11 +end Apostol.Chapter_1_11 diff --git a/Exercises/Apostol/Chapter_1_11.tex b/Bookshelf/Apostol/Chapter_1_11.tex similarity index 96% rename from Exercises/Apostol/Chapter_1_11.tex rename to Bookshelf/Apostol/Chapter_1_11.tex index cb9564d..24061fa 100644 --- a/Exercises/Apostol/Chapter_1_11.tex +++ b/Bookshelf/Apostol/Chapter_1_11.tex @@ -5,9 +5,9 @@ \input{../../preamble} \newcommand{\link}[1]{\lean{../..} - {Exercises/Apostol/Exercises\_1\_11} - {Exercises.Apostol.Exercises\_1\_11.#1} - {Exercises\_1\_11.#1} + {Bookshelf/Apostol/Chapter\_1\_11} + {Apostol.Chapter\_1\_11.#1} + {Chapter\_1\_11.#1} } \begin{document} diff --git a/Exercises/Apostol/Chapter_I_03.lean b/Bookshelf/Apostol/Chapter_I_03.lean similarity index 99% rename from Exercises/Apostol/Chapter_I_03.lean rename to Bookshelf/Apostol/Chapter_I_03.lean index e5e4245..c0ffdd5 100644 --- a/Exercises/Apostol/Chapter_I_03.lean +++ b/Bookshelf/Apostol/Chapter_I_03.lean @@ -1,11 +1,11 @@ import Common.Real.Set -/-! # Exercises.Apostol.Chapter_I_3 +/-! # Apostol.Chapter_I_3 A Set of Axioms for the Real-Number System -/ -namespace Exercises.Apostol.Chapter_I_3 +namespace Apostol.Chapter_I_3 #check Archimedean #check Real.exists_isLUB @@ -640,4 +640,4 @@ the Archimedean property does not imply the least-upper-bound axiom. ###### TODO -/ -end Exercises.Apostol.Chapter_I_3 \ No newline at end of file +end Apostol.Chapter_I_3 \ No newline at end of file diff --git a/Exercises/Apostol/Chapter_I_03.tex b/Bookshelf/Apostol/Chapter_I_03.tex similarity index 100% rename from Exercises/Apostol/Chapter_I_03.tex rename to Bookshelf/Apostol/Chapter_I_03.tex diff --git a/Exercises/Apostol/images/right-triangle.png b/Bookshelf/Apostol/images/right-triangle.png similarity index 100% rename from Exercises/Apostol/images/right-triangle.png rename to Bookshelf/Apostol/images/right-triangle.png diff --git a/Exercises/Apostol/images/trapezoid-cases.png b/Bookshelf/Apostol/images/trapezoid-cases.png similarity index 100% rename from Exercises/Apostol/images/trapezoid-cases.png rename to Bookshelf/Apostol/images/trapezoid-cases.png diff --git a/Bookshelf/Avigad.lean b/Bookshelf/Avigad.lean new file mode 100644 index 0000000..770de9d --- /dev/null +++ b/Bookshelf/Avigad.lean @@ -0,0 +1,6 @@ +import Bookshelf.Avigad.Chapter2 +import Bookshelf.Avigad.Chapter3 +import Bookshelf.Avigad.Chapter4 +import Bookshelf.Avigad.Chapter5 +import Bookshelf.Avigad.Chapter7 +import Bookshelf.Avigad.Chapter8 diff --git a/Exercises/Avigad/Chapter2.lean b/Bookshelf/Avigad/Chapter2.lean similarity index 96% rename from Exercises/Avigad/Chapter2.lean rename to Bookshelf/Avigad/Chapter2.lean index 0220b03..d96a4d4 100644 --- a/Exercises/Avigad/Chapter2.lean +++ b/Bookshelf/Avigad/Chapter2.lean @@ -1,4 +1,4 @@ -/-! # Exercises.Avigad.Chapter2 +/-! # Avigad.Chapter2 Dependent Type Theory -/ @@ -8,7 +8,7 @@ Dependent Type Theory Define the function `Do_Twice`, as described in Section 2.4. -/ -namespace Exercises.Avigad.Chapter2 +namespace Avigad.Chapter2 namespace ex1 @@ -106,4 +106,4 @@ variable (d : ex3.vec Prop 3) end ex4 -end Exercises.Avigad.Chapter2 \ No newline at end of file +end Avigad.Chapter2 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter3.lean b/Bookshelf/Avigad/Chapter3.lean similarity index 97% rename from Exercises/Avigad/Chapter3.lean rename to Bookshelf/Avigad/Chapter3.lean index 08bd45e..b83855f 100644 --- a/Exercises/Avigad/Chapter3.lean +++ b/Bookshelf/Avigad/Chapter3.lean @@ -1,4 +1,4 @@ -/-! # Exercises.Avigad.Chapter3 +/-! # Avigad.Chapter3 Propositions and Proofs -/ @@ -8,7 +8,7 @@ Propositions and Proofs Prove the following identities. -/ -namespace Exercises.Avigad.Chapter3 +namespace Avigad.Chapter3 namespace ex1 @@ -164,4 +164,4 @@ theorem iff_not_self (hp : p) : ¬(p ↔ ¬p) := end ex3 -end Exercises.Avigad.Chapter3 \ No newline at end of file +end Avigad.Chapter3 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter4.lean b/Bookshelf/Avigad/Chapter4.lean similarity index 98% rename from Exercises/Avigad/Chapter4.lean rename to Bookshelf/Avigad/Chapter4.lean index 5066bc3..793d823 100644 --- a/Exercises/Avigad/Chapter4.lean +++ b/Bookshelf/Avigad/Chapter4.lean @@ -1,4 +1,4 @@ -/-! # Exercises.Avigad.Chapter4 +/-! # Avigad.Chapter4 Quantifiers and Equality -/ @@ -9,7 +9,7 @@ Prove these equivalences. You should also try to understand why the reverse implication is not derivable in the last example. -/ -namespace Exercises.Avigad.Chapter4 +namespace Avigad.Chapter4 namespace ex1 @@ -258,4 +258,4 @@ theorem log_mul {x y : Float} (hx : x > 0) (hy : y > 0) : end ex6 -end Exercises.Avigad.Chapter4 \ No newline at end of file +end Avigad.Chapter4 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter5.lean b/Bookshelf/Avigad/Chapter5.lean similarity index 99% rename from Exercises/Avigad/Chapter5.lean rename to Bookshelf/Avigad/Chapter5.lean index bf743ec..0829235 100644 --- a/Exercises/Avigad/Chapter5.lean +++ b/Bookshelf/Avigad/Chapter5.lean @@ -1,4 +1,4 @@ -/-! # Exercises.Avigad.Chapter5 +/-! # Avigad.Chapter5 Tactics -/ @@ -9,7 +9,7 @@ Go back to the exercises in Chapter 3 and Chapter 4 and redo as many as you can now with tactic proofs, using also `rw` and `simp` as appropriate. -/ -namespace Exercises.Avigad.Chapter5 +namespace Avigad.Chapter5 namespace ex1 @@ -461,4 +461,4 @@ theorem or_and_or_and_or (p q r : Prop) (hp : p) end ex2 -end Exercises.Avigad.Chapter5 \ No newline at end of file +end Avigad.Chapter5 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter7.lean b/Bookshelf/Avigad/Chapter7.lean similarity index 98% rename from Exercises/Avigad/Chapter7.lean rename to Bookshelf/Avigad/Chapter7.lean index 2620361..404a135 100644 --- a/Exercises/Avigad/Chapter7.lean +++ b/Bookshelf/Avigad/Chapter7.lean @@ -1,9 +1,9 @@ -/-! # Exercises.Avigad.Chapter7 +/-! # Avigad.Chapter7 Inductive Types -/ -namespace Exercises.Avigad.Chapter7 +namespace Avigad.Chapter7 /-! #### Exercise 1 @@ -217,4 +217,4 @@ def eval_foo : Foo → List Nat → Nat end ex3 -end Exercises.Avigad.Chapter7 \ No newline at end of file +end Avigad.Chapter7 \ No newline at end of file diff --git a/Exercises/Avigad/Chapter8.lean b/Bookshelf/Avigad/Chapter8.lean similarity index 98% rename from Exercises/Avigad/Chapter8.lean rename to Bookshelf/Avigad/Chapter8.lean index 49bf41b..1673b4d 100644 --- a/Exercises/Avigad/Chapter8.lean +++ b/Bookshelf/Avigad/Chapter8.lean @@ -1,9 +1,9 @@ -/-! # Exercises.Avigad.Chapter8 +/-! # Avigad.Chapter8 Induction and Recursion -/ -namespace Exercises.Avigad.Chapter8 +namespace Avigad.Chapter8 /-! #### Exercise 1 @@ -206,4 +206,4 @@ theorem fuse_eq (v : Nat → Nat) end ex5 -end Exercises.Avigad.Chapter8 \ No newline at end of file +end Avigad.Chapter8 \ No newline at end of file diff --git a/Bookshelf/Enderton.lean b/Bookshelf/Enderton.lean new file mode 100644 index 0000000..18d7966 --- /dev/null +++ b/Bookshelf/Enderton.lean @@ -0,0 +1 @@ +import Bookshelf.Enderton.Chapter0 \ No newline at end of file diff --git a/Exercises/Enderton/Chapter0.lean b/Bookshelf/Enderton/Chapter0.lean similarity index 98% rename from Exercises/Enderton/Chapter0.lean rename to Bookshelf/Enderton/Chapter0.lean index c852644..d7f1c36 100644 --- a/Exercises/Enderton/Chapter0.lean +++ b/Bookshelf/Enderton/Chapter0.lean @@ -1,11 +1,11 @@ import Common.LTuple.Basic -/-! # Exercises.Enderton.Chapter0 +/-! # Enderton.Chapter0 Useful Facts About Sets -/ -namespace Exercises.Enderton.Chapter0 +namespace Enderton.Chapter0 /-- The following describes a so-called "generic" tuple. Like an `LTuple`, a generic @@ -275,4 +275,4 @@ theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k)) end -end Exercises.Enderton.Chapter0 \ No newline at end of file +end Enderton.Chapter0 \ No newline at end of file diff --git a/Exercises/Enderton/Chapter0.tex b/Bookshelf/Enderton/Chapter0.tex similarity index 84% rename from Exercises/Enderton/Chapter0.tex rename to Bookshelf/Enderton/Chapter0.tex index c2817c6..d25cd7b 100644 --- a/Exercises/Enderton/Chapter0.tex +++ b/Bookshelf/Enderton/Chapter0.tex @@ -3,8 +3,8 @@ \input{../../preamble} \newcommand{\link}[1]{\lean{../..} - {Exercises/Enderton/Chapter0} - {Exercises.Enderton.Chapter0.#1} + {Bookshelf/Enderton/Chapter0} + {Enderton.Chapter0.#1} {Chapter0.#1} } diff --git a/Bookshelf/Fraleigh.lean b/Bookshelf/Fraleigh.lean new file mode 100644 index 0000000..2e0798a --- /dev/null +++ b/Bookshelf/Fraleigh.lean @@ -0,0 +1 @@ +import Bookshelf.Fraleigh.Chapter1 \ No newline at end of file diff --git a/Exercises/Fraleigh/Chapter1.lean b/Bookshelf/Fraleigh/Chapter1.lean similarity index 78% rename from Exercises/Fraleigh/Chapter1.lean rename to Bookshelf/Fraleigh/Chapter1.lean index 8b2f2b1..ce05148 100644 --- a/Exercises/Fraleigh/Chapter1.lean +++ b/Bookshelf/Fraleigh/Chapter1.lean @@ -1,11 +1,11 @@ import Mathlib.Data.Complex.Basic -/-! # Exercises.Fraleign.Chapter1 +/-! # Fraleign.Chapter1 Introduction and Examples -/ -namespace Exercises.Fraleign.Chapter1 +namespace Fraleign.Chapter1 open Complex open HPow @@ -21,4 +21,4 @@ theorem exercise1 : I^3 = 0 + (-1) * I := calc = I * (I * hPow I 1) := rfl _ = 0 + (-1) * I := by simp -end Exercises.Fraleign.Chapter1 \ No newline at end of file +end Fraleign.Chapter1 \ No newline at end of file diff --git a/Exercises.lean b/Exercises.lean deleted file mode 100644 index 68cc8dd..0000000 --- a/Exercises.lean +++ /dev/null @@ -1,4 +0,0 @@ -import Exercises.Apostol -import Exercises.Avigad -import Exercises.Enderton -import Exercises.Fraleigh diff --git a/Exercises/Apostol.lean b/Exercises/Apostol.lean deleted file mode 100644 index e8d8fc4..0000000 --- a/Exercises/Apostol.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Exercises.Apostol.Chapter_I_03 -import Exercises.Apostol.Chapter_1_11 \ No newline at end of file diff --git a/Exercises/Avigad.lean b/Exercises/Avigad.lean deleted file mode 100644 index 86a247f..0000000 --- a/Exercises/Avigad.lean +++ /dev/null @@ -1,6 +0,0 @@ -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/Exercises/Enderton.lean b/Exercises/Enderton.lean deleted file mode 100644 index 0fcf796..0000000 --- a/Exercises/Enderton.lean +++ /dev/null @@ -1 +0,0 @@ -import Exercises.Enderton.Chapter0 \ No newline at end of file diff --git a/Exercises/Fraleigh.lean b/Exercises/Fraleigh.lean deleted file mode 100644 index 8126b2f..0000000 --- a/Exercises/Fraleigh.lean +++ /dev/null @@ -1 +0,0 @@ -import Exercises.Fraleigh.Chapter1 \ No newline at end of file diff --git a/lakefile.lean b/lakefile.lean index 6464469..1ff5e09 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -16,7 +16,7 @@ require «doc-gen4» from git @[default_target] lean_lib «Bookshelf» { - roots := #[`Common, `Exercises] + roots := #[`Bookshelf, `Common] } /--