From 827229a92787f34e01a11815b43016779ecf3906 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 14 Feb 2023 09:54:31 -0700 Subject: [PATCH] Add initial arithmetic/geometric sequence/series definitions/theorems. --- Bookshelf.lean | 3 +- Bookshelf/Sequence/Arithmetic.lean | 66 +++++++++++++++++++ Bookshelf/Sequence/Geometric.lean | 49 ++++++++++++++ .../theorem-proving-in-lean/exercises-2.lean | 0 .../theorem-proving-in-lean/exercises-3.lean | 0 .../theorem-proving-in-lean/exercises-4.lean | 0 .../theorem-proving-in-lean/exercises-5.lean | 0 .../theorem-proving-in-lean/exercises-7.lean | 0 .../theorem-proving-in-lean/exercises-8.lean | 0 lake-manifest.json | 27 ++++++++ lakefile.lean | 3 + 11 files changed, 147 insertions(+), 1 deletion(-) create mode 100644 Bookshelf/Sequence/Arithmetic.lean create mode 100644 Bookshelf/Sequence/Geometric.lean rename {src => exercises}/theorem-proving-in-lean/exercises-2.lean (100%) rename {src => exercises}/theorem-proving-in-lean/exercises-3.lean (100%) rename {src => exercises}/theorem-proving-in-lean/exercises-4.lean (100%) rename {src => exercises}/theorem-proving-in-lean/exercises-5.lean (100%) rename {src => exercises}/theorem-proving-in-lean/exercises-7.lean (100%) rename {src => exercises}/theorem-proving-in-lean/exercises-8.lean (100%) create mode 100644 lake-manifest.json diff --git a/Bookshelf.lean b/Bookshelf.lean index e99d3a6..037efd7 100644 --- a/Bookshelf.lean +++ b/Bookshelf.lean @@ -1 +1,2 @@ -def hello := "world" \ No newline at end of file +import Bookshelf.Sequence.Arithmetic +import Bookshelf.Sequence.Geometric diff --git a/Bookshelf/Sequence/Arithmetic.lean b/Bookshelf/Sequence/Arithmetic.lean new file mode 100644 index 0000000..03d84cb --- /dev/null +++ b/Bookshelf/Sequence/Arithmetic.lean @@ -0,0 +1,66 @@ +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Ring + +/-- +A 0th-indexed arithmetic sequence. +-/ +structure Arithmetic where + a₀ : Int + Δ : Int + +namespace Arithmetic + +/-- +Returns the value of the `n`th term of an arithmetic sequence. +-/ +def termClosed (seq : Arithmetic) (n : Nat) : Int := seq.a₀ + seq.Δ * n + +/-- +Returns the value of the `n`th term of an arithmetic sequence. +-/ +def termRecursive : Arithmetic → Nat → Int + | seq, 0 => seq.a₀ + | seq, (n + 1) => seq.Δ + seq.termRecursive n + +/-- +The recursive definition and closed definitions of an arithmetic sequence are +equivalent. +-/ +theorem term_recursive_closed (seq : Arithmetic) (n : Nat) + : seq.termRecursive n = seq.termClosed n := + Nat.recOn + n + (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) + +/-- +Summation of the first `n` terms of an arithmetic sequence. +-/ +def sum : Arithmetic → Nat → Int + | _, 0 => 0 + | seq, (n + 1) => seq.termClosed n + seq.sum n + +/-- +The closed formula of the summation of the first `n` terms of an arithmetic +series. +--/ +theorem sum_closed_formula (seq : Arithmetic) (n : Nat) + : seq.sum n = (n / 2) * (seq.a₀ + seq.termClosed (n - 1)) := + Nat.recOn + n + (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) + +end Arithmetic \ No newline at end of file diff --git a/Bookshelf/Sequence/Geometric.lean b/Bookshelf/Sequence/Geometric.lean new file mode 100644 index 0000000..d1a86c5 --- /dev/null +++ b/Bookshelf/Sequence/Geometric.lean @@ -0,0 +1,49 @@ +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Ring + +/-- +A 0th-indexed geometric sequence. +-/ +structure Geometric where + a₀ : Int + r : Int + +namespace Geometric + +/-- +The value of the `n`th term of an geometric sequence. +-/ +def termClosed (seq : Geometric) (n : Nat) : Int := seq.a₀ * seq.r ^ n + +/-- +The value of the `n`th term of an geometric sequence. +-/ +def termRecursive : Geometric → Nat → Int + | seq, 0 => seq.a₀ + | seq, (n + 1) => seq.r * (seq.termRecursive n) + +/-- +The recursive definition and closed definitions of a geometric sequence are +equivalent. +-/ +theorem term_recursive_closed (seq : Geometric) (n : Nat) + : seq.termRecursive n = seq.termClosed n := + Nat.recOn + n + (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) + +/-- +Summation of the first `n` terms of a geometric sequence. +-/ +def sum : Geometric → Nat → Int + | _, 0 => 0 + | seq, (n + 1) => seq.termClosed n + seq.sum n + +end Geometric \ No newline at end of file diff --git a/src/theorem-proving-in-lean/exercises-2.lean b/exercises/theorem-proving-in-lean/exercises-2.lean similarity index 100% rename from src/theorem-proving-in-lean/exercises-2.lean rename to exercises/theorem-proving-in-lean/exercises-2.lean diff --git a/src/theorem-proving-in-lean/exercises-3.lean b/exercises/theorem-proving-in-lean/exercises-3.lean similarity index 100% rename from src/theorem-proving-in-lean/exercises-3.lean rename to exercises/theorem-proving-in-lean/exercises-3.lean diff --git a/src/theorem-proving-in-lean/exercises-4.lean b/exercises/theorem-proving-in-lean/exercises-4.lean similarity index 100% rename from src/theorem-proving-in-lean/exercises-4.lean rename to exercises/theorem-proving-in-lean/exercises-4.lean diff --git a/src/theorem-proving-in-lean/exercises-5.lean b/exercises/theorem-proving-in-lean/exercises-5.lean similarity index 100% rename from src/theorem-proving-in-lean/exercises-5.lean rename to exercises/theorem-proving-in-lean/exercises-5.lean diff --git a/src/theorem-proving-in-lean/exercises-7.lean b/exercises/theorem-proving-in-lean/exercises-7.lean similarity index 100% rename from src/theorem-proving-in-lean/exercises-7.lean rename to exercises/theorem-proving-in-lean/exercises-7.lean diff --git a/src/theorem-proving-in-lean/exercises-8.lean b/exercises/theorem-proving-in-lean/exercises-8.lean similarity index 100% rename from src/theorem-proving-in-lean/exercises-8.lean rename to exercises/theorem-proving-in-lean/exercises-8.lean diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..fe3e9de --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,27 @@ +{"version": 4, + "packagesDir": "lake-packages", + "packages": + [{"git": + {"url": "https://github.com/leanprover-community/mathlib4.git", + "subDir?": null, + "rev": "065e9956724008d1059577700fd676eaf25f35d5", + "name": "mathlib", + "inputRev?": null}}, + {"git": + {"url": "https://github.com/gebner/quote4", + "subDir?": null, + "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf", + "name": "Qq", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/JLimperg/aesop", + "subDir?": null, + "rev": "ba61f7fec6174d8c7d2796457da5a8d0b0da44c6", + "name": "aesop", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "de7e2a79905a3f87cad1ad5bf57045206f9738c7", + "name": "std", + "inputRev?": "main"}}]} diff --git a/lakefile.lean b/lakefile.lean index e91ff6f..3d0e994 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,6 +1,9 @@ import Lake open Lake DSL +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" + package «bookshelf» { -- add package configuration options here }