Setup scaffolding for Fraleigh's "A First Course in Abstract Algebra".

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
+```

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

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.

bookshelf/Bookshelf/Tuple.lean

@@ -5,7 +5,6 @@
    Harcourt/Academic Press, 2001.
 -/
 
-import Mathlib.Tactic.NormCast
 import Mathlib.Tactic.Ring
 
 /--

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"}}]}

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

bookshelf/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-10
+leanprover/lean4:nightly-2023-04-02

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

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

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"}}]}

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
+}

first-course-abstract-algebra/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-04-02

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,

mathematical-introduction-logic/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-12
+leanprover/lean4:nightly-2023-04-02

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
 

theorem-proving-in-lean/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-10
+leanprover/lean4:nightly-2023-04-02