From 87e293ea8d48f19e6b7ad2c48316d9fcf930acb1 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sun, 2 Apr 2023 08:57:58 -0600 Subject: [PATCH] Structure projects in the same way. --- .../FirstCourseAbstractAlgebra.lean | 6 ------ first-course-abstract-algebra/Fraleigh.lean | 1 + .../Exercises1.lean => Fraleigh/Chapter1.lean} | 6 +++--- first-course-abstract-algebra/README.md | 3 +++ first-course-abstract-algebra/lakefile.lean | 4 +--- mathematical-introduction-logic/Enderton.lean | 1 + .../Chapter0.lean | 5 ++--- .../MathematicalIntroductionLogic.lean | 7 ------- mathematical-introduction-logic/README.md | 4 ++++ mathematical-introduction-logic/lake-manifest.json | 10 +++++----- mathematical-introduction-logic/lakefile.lean | 2 +- theorem-proving-in-lean/Avigad.lean | 6 ++++++ .../Exercises2.lean => Avigad/Chapter2.lean} | 4 ++-- .../Exercises3.lean => Avigad/Chapter3.lean} | 4 ++-- .../Exercises4.lean => Avigad/Chapter4.lean} | 4 ++-- .../Exercises5.lean => Avigad/Chapter5.lean} | 4 ++-- .../Exercises7.lean => Avigad/Chapter7.lean} | 4 ++-- .../Exercises8.lean => Avigad/Chapter8.lean} | 4 ++-- theorem-proving-in-lean/README.md | 3 +++ theorem-proving-in-lean/TheoremProvingInLean.lean | 6 ------ theorem-proving-in-lean/lakefile.lean | 2 +- 21 files changed, 43 insertions(+), 47 deletions(-) delete mode 100644 first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean create mode 100644 first-course-abstract-algebra/Fraleigh.lean rename first-course-abstract-algebra/{FirstCourseAbstractAlgebra/Exercises1.lean => Fraleigh/Chapter1.lean} (72%) create mode 100644 first-course-abstract-algebra/README.md create mode 100644 mathematical-introduction-logic/Enderton.lean rename mathematical-introduction-logic/{MathematicalIntroductionLogic => Enderton}/Chapter0.lean (98%) delete mode 100644 mathematical-introduction-logic/MathematicalIntroductionLogic.lean create mode 100644 mathematical-introduction-logic/README.md create mode 100644 theorem-proving-in-lean/Avigad.lean rename theorem-proving-in-lean/{TheoremProvingInLean/Exercises2.lean => Avigad/Chapter2.lean} (97%) rename theorem-proving-in-lean/{TheoremProvingInLean/Exercises3.lean => Avigad/Chapter3.lean} (98%) rename theorem-proving-in-lean/{TheoremProvingInLean/Exercises4.lean => Avigad/Chapter4.lean} (99%) rename theorem-proving-in-lean/{TheoremProvingInLean/Exercises5.lean => Avigad/Chapter5.lean} (99%) rename theorem-proving-in-lean/{TheoremProvingInLean/Exercises7.lean => Avigad/Chapter7.lean} (99%) rename theorem-proving-in-lean/{TheoremProvingInLean/Exercises8.lean => Avigad/Chapter8.lean} (98%) create mode 100644 theorem-proving-in-lean/README.md delete mode 100644 theorem-proving-in-lean/TheoremProvingInLean.lean diff --git a/first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean b/first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean deleted file mode 100644 index 6c2bc9a..0000000 --- a/first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean +++ /dev/null @@ -1,6 +0,0 @@ -/- -# References - -1. Fraleigh, John B. A First Course in Abstract Algebra, n.d. --/ -import FirstCourseAbstractAlgebra.Exercises1 \ No newline at end of file diff --git a/first-course-abstract-algebra/Fraleigh.lean b/first-course-abstract-algebra/Fraleigh.lean new file mode 100644 index 0000000..d3e8abf --- /dev/null +++ b/first-course-abstract-algebra/Fraleigh.lean @@ -0,0 +1 @@ +import Fraleigh.Chapter1 diff --git a/first-course-abstract-algebra/FirstCourseAbstractAlgebra/Exercises1.lean b/first-course-abstract-algebra/Fraleigh/Chapter1.lean similarity index 72% rename from first-course-abstract-algebra/FirstCourseAbstractAlgebra/Exercises1.lean rename to first-course-abstract-algebra/Fraleigh/Chapter1.lean index 11f39fc..f0f0df8 100644 --- a/first-course-abstract-algebra/FirstCourseAbstractAlgebra/Exercises1.lean +++ b/first-course-abstract-algebra/Fraleigh/Chapter1.lean @@ -1,7 +1,7 @@ /- -# References +Chapter 1 -1. Fraleigh, John B. A First Course in Abstract Algebra, n.d. +Introduction and Examples -/ import Mathlib.Data.Complex.Basic @@ -15,4 +15,4 @@ open HPow theorem ex1_1 : I^3 = 0 + (-1) * I := calc I^3 = I * (I * hPow I 1) := rfl - _ = 0 + (-1) * I := by simp \ No newline at end of file + _ = 0 + (-1) * I := by simp diff --git a/first-course-abstract-algebra/README.md b/first-course-abstract-algebra/README.md new file mode 100644 index 0000000..21cacc2 --- /dev/null +++ b/first-course-abstract-algebra/README.md @@ -0,0 +1,3 @@ +# A First Course in Abstract Algebra + +Fraleigh, John B. A First Course in Abstract Algebra, n.d. diff --git a/first-course-abstract-algebra/lakefile.lean b/first-course-abstract-algebra/lakefile.lean index 2c7a6f3..847a260 100644 --- a/first-course-abstract-algebra/lakefile.lean +++ b/first-course-abstract-algebra/lakefile.lean @@ -9,6 +9,4 @@ require mathlib from git "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" @[default_target] -lean_lib «FirstCourseAbstractAlgebra» { - -- add library configuration options here -} +lean_lib «fraleigh» diff --git a/mathematical-introduction-logic/Enderton.lean b/mathematical-introduction-logic/Enderton.lean new file mode 100644 index 0000000..c336653 --- /dev/null +++ b/mathematical-introduction-logic/Enderton.lean @@ -0,0 +1 @@ +import Enderton.Chapter0 diff --git a/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean b/mathematical-introduction-logic/Enderton/Chapter0.lean similarity index 98% rename from mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean rename to mathematical-introduction-logic/Enderton/Chapter0.lean index 57e0c98..f0e95e2 100644 --- a/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean +++ b/mathematical-introduction-logic/Enderton/Chapter0.lean @@ -1,8 +1,7 @@ /- -# References +Chapter 0 -1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: - Harcourt/Academic Press, 2001. +Useful Facts About Sets -/ import Bookshelf.Tuple diff --git a/mathematical-introduction-logic/MathematicalIntroductionLogic.lean b/mathematical-introduction-logic/MathematicalIntroductionLogic.lean deleted file mode 100644 index d34aba4..0000000 --- a/mathematical-introduction-logic/MathematicalIntroductionLogic.lean +++ /dev/null @@ -1,7 +0,0 @@ -/- -# References - -1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: - Harcourt/Academic Press, 2001. --/ -import MathematicalIntroductionLogic.Chapter0 diff --git a/mathematical-introduction-logic/README.md b/mathematical-introduction-logic/README.md new file mode 100644 index 0000000..abcd6ee --- /dev/null +++ b/mathematical-introduction-logic/README.md @@ -0,0 +1,4 @@ +# A Mathematical Introduction to Logic + +Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: +Harcourt/Academic Press, 2001. diff --git a/mathematical-introduction-logic/lake-manifest.json b/mathematical-introduction-logic/lake-manifest.json index a6ef150..123a66f 100644 --- a/mathematical-introduction-logic/lake-manifest.json +++ b/mathematical-introduction-logic/lake-manifest.json @@ -5,24 +5,24 @@ {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "7e974fd3806866272e9f6d9e44fa04c210a21f87", + "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", "name": "mathlib", - "inputRev?": "7e974fd3806866272e9f6d9e44fa04c210a21f87"}}, + "inputRev?": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, - "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf", + "rev": "7ae096b232087096ff0243a2b70d32720d2621ae", "name": "Qq", "inputRev?": "master"}}, {"git": {"url": "https://github.com/JLimperg/aesop", "subDir?": null, - "rev": "ba61f7fec6174d8c7d2796457da5a8d0b0da44c6", + "rev": "071464ac36e339afb7a87640aa1f8121f707a59a", "name": "aesop", "inputRev?": "master"}}, {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "de7e2a79905a3f87cad1ad5bf57045206f9738c7", + "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", "name": "std", "inputRev?": "main"}}]} diff --git a/mathematical-introduction-logic/lakefile.lean b/mathematical-introduction-logic/lakefile.lean index 9ea98f4..6ead34c 100644 --- a/mathematical-introduction-logic/lakefile.lean +++ b/mathematical-introduction-logic/lakefile.lean @@ -6,6 +6,6 @@ package «mathematical-introduction-logic» require Bookshelf from "../bookshelf" @[default_target] -lean_lib «MathematicalIntroductionLogic» { +lean_lib «enderton» { -- add library configuration options here } diff --git a/theorem-proving-in-lean/Avigad.lean b/theorem-proving-in-lean/Avigad.lean new file mode 100644 index 0000000..478fb85 --- /dev/null +++ b/theorem-proving-in-lean/Avigad.lean @@ -0,0 +1,6 @@ +import Avigad.Chapter2 +import Avigad.Chapter3 +import Avigad.Chapter4 +import Avigad.Chapter5 +import Avigad.Chapter7 +import Avigad.Chapter8 diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean b/theorem-proving-in-lean/Avigad/Chapter2.lean similarity index 97% rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean rename to theorem-proving-in-lean/Avigad/Chapter2.lean index 13edbaa..37066f8 100644 --- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean +++ b/theorem-proving-in-lean/Avigad/Chapter2.lean @@ -1,7 +1,7 @@ /- -# References +Chapter 2 -1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Dependent Type Theory -/ -- Exercise 1 diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean b/theorem-proving-in-lean/Avigad/Chapter3.lean similarity index 98% rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean rename to theorem-proving-in-lean/Avigad/Chapter3.lean index 0f69765..47b465d 100644 --- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean +++ b/theorem-proving-in-lean/Avigad/Chapter3.lean @@ -1,7 +1,7 @@ /- -# References +Chapter 3 -1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Propositions and Proofs -/ -- Exercise 1 diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean b/theorem-proving-in-lean/Avigad/Chapter4.lean similarity index 99% rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean rename to theorem-proving-in-lean/Avigad/Chapter4.lean index d016adc..6768087 100644 --- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean +++ b/theorem-proving-in-lean/Avigad/Chapter4.lean @@ -1,7 +1,7 @@ /- -# References +Chapter 4 -1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Quantifiers and Equality -/ -- Exercise 1 diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean b/theorem-proving-in-lean/Avigad/Chapter5.lean similarity index 99% rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean rename to theorem-proving-in-lean/Avigad/Chapter5.lean index e269ec1..1698e11 100644 --- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean +++ b/theorem-proving-in-lean/Avigad/Chapter5.lean @@ -1,7 +1,7 @@ /- -# References +Chapter 5 -1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Tactics -/ -- Exercise 1 diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean b/theorem-proving-in-lean/Avigad/Chapter7.lean similarity index 99% rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean rename to theorem-proving-in-lean/Avigad/Chapter7.lean index b5dde0f..032e5f9 100644 --- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean +++ b/theorem-proving-in-lean/Avigad/Chapter7.lean @@ -1,7 +1,7 @@ /- -# References +Chapter 7 -1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Inductive Types -/ -- Exercise 1 diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean b/theorem-proving-in-lean/Avigad/Chapter8.lean similarity index 98% rename from theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean rename to theorem-proving-in-lean/Avigad/Chapter8.lean index 934b394..0ae3c31 100644 --- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean +++ b/theorem-proving-in-lean/Avigad/Chapter8.lean @@ -1,7 +1,7 @@ /- -# References +Chapter 8 -1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Induction and Recursion -/ -- Exercise 1 diff --git a/theorem-proving-in-lean/README.md b/theorem-proving-in-lean/README.md new file mode 100644 index 0000000..e370109 --- /dev/null +++ b/theorem-proving-in-lean/README.md @@ -0,0 +1,3 @@ +# Theorem Proving in Lean + +Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. diff --git a/theorem-proving-in-lean/TheoremProvingInLean.lean b/theorem-proving-in-lean/TheoremProvingInLean.lean deleted file mode 100644 index 277ec5e..0000000 --- a/theorem-proving-in-lean/TheoremProvingInLean.lean +++ /dev/null @@ -1,6 +0,0 @@ -import TheoremProvingInLean.Exercises2 -import TheoremProvingInLean.Exercises3 -import TheoremProvingInLean.Exercises4 -import TheoremProvingInLean.Exercises5 -import TheoremProvingInLean.Exercises7 -import TheoremProvingInLean.Exercises8 \ No newline at end of file diff --git a/theorem-proving-in-lean/lakefile.lean b/theorem-proving-in-lean/lakefile.lean index d989b0a..a5dd762 100644 --- a/theorem-proving-in-lean/lakefile.lean +++ b/theorem-proving-in-lean/lakefile.lean @@ -4,4 +4,4 @@ open Lake DSL package «theorem-proving-in-lean» @[default_target] -lean_lib «TheoremProvingInLean» +lean_lib «avigad»