From c92dee8e3d1e0369a8ebf732430315ac9aa98a0f Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 20 Feb 2023 18:05:15 -0700 Subject: [PATCH] Add `Tuple` module for use in mathematical-introduction-logic, chapter 1. --- .../MathematicalIntroductionLogic.lean | 7 +++ .../Chapter0.lean | 6 ++ .../lakefile.lean | 9 +++ .../lean-toolchain | 1 + common/Bookshelf.lean | 3 + .../{ => Bookshelf}/Sequence/Arithmetic.lean | 19 ++++-- .../{ => Bookshelf}/Sequence/Geometric.lean | 17 ++++-- common/Bookshelf/Tuple.lean | 59 +++++++++++++++++++ common/Sequence.lean | 2 - common/lakefile.lean | 2 +- 10 files changed, 111 insertions(+), 14 deletions(-) create mode 100644 bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic.lean create mode 100644 bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean create mode 100644 bookshelf/mathematical-introduction-logic/lakefile.lean create mode 100644 bookshelf/mathematical-introduction-logic/lean-toolchain create mode 100644 common/Bookshelf.lean rename common/{ => Bookshelf}/Sequence/Arithmetic.lean (90%) rename common/{ => Bookshelf}/Sequence/Geometric.lean (85%) create mode 100644 common/Bookshelf/Tuple.lean delete mode 100644 common/Sequence.lean diff --git a/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic.lean b/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic.lean new file mode 100644 index 0000000..d34aba4 --- /dev/null +++ b/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic.lean @@ -0,0 +1,7 @@ +/- +# References + +1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: + Harcourt/Academic Press, 2001. +-/ +import MathematicalIntroductionLogic.Chapter0 diff --git a/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean b/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean new file mode 100644 index 0000000..3216b75 --- /dev/null +++ b/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean @@ -0,0 +1,6 @@ +/- +# References + +1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: + Harcourt/Academic Press, 2001. +-/ \ No newline at end of file diff --git a/bookshelf/mathematical-introduction-logic/lakefile.lean b/bookshelf/mathematical-introduction-logic/lakefile.lean new file mode 100644 index 0000000..60550a7 --- /dev/null +++ b/bookshelf/mathematical-introduction-logic/lakefile.lean @@ -0,0 +1,9 @@ +import Lake +open Lake DSL + +package «mathematical-introduction-logic» + +@[default_target] +lean_lib «MathematicalIntroductionLogic» { + -- add library configuration options here +} diff --git a/bookshelf/mathematical-introduction-logic/lean-toolchain b/bookshelf/mathematical-introduction-logic/lean-toolchain new file mode 100644 index 0000000..19d47bf --- /dev/null +++ b/bookshelf/mathematical-introduction-logic/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2023-02-12 diff --git a/common/Bookshelf.lean b/common/Bookshelf.lean new file mode 100644 index 0000000..0778a0a --- /dev/null +++ b/common/Bookshelf.lean @@ -0,0 +1,3 @@ +import Bookshelf.Sequence.Arithmetic +import Bookshelf.Sequence.Geometric +import Bookshelf.Tuple \ No newline at end of file diff --git a/common/Sequence/Arithmetic.lean b/common/Bookshelf/Sequence/Arithmetic.lean similarity index 90% rename from common/Sequence/Arithmetic.lean rename to common/Bookshelf/Sequence/Arithmetic.lean index 03d84cb..ebb9d85 100644 --- a/common/Sequence/Arithmetic.lean +++ b/common/Bookshelf/Sequence/Arithmetic.lean @@ -1,7 +1,14 @@ +/- +# References + +1. Levin, Oscar. Discrete Mathematics: An Open Introduction. 3rd ed., n.d. + https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf. +-/ + import Mathlib.Tactic.NormNum import Mathlib.Tactic.Ring -/-- +/--[1] A 0th-indexed arithmetic sequence. -/ structure Arithmetic where @@ -10,19 +17,19 @@ structure Arithmetic where namespace Arithmetic -/-- +/--[1] Returns the value of the `n`th term of an arithmetic sequence. -/ def termClosed (seq : Arithmetic) (n : Nat) : Int := seq.a₀ + seq.Δ * n -/-- +/--[1] 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 -/-- +/--[1] The recursive definition and closed definitions of an arithmetic sequence are equivalent. -/ @@ -39,14 +46,14 @@ theorem term_recursive_closed (seq : Arithmetic) (n : Nat) _ = seq.a₀ + seq.Δ * (n + 1) := by ring _ = termClosed seq (n + 1) := rfl) -/-- +/--[1] 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 -/-- +/--[1] The closed formula of the summation of the first `n` terms of an arithmetic series. --/ diff --git a/common/Sequence/Geometric.lean b/common/Bookshelf/Sequence/Geometric.lean similarity index 85% rename from common/Sequence/Geometric.lean rename to common/Bookshelf/Sequence/Geometric.lean index d1a86c5..11c94ce 100644 --- a/common/Sequence/Geometric.lean +++ b/common/Bookshelf/Sequence/Geometric.lean @@ -1,7 +1,14 @@ +/- +# References + +1. Levin, Oscar. Discrete Mathematics: An Open Introduction. 3rd ed., n.d. + https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf. +-/ + import Mathlib.Tactic.NormNum import Mathlib.Tactic.Ring -/-- +/--[1] A 0th-indexed geometric sequence. -/ structure Geometric where @@ -10,19 +17,19 @@ structure Geometric where namespace Geometric -/-- +/--[1] The value of the `n`th term of an geometric sequence. -/ def termClosed (seq : Geometric) (n : Nat) : Int := seq.a₀ * seq.r ^ n -/-- +/--[1] 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) -/-- +/--[1] The recursive definition and closed definitions of a geometric sequence are equivalent. -/ @@ -39,7 +46,7 @@ theorem term_recursive_closed (seq : Geometric) (n : Nat) _ = seq.a₀ * seq.r ^ (n + 1) := by ring _ = seq.termClosed (n + 1) := rfl) -/-- +/--[1] Summation of the first `n` terms of a geometric sequence. -/ def sum : Geometric → Nat → Int diff --git a/common/Bookshelf/Tuple.lean b/common/Bookshelf/Tuple.lean new file mode 100644 index 0000000..23c6461 --- /dev/null +++ b/common/Bookshelf/Tuple.lean @@ -0,0 +1,59 @@ +/- +# References + +1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: + Harcourt/Academic Press, 2001. +-/ + +import Mathlib.Tactic.Ring + +universe u + +/--[1] +An n-tuple is defined recursively as: + + ⟨x₁, ..., xₙ₊₁⟩ = ⟨⟨x₁, ..., xₙ⟩, xₙ₊₁⟩ + +As [1] notes, it is also useful to define ⟨x⟩ = x. +--/ +inductive Tuple (α : Type u) : Nat → Type u where + | nil : Tuple α 0 + | cons : {n : Nat} → Tuple α n → α → Tuple α (n + 1) + +syntax (priority := high) "⟨" term,+ "⟩" : term + +macro_rules + | `(⟨$x⟩) => `(Tuple.cons Tuple.nil $x) + | `(⟨$xs:term,*, $x⟩) => `(Tuple.cons ⟨$xs,*⟩ $x) + +namespace Tuple + +/-- +Returns the value at the nth-index of the given tuple. +-/ +def index (t : Tuple α n) (m : Nat) : 1 ≤ m ∧ m ≤ n → α := by + intro h + cases t + · case nil => + have ff : 1 ≤ 0 := Nat.le_trans h.left h.right + ring_nf at ff + exact False.elim ff + . case cons n' init last => + by_cases k : m = n' + 1 + · exact last + · exact index init m (And.intro h.left (by + have h₂ : m + 1 ≤ n' + 1 := Nat.lt_of_le_of_ne h.right k + norm_num at h₂ + exact h₂)) + +-- TODO: Prove the following theorem + +theorem eq_by_index (t₁ t₂ : Tuple α n) + : (t₁ = t₂) ↔ (∀ i : Nat, 1 ≤ i ∧ i ≤ n → index t₁ i = index t₂ i) := by + apply Iff.intro + · sorry + · sorry + +-- TODO: [1] Lemma 0A + +end Tuple \ No newline at end of file diff --git a/common/Sequence.lean b/common/Sequence.lean deleted file mode 100644 index a56ac94..0000000 --- a/common/Sequence.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Sequence.Arithmetic -import Sequence.Geometric \ No newline at end of file diff --git a/common/lakefile.lean b/common/lakefile.lean index b27615a..033e036 100644 --- a/common/lakefile.lean +++ b/common/lakefile.lean @@ -8,5 +8,5 @@ package «Common» @[default_target] lean_lib «Common» { - roots := #["Sequence"] + roots := #["Bookshelf"] }