From acb301a5692abcec08cb593019a5e1f8ebc2561a Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 20 Apr 2023 13:19:56 -0600 Subject: [PATCH] Use `Bookshelf` instead of `Common`. --- common/Common/List.lean | 1 - common/Common/Real.lean | 5 ----- common/Common/Real/Function.lean | 1 - common/Common/Real/Geometry.lean | 2 -- common/Common/Real/Sequence.lean | 2 -- common/Common/Real/Set.lean | 3 --- first-course-abstract-algebra/lake-manifest.json | 6 +++--- first-course-abstract-algebra/lakefile.lean | 2 +- mathematical-introduction-logic/Enderton/Chapter0.lean | 10 +++++----- mathematical-introduction-logic/lake-manifest.json | 6 +++--- mathematical-introduction-logic/lakefile.lean | 2 +- one-variable-calculus/Apostol/Chapter_1_6.lean | 4 ++-- one-variable-calculus/Apostol/Chapter_I_3.lean | 2 +- one-variable-calculus/lake-manifest.json | 6 +++--- one-variable-calculus/lakefile.lean | 2 +- common/Common.lean => shared/Bookshelf.lean | 0 shared/Bookshelf/List.lean | 1 + {common/Common => shared/Bookshelf}/List/Basic.lean | 0 shared/Bookshelf/Real.lean | 5 +++++ {common/Common => shared/Bookshelf}/Real/Basic.lean | 0 shared/Bookshelf/Real/Function.lean | 1 + .../Bookshelf}/Real/Function/Step.lean | 6 +++--- shared/Bookshelf/Real/Geometry.lean | 2 ++ .../Bookshelf}/Real/Geometry/Basic.lean | 4 ++-- .../Bookshelf}/Real/Geometry/Rectangle.lean | 4 ++-- shared/Bookshelf/Real/Sequence.lean | 2 ++ {common/Common => shared/Bookshelf}/Real/Sequence.tex | 0 .../Bookshelf}/Real/Sequence/Arithmetic.lean | 0 .../Bookshelf}/Real/Sequence/Geometric.lean | 0 shared/Bookshelf/Real/Set.lean | 3 +++ .../Common => shared/Bookshelf}/Real/Set/Basic.lean | 0 .../Common => shared/Bookshelf}/Real/Set/Interval.lean | 0 .../Bookshelf}/Real/Set/Partition.lean | 6 +++--- {common/Common => shared/Bookshelf}/Tuple.lean | 0 {common => shared}/lake-manifest.json | 0 {common => shared}/lakefile.lean | 4 ++-- {common => shared}/lean-toolchain | 0 {common => shared}/preamble.tex | 0 38 files changed, 46 insertions(+), 46 deletions(-) delete mode 100644 common/Common/List.lean delete mode 100644 common/Common/Real.lean delete mode 100644 common/Common/Real/Function.lean delete mode 100644 common/Common/Real/Geometry.lean delete mode 100644 common/Common/Real/Sequence.lean delete mode 100644 common/Common/Real/Set.lean rename common/Common.lean => shared/Bookshelf.lean (100%) create mode 100644 shared/Bookshelf/List.lean rename {common/Common => shared/Bookshelf}/List/Basic.lean (100%) create mode 100644 shared/Bookshelf/Real.lean rename {common/Common => shared/Bookshelf}/Real/Basic.lean (100%) create mode 100644 shared/Bookshelf/Real/Function.lean rename {common/Common => shared/Bookshelf}/Real/Function/Step.lean (91%) create mode 100644 shared/Bookshelf/Real/Geometry.lean rename {common/Common => shared/Bookshelf}/Real/Geometry/Basic.lean (97%) rename {common/Common => shared/Bookshelf}/Real/Geometry/Rectangle.lean (94%) create mode 100644 shared/Bookshelf/Real/Sequence.lean rename {common/Common => shared/Bookshelf}/Real/Sequence.tex (100%) rename {common/Common => shared/Bookshelf}/Real/Sequence/Arithmetic.lean (100%) rename {common/Common => shared/Bookshelf}/Real/Sequence/Geometric.lean (100%) create mode 100644 shared/Bookshelf/Real/Set.lean rename {common/Common => shared/Bookshelf}/Real/Set/Basic.lean (100%) rename {common/Common => shared/Bookshelf}/Real/Set/Interval.lean (100%) rename {common/Common => shared/Bookshelf}/Real/Set/Partition.lean (93%) rename {common/Common => shared/Bookshelf}/Tuple.lean (100%) rename {common => shared}/lake-manifest.json (100%) rename {common => shared}/lakefile.lean (79%) rename {common => shared}/lean-toolchain (100%) rename {common => shared}/preamble.tex (100%) diff --git a/common/Common/List.lean b/common/Common/List.lean deleted file mode 100644 index 798f875..0000000 --- a/common/Common/List.lean +++ /dev/null @@ -1 +0,0 @@ -import Common.List.Basic \ No newline at end of file diff --git a/common/Common/Real.lean b/common/Common/Real.lean deleted file mode 100644 index 2f95067..0000000 --- a/common/Common/Real.lean +++ /dev/null @@ -1,5 +0,0 @@ -import Common.Real.Basic -import Common.Real.Function -import Common.Real.Geometry -import Common.Real.Sequence -import Common.Real.Set \ No newline at end of file diff --git a/common/Common/Real/Function.lean b/common/Common/Real/Function.lean deleted file mode 100644 index c2a2a7a..0000000 --- a/common/Common/Real/Function.lean +++ /dev/null @@ -1 +0,0 @@ -import Common.Real.Function.Step \ No newline at end of file diff --git a/common/Common/Real/Geometry.lean b/common/Common/Real/Geometry.lean deleted file mode 100644 index 220e9c6..0000000 --- a/common/Common/Real/Geometry.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Common.Real.Geometry.Basic -import Common.Real.Geometry.Rectangle \ No newline at end of file diff --git a/common/Common/Real/Sequence.lean b/common/Common/Real/Sequence.lean deleted file mode 100644 index b08da38..0000000 --- a/common/Common/Real/Sequence.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Common.Real.Sequence.Arithmetic -import Common.Real.Sequence.Geometric \ No newline at end of file diff --git a/common/Common/Real/Set.lean b/common/Common/Real/Set.lean deleted file mode 100644 index e7b2fc3..0000000 --- a/common/Common/Real/Set.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Common.Real.Set.Basic -import Common.Real.Set.Interval -import Common.Real.Set.Partition \ No newline at end of file diff --git a/first-course-abstract-algebra/lake-manifest.json b/first-course-abstract-algebra/lake-manifest.json index 59662d6..b594809 100644 --- a/first-course-abstract-algebra/lake-manifest.json +++ b/first-course-abstract-algebra/lake-manifest.json @@ -1,7 +1,8 @@ {"version": 4, "packagesDir": "lake-packages", "packages": - [{"git": + [{"path": {"name": "Bookshelf", "dir": "./../shared"}}, + {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", @@ -24,5 +25,4 @@ "subDir?": null, "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", "name": "std", - "inputRev?": "main"}}, - {"path": {"name": "Common", "dir": "./../common"}}]} + "inputRev?": "main"}}]} diff --git a/first-course-abstract-algebra/lakefile.lean b/first-course-abstract-algebra/lakefile.lean index 6ace49d..b09cff8 100644 --- a/first-course-abstract-algebra/lakefile.lean +++ b/first-course-abstract-algebra/lakefile.lean @@ -3,7 +3,7 @@ open Lake DSL package «first-course-abstract-algebra» -require Common from "../common" +require Bookshelf from "../shared" require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" diff --git a/mathematical-introduction-logic/Enderton/Chapter0.lean b/mathematical-introduction-logic/Enderton/Chapter0.lean index 1dcce8c..29a1fcf 100644 --- a/mathematical-introduction-logic/Enderton/Chapter0.lean +++ b/mathematical-introduction-logic/Enderton/Chapter0.lean @@ -4,15 +4,15 @@ Chapter 0 Useful Facts About Sets -/ -import Common.Tuple +import Bookshelf.Tuple /-- -The following describes a so-called "generic" tuple. Like in `Common.Tuple`, an -`n`-tuple is defined recursively like so: +The following describes a so-called "generic" tuple. Like in `Bookshelf.Tuple`, +an `n`-tuple is defined recursively like so: `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩` -Unlike `Common.Tuple`, a "generic" tuple bends the syntax above further. For +Unlike `Bookshelf.Tuple`, a "generic" tuple bends the syntax above further. For example, both tuples above are equivalent to: `⟨⟨x₁, ..., xₘ⟩, xₘ₊₁, ..., xₙ⟩` @@ -20,7 +20,7 @@ example, both tuples above are equivalent to: for some `1 ≤ m ≤ n`. This distinction is purely syntactic, but necessary to prove certain theorems found in [1] (e.g. `lemma_0a`). -In general, prefer `Common.Tuple`. +In general, prefer `Bookshelf.Tuple`. -/ inductive XTuple : (α : Type u) → (size : Nat × Nat) → Type u where | nil : XTuple α (0, 0) diff --git a/mathematical-introduction-logic/lake-manifest.json b/mathematical-introduction-logic/lake-manifest.json index 59662d6..b594809 100644 --- a/mathematical-introduction-logic/lake-manifest.json +++ b/mathematical-introduction-logic/lake-manifest.json @@ -1,7 +1,8 @@ {"version": 4, "packagesDir": "lake-packages", "packages": - [{"git": + [{"path": {"name": "Bookshelf", "dir": "./../shared"}}, + {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", @@ -24,5 +25,4 @@ "subDir?": null, "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", "name": "std", - "inputRev?": "main"}}, - {"path": {"name": "Common", "dir": "./../common"}}]} + "inputRev?": "main"}}]} diff --git a/mathematical-introduction-logic/lakefile.lean b/mathematical-introduction-logic/lakefile.lean index 338c3cc..3848b97 100644 --- a/mathematical-introduction-logic/lakefile.lean +++ b/mathematical-introduction-logic/lakefile.lean @@ -3,7 +3,7 @@ open Lake DSL package «mathematical-introduction-logic» -require Common from "../common" +require Bookshelf from "../shared" @[default_target] lean_lib «enderton» diff --git a/one-variable-calculus/Apostol/Chapter_1_6.lean b/one-variable-calculus/Apostol/Chapter_1_6.lean index beee9cf..299dc83 100644 --- a/one-variable-calculus/Apostol/Chapter_1_6.lean +++ b/one-variable-calculus/Apostol/Chapter_1_6.lean @@ -3,8 +3,8 @@ Chapter 1.6 The concept of area as a set function -/ -import Common.Real.Function.Step -import Common.Real.Geometry.Rectangle +import Bookshelf.Real.Function.Step +import Bookshelf.Real.Geometry.Rectangle namespace Real diff --git a/one-variable-calculus/Apostol/Chapter_I_3.lean b/one-variable-calculus/Apostol/Chapter_I_3.lean index bd43f34..536f98e 100644 --- a/one-variable-calculus/Apostol/Chapter_I_3.lean +++ b/one-variable-calculus/Apostol/Chapter_I_3.lean @@ -3,7 +3,7 @@ Chapter I 3 A Set of Axioms for the Real-Number System -/ -import Common.Real.Set +import Bookshelf.Real.Set #check Archimedean #check Real.exists_isLUB diff --git a/one-variable-calculus/lake-manifest.json b/one-variable-calculus/lake-manifest.json index 59662d6..b594809 100644 --- a/one-variable-calculus/lake-manifest.json +++ b/one-variable-calculus/lake-manifest.json @@ -1,7 +1,8 @@ {"version": 4, "packagesDir": "lake-packages", "packages": - [{"git": + [{"path": {"name": "Bookshelf", "dir": "./../shared"}}, + {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", @@ -24,5 +25,4 @@ "subDir?": null, "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", "name": "std", - "inputRev?": "main"}}, - {"path": {"name": "Common", "dir": "./../common"}}]} + "inputRev?": "main"}}]} diff --git a/one-variable-calculus/lakefile.lean b/one-variable-calculus/lakefile.lean index a2e6da4..d87456f 100644 --- a/one-variable-calculus/lakefile.lean +++ b/one-variable-calculus/lakefile.lean @@ -3,7 +3,7 @@ open Lake DSL package «one-variable-calculus» -require Common from "../common" +require Bookshelf from "../shared" require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" diff --git a/common/Common.lean b/shared/Bookshelf.lean similarity index 100% rename from common/Common.lean rename to shared/Bookshelf.lean diff --git a/shared/Bookshelf/List.lean b/shared/Bookshelf/List.lean new file mode 100644 index 0000000..e86566b --- /dev/null +++ b/shared/Bookshelf/List.lean @@ -0,0 +1 @@ +import Bookshelf.List.Basic diff --git a/common/Common/List/Basic.lean b/shared/Bookshelf/List/Basic.lean similarity index 100% rename from common/Common/List/Basic.lean rename to shared/Bookshelf/List/Basic.lean diff --git a/shared/Bookshelf/Real.lean b/shared/Bookshelf/Real.lean new file mode 100644 index 0000000..6313158 --- /dev/null +++ b/shared/Bookshelf/Real.lean @@ -0,0 +1,5 @@ +import Bookshelf.Real.Basic +import Bookshelf.Real.Function +import Bookshelf.Real.Geometry +import Bookshelf.Real.Sequence +import Bookshelf.Real.Set diff --git a/common/Common/Real/Basic.lean b/shared/Bookshelf/Real/Basic.lean similarity index 100% rename from common/Common/Real/Basic.lean rename to shared/Bookshelf/Real/Basic.lean diff --git a/shared/Bookshelf/Real/Function.lean b/shared/Bookshelf/Real/Function.lean new file mode 100644 index 0000000..c2a3e36 --- /dev/null +++ b/shared/Bookshelf/Real/Function.lean @@ -0,0 +1 @@ +import Bookshelf.Real.Function.Step diff --git a/common/Common/Real/Function/Step.lean b/shared/Bookshelf/Real/Function/Step.lean similarity index 91% rename from common/Common/Real/Function/Step.lean rename to shared/Bookshelf/Real/Function/Step.lean index 55c49f2..455351e 100644 --- a/common/Common/Real/Function/Step.lean +++ b/shared/Bookshelf/Real/Function/Step.lean @@ -1,8 +1,8 @@ import Mathlib.Data.Fin.Basic import Mathlib.Tactic.NormNum -import Common.Real.Basic -import Common.Real.Set.Partition +import Bookshelf.Real.Basic +import Bookshelf.Real.Set.Partition namespace Real.Function @@ -35,4 +35,4 @@ def set_def (f : Step) : Set ℝ² := sorry -- TODO: Fill out -end Real.Function.Step \ No newline at end of file +end Real.Function.Step diff --git a/shared/Bookshelf/Real/Geometry.lean b/shared/Bookshelf/Real/Geometry.lean new file mode 100644 index 0000000..2fc3101 --- /dev/null +++ b/shared/Bookshelf/Real/Geometry.lean @@ -0,0 +1,2 @@ +import Bookshelf.Real.Geometry.Basic +import Bookshelf.Real.Geometry.Rectangle diff --git a/common/Common/Real/Geometry/Basic.lean b/shared/Bookshelf/Real/Geometry/Basic.lean similarity index 97% rename from common/Common/Real/Geometry/Basic.lean rename to shared/Bookshelf/Real/Geometry/Basic.lean index c26299e..53dcc99 100644 --- a/common/Common/Real/Geometry/Basic.lean +++ b/shared/Bookshelf/Real/Geometry/Basic.lean @@ -1,6 +1,6 @@ import Mathlib.Data.Real.Sqrt -import Common.Real.Basic +import Bookshelf.Real.Basic namespace Real @@ -47,4 +47,4 @@ theorem congruent_similar {S T : Set ℝ²} : congruent S T → similar S T := b conv at hs => intro x y hxy; arg 1; rw [← one_mul (dist x y)] exact ⟨f, ⟨hf, ⟨1, hs⟩⟩⟩ -end Real \ No newline at end of file +end Real diff --git a/common/Common/Real/Geometry/Rectangle.lean b/shared/Bookshelf/Real/Geometry/Rectangle.lean similarity index 94% rename from common/Common/Real/Geometry/Rectangle.lean rename to shared/Bookshelf/Real/Geometry/Rectangle.lean index b10efb0..8350fa8 100644 --- a/common/Common/Real/Geometry/Rectangle.lean +++ b/shared/Bookshelf/Real/Geometry/Rectangle.lean @@ -1,4 +1,4 @@ -import Common.Real.Geometry.Basic +import Bookshelf.Real.Geometry.Basic namespace Real @@ -41,4 +41,4 @@ Computes the height of a `Rectangle`. noncomputable def height (r : Rectangle) : ℝ := dist r.bottom_left r.bottom_right -end Real.Rectangle \ No newline at end of file +end Real.Rectangle diff --git a/shared/Bookshelf/Real/Sequence.lean b/shared/Bookshelf/Real/Sequence.lean new file mode 100644 index 0000000..0bfafc5 --- /dev/null +++ b/shared/Bookshelf/Real/Sequence.lean @@ -0,0 +1,2 @@ +import Bookshelf.Real.Sequence.Arithmetic +import Bookshelf.Real.Sequence.Geometric diff --git a/common/Common/Real/Sequence.tex b/shared/Bookshelf/Real/Sequence.tex similarity index 100% rename from common/Common/Real/Sequence.tex rename to shared/Bookshelf/Real/Sequence.tex diff --git a/common/Common/Real/Sequence/Arithmetic.lean b/shared/Bookshelf/Real/Sequence/Arithmetic.lean similarity index 100% rename from common/Common/Real/Sequence/Arithmetic.lean rename to shared/Bookshelf/Real/Sequence/Arithmetic.lean diff --git a/common/Common/Real/Sequence/Geometric.lean b/shared/Bookshelf/Real/Sequence/Geometric.lean similarity index 100% rename from common/Common/Real/Sequence/Geometric.lean rename to shared/Bookshelf/Real/Sequence/Geometric.lean diff --git a/shared/Bookshelf/Real/Set.lean b/shared/Bookshelf/Real/Set.lean new file mode 100644 index 0000000..9f936f3 --- /dev/null +++ b/shared/Bookshelf/Real/Set.lean @@ -0,0 +1,3 @@ +import Bookshelf.Real.Set.Basic +import Bookshelf.Real.Set.Interval +import Bookshelf.Real.Set.Partition diff --git a/common/Common/Real/Set/Basic.lean b/shared/Bookshelf/Real/Set/Basic.lean similarity index 100% rename from common/Common/Real/Set/Basic.lean rename to shared/Bookshelf/Real/Set/Basic.lean diff --git a/common/Common/Real/Set/Interval.lean b/shared/Bookshelf/Real/Set/Interval.lean similarity index 100% rename from common/Common/Real/Set/Interval.lean rename to shared/Bookshelf/Real/Set/Interval.lean diff --git a/common/Common/Real/Set/Partition.lean b/shared/Bookshelf/Real/Set/Partition.lean similarity index 93% rename from common/Common/Real/Set/Partition.lean rename to shared/Bookshelf/Real/Set/Partition.lean index 44cddbe..a30f029 100644 --- a/common/Common/Real/Set/Partition.lean +++ b/shared/Bookshelf/Real/Set/Partition.lean @@ -1,5 +1,5 @@ -import Common.List.Basic -import Common.Real.Set.Interval +import Bookshelf.List.Basic +import Bookshelf.Real.Set.Interval namespace Real @@ -42,4 +42,4 @@ instance : Membership ℝ Partition where end Partition -end Real \ No newline at end of file +end Real diff --git a/common/Common/Tuple.lean b/shared/Bookshelf/Tuple.lean similarity index 100% rename from common/Common/Tuple.lean rename to shared/Bookshelf/Tuple.lean diff --git a/common/lake-manifest.json b/shared/lake-manifest.json similarity index 100% rename from common/lake-manifest.json rename to shared/lake-manifest.json diff --git a/common/lakefile.lean b/shared/lakefile.lean similarity index 79% rename from common/lakefile.lean rename to shared/lakefile.lean index 41fc850..da702ea 100644 --- a/common/lakefile.lean +++ b/shared/lakefile.lean @@ -1,11 +1,11 @@ import Lake open Lake DSL -package «Common» +package «Bookshelf» require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" @[default_target] -lean_lib «Common» +lean_lib «Bookshelf» diff --git a/common/lean-toolchain b/shared/lean-toolchain similarity index 100% rename from common/lean-toolchain rename to shared/lean-toolchain diff --git a/common/preamble.tex b/shared/preamble.tex similarity index 100% rename from common/preamble.tex rename to shared/preamble.tex