From 62077460b5e306e0bf79ce1ea7497ea1676a9ac5 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 1 Apr 2023 20:59:12 -0600 Subject: [PATCH] Setup scaffolding for Fraleigh's "A First Course in Abstract Algebra". --- README.md | 13 ++++ bookshelf/Bookshelf/Sequence/Arithmetic.lean | 20 ++--- bookshelf/Bookshelf/Sequence/Geometric.lean | 10 +-- bookshelf/Bookshelf/Tuple.lean | 1 - bookshelf/lake-manifest.json | 10 +-- bookshelf/lakefile.lean | 7 +- bookshelf/lean-toolchain | 2 +- .../FirstCourseAbstractAlgebra.lean | 6 ++ .../Exercises1.lean | 18 +++++ .../lake-manifest.json | 28 +++++++ first-course-abstract-algebra/lakefile.lean | 14 ++++ first-course-abstract-algebra/lean-toolchain | 1 + .../lake-manifest.json | 2 +- .../lean-toolchain | 2 +- .../TheoremProvingInLean/Exercises7.lean | 73 ++++++++++--------- theorem-proving-in-lean/lean-toolchain | 2 +- 16 files changed, 145 insertions(+), 64 deletions(-) create mode 100644 first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean create mode 100644 first-course-abstract-algebra/FirstCourseAbstractAlgebra/Exercises1.lean create mode 100644 first-course-abstract-algebra/lake-manifest.json create mode 100644 first-course-abstract-algebra/lakefile.lean create mode 100644 first-course-abstract-algebra/lean-toolchain diff --git a/README.md b/README.md index af9b1e6..5f17d7b 100644 --- a/README.md +++ b/README.md @@ -1 +1,14 @@ # bookshelf-lean + +A collection of proofs and answers to exercises to books I'm studying. + +## Updates + +Lean's tooling is a fickle beast. If looking to update e.g. `Mathlib`, pin a new +version to the `lake-manifest.json` file and start a new build from scratch: + +```bash +> lake update +> lake clean +> lake build +``` diff --git a/bookshelf/Bookshelf/Sequence/Arithmetic.lean b/bookshelf/Bookshelf/Sequence/Arithmetic.lean index ebb9d85..c732265 100644 --- a/bookshelf/Bookshelf/Sequence/Arithmetic.lean +++ b/bookshelf/Bookshelf/Sequence/Arithmetic.lean @@ -40,11 +40,11 @@ theorem term_recursive_closed (seq : Arithmetic) (n : Nat) (by unfold termRecursive termClosed; norm_num) (fun n ih => calc termRecursive seq (Nat.succ n) - = seq.Δ + seq.termRecursive n := rfl - _ = seq.Δ + seq.termClosed n := by rw [ih] - _ = seq.Δ + (seq.a₀ + seq.Δ * n) := rfl - _ = seq.a₀ + seq.Δ * (n + 1) := by ring - _ = termClosed seq (n + 1) := rfl) + = seq.Δ + seq.termRecursive n := rfl + _ = seq.Δ + seq.termClosed n := by rw [ih] + _ = seq.Δ + (seq.a₀ + seq.Δ * n) := rfl + _ = seq.a₀ + seq.Δ * (n + 1) := by ring + _ = termClosed seq (n + 1) := rfl) /--[1] Summation of the first `n` terms of an arithmetic sequence. @@ -64,10 +64,10 @@ theorem sum_closed_formula (seq : Arithmetic) (n : Nat) (by unfold sum termClosed; norm_num) (fun n ih => calc sum seq n.succ - = seq.termClosed n + seq.sum n := rfl - _ = seq.termClosed n + (n / 2 * (seq.a₀ + seq.termClosed (n - 1))) := by rw [ih] - _ = seq.a₀ + seq.Δ * n + (n / 2 * (seq.a₀ + (seq.a₀ + seq.Δ * ↑(n - 1)))) := rfl - -- TODO: To continue, need to find how to deal with division. - _ = ↑(n + 1) / 2 * (seq.a₀ + seq.termClosed n) := by sorry) + = seq.termClosed n + seq.sum n := rfl + _ = seq.termClosed n + (n / 2 * (seq.a₀ + seq.termClosed (n - 1))) := by rw [ih] + _ = seq.a₀ + seq.Δ * n + (n / 2 * (seq.a₀ + (seq.a₀ + seq.Δ * ↑(n - 1)))) := rfl + -- TODO: To continue, need to find how to deal with division. + _ = ↑(n + 1) / 2 * (seq.a₀ + seq.termClosed n) := by sorry) end Arithmetic \ No newline at end of file diff --git a/bookshelf/Bookshelf/Sequence/Geometric.lean b/bookshelf/Bookshelf/Sequence/Geometric.lean index 11c94ce..fa3f033 100644 --- a/bookshelf/Bookshelf/Sequence/Geometric.lean +++ b/bookshelf/Bookshelf/Sequence/Geometric.lean @@ -40,11 +40,11 @@ theorem term_recursive_closed (seq : Geometric) (n : Nat) (by unfold termClosed termRecursive; norm_num) (fun n ih => calc seq.termRecursive (n + 1) - = seq.r * (seq.termRecursive n) := rfl - _ = seq.r * (seq.termClosed n) := by rw [ih] - _ = seq.r * (seq.a₀ * seq.r ^ n) := rfl - _ = seq.a₀ * seq.r ^ (n + 1) := by ring - _ = seq.termClosed (n + 1) := rfl) + = seq.r * (seq.termRecursive n) := rfl + _ = seq.r * (seq.termClosed n) := by rw [ih] + _ = seq.r * (seq.a₀ * seq.r ^ n) := rfl + _ = seq.a₀ * seq.r ^ (n + 1) := by ring + _ = seq.termClosed (n + 1) := rfl) /--[1] Summation of the first `n` terms of a geometric sequence. diff --git a/bookshelf/Bookshelf/Tuple.lean b/bookshelf/Bookshelf/Tuple.lean index 5584cac..6f45ee5 100644 --- a/bookshelf/Bookshelf/Tuple.lean +++ b/bookshelf/Bookshelf/Tuple.lean @@ -5,7 +5,6 @@ Harcourt/Academic Press, 2001. -/ -import Mathlib.Tactic.NormCast import Mathlib.Tactic.Ring /-- diff --git a/bookshelf/lake-manifest.json b/bookshelf/lake-manifest.json index d02be76..0c15284 100644 --- a/bookshelf/lake-manifest.json +++ b/bookshelf/lake-manifest.json @@ -4,24 +4,24 @@ [{"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "7e974fd3806866272e9f6d9e44fa04c210a21f87", + "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", "name": "mathlib", - "inputRev?": null}}, + "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/bookshelf/lakefile.lean b/bookshelf/lakefile.lean index fd40766..d21af3d 100644 --- a/bookshelf/lakefile.lean +++ b/bookshelf/lakefile.lean @@ -1,11 +1,12 @@ import Lake open Lake DSL -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" - package «Bookshelf» +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ + "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" + @[default_target] lean_lib «Bookshelf» { -- add library configuration options here diff --git a/bookshelf/lean-toolchain b/bookshelf/lean-toolchain index 5bf01da..d30699b 100644 --- a/bookshelf/lean-toolchain +++ b/bookshelf/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-02-10 +leanprover/lean4:nightly-2023-04-02 diff --git a/first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean b/first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean new file mode 100644 index 0000000..6c2bc9a --- /dev/null +++ b/first-course-abstract-algebra/FirstCourseAbstractAlgebra.lean @@ -0,0 +1,6 @@ +/- +# 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/FirstCourseAbstractAlgebra/Exercises1.lean b/first-course-abstract-algebra/FirstCourseAbstractAlgebra/Exercises1.lean new file mode 100644 index 0000000..11f39fc --- /dev/null +++ b/first-course-abstract-algebra/FirstCourseAbstractAlgebra/Exercises1.lean @@ -0,0 +1,18 @@ +/- +# References + +1. Fraleigh, John B. A First Course in Abstract Algebra, n.d. +-/ + +import Mathlib.Data.Complex.Basic + +open Complex +open HPow + +-- In Exercises 1 through 9 compute the given arithmetic expression and give the +-- answer in the form $a + bi$ for $a, b ∈ ℝ$. + +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 diff --git a/first-course-abstract-algebra/lake-manifest.json b/first-course-abstract-algebra/lake-manifest.json new file mode 100644 index 0000000..123a66f --- /dev/null +++ b/first-course-abstract-algebra/lake-manifest.json @@ -0,0 +1,28 @@ +{"version": 4, + "packagesDir": "lake-packages", + "packages": + [{"path": {"name": "Bookshelf", "dir": "./../bookshelf"}}, + {"git": + {"url": "https://github.com/leanprover-community/mathlib4.git", + "subDir?": null, + "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", + "name": "mathlib", + "inputRev?": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"}}, + {"git": + {"url": "https://github.com/gebner/quote4", + "subDir?": null, + "rev": "7ae096b232087096ff0243a2b70d32720d2621ae", + "name": "Qq", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/JLimperg/aesop", + "subDir?": null, + "rev": "071464ac36e339afb7a87640aa1f8121f707a59a", + "name": "aesop", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", + "name": "std", + "inputRev?": "main"}}]} diff --git a/first-course-abstract-algebra/lakefile.lean b/first-course-abstract-algebra/lakefile.lean new file mode 100644 index 0000000..2c7a6f3 --- /dev/null +++ b/first-course-abstract-algebra/lakefile.lean @@ -0,0 +1,14 @@ +import Lake +open Lake DSL + +package «first-course-abstract-algebra» + +require Bookshelf from "../bookshelf" +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ + "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" + +@[default_target] +lean_lib «FirstCourseAbstractAlgebra» { + -- add library configuration options here +} diff --git a/first-course-abstract-algebra/lean-toolchain b/first-course-abstract-algebra/lean-toolchain new file mode 100644 index 0000000..d30699b --- /dev/null +++ b/first-course-abstract-algebra/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2023-04-02 diff --git a/mathematical-introduction-logic/lake-manifest.json b/mathematical-introduction-logic/lake-manifest.json index 2810171..a6ef150 100644 --- a/mathematical-introduction-logic/lake-manifest.json +++ b/mathematical-introduction-logic/lake-manifest.json @@ -7,7 +7,7 @@ "subDir?": null, "rev": "7e974fd3806866272e9f6d9e44fa04c210a21f87", "name": "mathlib", - "inputRev?": null}}, + "inputRev?": "7e974fd3806866272e9f6d9e44fa04c210a21f87"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/mathematical-introduction-logic/lean-toolchain b/mathematical-introduction-logic/lean-toolchain index 19d47bf..d30699b 100644 --- a/mathematical-introduction-logic/lean-toolchain +++ b/mathematical-introduction-logic/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-02-12 +leanprover/lean4:nightly-2023-04-02 diff --git a/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean b/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean index 84c6fb0..b5dde0f 100644 --- a/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean +++ b/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean @@ -45,8 +45,9 @@ Nat.recOn (motive := fun x => Nat.zero + x = x) (fun (n : Nat) (ih : Nat.zero + n = n) => show Nat.zero + n.succ = n.succ from calc - Nat.zero + n.succ = (Nat.zero + n).succ := add_succ Nat.zero n - _ = n.succ := by rw [ih]) + Nat.zero + n.succ + = (Nat.zero + n).succ := add_succ Nat.zero n + _ = n.succ := by rw [ih]) -- Additional definitions. def mul (m n : Nat) : Nat := @@ -105,12 +106,12 @@ theorem length_inject_anywhere (x : α) (as bs : List α) | nil => simp | cons head tail ih => calc List.length (head :: tail ++ [x] ++ bs) - = List.length (tail ++ [x] ++ bs) + 1 := rfl - _ = List.length tail + List.length bs + 1 + 1 := by rw [ih] - _ = List.length tail + (List.length bs + 1) + 1 := by rw [Nat.add_assoc (List.length tail)] - _ = List.length tail + (1 + List.length bs) + 1 := by rw [Nat.add_comm (List.length bs)] - _ = List.length tail + 1 + List.length bs + 1 := by rw [Nat.add_assoc (List.length tail) 1] - _ = List.length (head :: tail) + List.length bs + 1 := rfl + = List.length (tail ++ [x] ++ bs) + 1 := rfl + _ = List.length tail + List.length bs + 1 + 1 := by rw [ih] + _ = List.length tail + (List.length bs + 1) + 1 := by rw [Nat.add_assoc (List.length tail)] + _ = List.length tail + (1 + List.length bs) + 1 := by rw [Nat.add_comm (List.length bs)] + _ = List.length tail + 1 + List.length bs + 1 := by rw [Nat.add_assoc (List.length tail) 1] + _ = List.length (head :: tail) + List.length bs + 1 := rfl theorem list_reverse_aux_append (as bs : List α) : List.reverseAux as bs = List.reverse as ++ bs := by @@ -118,12 +119,12 @@ theorem list_reverse_aux_append (as bs : List α) | nil => rw [List.reverseAux, List.reverse, List.reverseAux, List.nil_append] | cons head tail ih => calc List.reverseAux (head :: tail) bs - = List.reverseAux tail (head :: bs) := rfl - _ = List.reverse tail ++ (head :: bs) := by rw [ih] - _ = List.reverse tail ++ ([head] ++ bs) := rfl - _ = List.reverse tail ++ [head] ++ bs := by rw [List.append_assoc] - _ = List.reverseAux tail [head] ++ bs := by rw [ih] - _ = List.reverseAux (head :: tail) [] ++ bs := rfl + = List.reverseAux tail (head :: bs) := rfl + _ = List.reverse tail ++ (head :: bs) := by rw [ih] + _ = List.reverse tail ++ ([head] ++ bs) := rfl + _ = List.reverse tail ++ [head] ++ bs := by rw [List.append_assoc] + _ = List.reverseAux tail [head] ++ bs := by rw [ih] + _ = List.reverseAux (head :: tail) [] ++ bs := rfl theorem length_reverse (t : List α) : List.length (List.reverse t) = List.length t := by @@ -131,14 +132,14 @@ theorem length_reverse (t : List α) | nil => simp | cons head tail ih => calc List.length (List.reverse (head :: tail)) - = List.length (List.reverseAux tail [head]) := rfl - _ = List.length (List.reverse tail ++ [head]) := by rw [list_reverse_aux_append] - _ = List.length (List.reverse tail) + List.length [head] := by simp - _ = List.length tail + List.length [head] := by rw [ih] - _ = List.length tail + 1 := rfl - _ = List.length [] + List.length tail + 1 := by simp - _ = List.length ([] ++ [head] ++ tail) := by rw [length_inject_anywhere] - _ = List.length (head :: tail) := rfl + = List.length (List.reverseAux tail [head]) := rfl + _ = List.length (List.reverse tail ++ [head]) := by rw [list_reverse_aux_append] + _ = List.length (List.reverse tail) + List.length [head] := by simp + _ = List.length tail + List.length [head] := by rw [ih] + _ = List.length tail + 1 := rfl + _ = List.length [] + List.length tail + 1 := by simp + _ = List.length ([] ++ [head] ++ tail) := by rw [length_inject_anywhere] + _ = List.length (head :: tail) := rfl theorem reverse_reverse_aux (as bs : List α) : List.reverse (as ++ bs) = List.reverse bs ++ List.reverse as := by @@ -146,14 +147,14 @@ theorem reverse_reverse_aux (as bs : List α) | nil => simp | cons head tail ih => calc List.reverse (head :: tail ++ bs) - = List.reverseAux (head :: tail ++ bs) [] := rfl - _ = List.reverseAux (tail ++ bs) [head] := rfl - _ = List.reverse (tail ++ bs) ++ [head] := by rw [list_reverse_aux_append] - _ = List.reverse bs ++ List.reverse tail ++ [head] := by rw [ih] - _ = List.reverse bs ++ (List.reverse tail ++ [head]) := by rw [List.append_assoc] - _ = List.reverse bs ++ (List.reverseAux tail [head]) := by rw [list_reverse_aux_append] - _ = List.reverse bs ++ (List.reverseAux (head :: tail) []) := rfl - _ = List.reverse bs ++ List.reverse (head :: tail) := rfl + = List.reverseAux (head :: tail ++ bs) [] := rfl + _ = List.reverseAux (tail ++ bs) [head] := rfl + _ = List.reverse (tail ++ bs) ++ [head] := by rw [list_reverse_aux_append] + _ = List.reverse bs ++ List.reverse tail ++ [head] := by rw [ih] + _ = List.reverse bs ++ (List.reverse tail ++ [head]) := by rw [List.append_assoc] + _ = List.reverse bs ++ (List.reverseAux tail [head]) := by rw [list_reverse_aux_append] + _ = List.reverse bs ++ (List.reverseAux (head :: tail) []) := rfl + _ = List.reverse bs ++ List.reverse (head :: tail) := rfl theorem reverse_reverse (t : List α) : List.reverse (List.reverse t) = t := by @@ -161,12 +162,12 @@ theorem reverse_reverse (t : List α) | nil => simp | cons head tail ih => calc List.reverse (List.reverse (head :: tail)) - = List.reverse (List.reverseAux tail [head]) := rfl - _ = List.reverse (List.reverse tail ++ [head]) := by rw [list_reverse_aux_append] - _ = List.reverse [head] ++ List.reverse (List.reverse tail) := by rw [reverse_reverse_aux] - _ = List.reverse [head] ++ tail := by rw [ih] - _ = [head] ++ tail := by simp - _ = head :: tail := rfl + = List.reverse (List.reverseAux tail [head]) := rfl + _ = List.reverse (List.reverse tail ++ [head]) := by rw [list_reverse_aux_append] + _ = List.reverse [head] ++ List.reverse (List.reverse tail) := by rw [reverse_reverse_aux] + _ = List.reverse [head] ++ tail := by rw [ih] + _ = [head] ++ tail := by simp + _ = head :: tail := rfl end ex2 diff --git a/theorem-proving-in-lean/lean-toolchain b/theorem-proving-in-lean/lean-toolchain index 5bf01da..d30699b 100644 --- a/theorem-proving-in-lean/lean-toolchain +++ b/theorem-proving-in-lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-02-10 +leanprover/lean4:nightly-2023-04-02