diff --git a/common/Bookshelf.lean b/bookshelf/Bookshelf.lean similarity index 60% rename from common/Bookshelf.lean rename to bookshelf/Bookshelf.lean index 0778a0a..f4bb429 100644 --- a/common/Bookshelf.lean +++ b/bookshelf/Bookshelf.lean @@ -1,3 +1,4 @@ import Bookshelf.Sequence.Arithmetic import Bookshelf.Sequence.Geometric -import Bookshelf.Tuple \ No newline at end of file +import Bookshelf.Tuple +import Bookshelf.Vector diff --git a/common/Bookshelf/Sequence/Arithmetic.lean b/bookshelf/Bookshelf/Sequence/Arithmetic.lean similarity index 100% rename from common/Bookshelf/Sequence/Arithmetic.lean rename to bookshelf/Bookshelf/Sequence/Arithmetic.lean diff --git a/common/Bookshelf/Sequence/Geometric.lean b/bookshelf/Bookshelf/Sequence/Geometric.lean similarity index 100% rename from common/Bookshelf/Sequence/Geometric.lean rename to bookshelf/Bookshelf/Sequence/Geometric.lean diff --git a/bookshelf/Bookshelf/Tuple.lean b/bookshelf/Bookshelf/Tuple.lean new file mode 100644 index 0000000..d31843b --- /dev/null +++ b/bookshelf/Bookshelf/Tuple.lean @@ -0,0 +1,118 @@ +/- +# References + +1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: + Harcourt/Academic Press, 2001. +2. Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in + Mathematics. Cham: Springer International Publishing, 2015. + https://doi.org/10.1007/978-3-319-11080-6. +-/ + +import Mathlib.Tactic.Ring + +universe u + +/-- +As described in [1], `n`-tuples are defined recursively as such: + + `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩` + +We allow for empty tuples; [2] expects this functionality. + +For a `Tuple`-like type with opposite "endian", refer to `Vector`. + +TODO: It would be nice to define `⟨x⟩ = x`. It's not clear to me yet how to do +so or whether I could leverage a simple isomorphism everywhere I would like +this. +-/ +inductive Tuple : (α : Type u) → (size : Nat) → Type u where + | nil : Tuple α 0 + | snoc : Tuple α n → α → Tuple α (n + 1) + +syntax (priority := high) "t[" term,* "]" : term + +macro_rules + | `(t[]) => `(Tuple.nil) + | `(t[$x]) => `(Tuple.snoc t[] $x) + | `(t[$xs:term,*, $x]) => `(Tuple.snoc t[$xs,*] $x) + +namespace Tuple + +theorem eq_nil : @Tuple.nil α = t[] := rfl + +theorem eq_iff_singleton : (a = b) ↔ (t[a] = t[b]) := by + apply Iff.intro + · intro h; rw [h] + · intro h; injection h + +theorem eq_iff_snoc {t₁ t₂ : Tuple α n} + : (a = b ∧ t₁ = t₂) ↔ (snoc t₁ a = snoc t₂ b) := by + apply Iff.intro + · intro ⟨h₁, h₂ ⟩; rw [h₁, h₂] + · intro h + injection h with _ h₁ h₂ + exact And.intro h₂ h₁ + +/-- +Implements decidable equality for `Tuple α m`, provided `a` has decidable equality. +-/ +protected def hasDecEq [DecidableEq α] (t₁ t₂ : Tuple α n) : Decidable (Eq t₁ t₂) := + match t₁, t₂ with + | t[], t[] => isTrue eq_nil + | snoc as a, snoc bs b => + match Tuple.hasDecEq as bs with + | isFalse np => isFalse (fun h => absurd (eq_iff_snoc.mpr h).right np) + | isTrue hp => + if hq : a = b then + isTrue (eq_iff_snoc.mp $ And.intro hq hp) + else + isFalse (fun h => absurd (eq_iff_snoc.mpr h).left hq) + +instance [DecidableEq α] : DecidableEq (Tuple α n) := Tuple.hasDecEq + +/-- +Returns the number of entries of the `Tuple`. +-/ +def size (_ : Tuple α n) : Nat := n + +/-- +Returns all but the last entry of the `Tuple`. +-/ +def init : Tuple α n → 1 ≤ n → Tuple α (n - 1) + | snoc vs _, _ => vs + +/-- +Returns the last entry of the `Tuple`. +-/ +def last : Tuple α n → 1 ≤ n → α + | snoc _ v, _ => v + +/-- +Prepends an entry to the start of the `Tuple`. +-/ +def cons : Tuple α n → α → Tuple α (n + 1) + | t[], a => t[a] + | snoc ts t, a => snoc (cons ts a) t + +/-- +Join two `Tuple`s together end to end. +-/ +def concat : Tuple α m → Tuple α n → Tuple α (m + n) + | t[], ts => cast (by simp) ts + | is, t[] => is + | is, snoc ts t => snoc (concat is ts) t + +/-- +Take the first `k` entries from the `Tuple` to form a new `Tuple`. +-/ +def take (t : Tuple α n) (k : Nat) (p : 1 ≤ k ∧ k ≤ n) : Tuple α k := + have _ : 1 ≤ n := Nat.le_trans p.left p.right + match t with + | @snoc _ n' init last => by + by_cases h : k = n' + 1 + · rw [h]; exact snoc init last + · exact take init k (And.intro p.left $ + have h' : k + 1 ≤ n' + 1 := Nat.lt_of_le_of_ne p.right h + by simp at h'; exact h') + +end Tuple diff --git a/bookshelf/Bookshelf/Vector.lean b/bookshelf/Bookshelf/Vector.lean new file mode 100644 index 0000000..e402f3c --- /dev/null +++ b/bookshelf/Bookshelf/Vector.lean @@ -0,0 +1,54 @@ +import Mathlib.Tactic.Ring + +/-- +A list-like structure with its size encoded in the type. + +For a `Vector`-like type with opposite "endian", refer to `Tuple`. +-/ +inductive Vector (α : Type u) : (size : Nat) → Type u where + | nil : Vector α 0 + | cons : α → Vector α n → Vector α (n + 1) + +syntax (priority := high) "v[" term,* "]" : term + +macro_rules + | `(v[]) => `(Vector.nil) + | `(v[$x]) => `(Vector.cons $x v[]) + | `(v[$x, $xs:term,*]) => `(Vector.cons $x v[$xs,*]) + +namespace Vector + +/-- +Returns the number of entries in the `Vector`. +-/ +def size (_ : Vector α n) : Nat := n + +/-- +Returns the first entry of the `Vector`. +-/ +def head : Vector α n → 1 ≤ n → α + | cons v _, _ => v + +/-- +Returns the last entry of the `Vector`. +-/ +def last (v : Vector α n) : 1 ≤ n → α := + fun h => + match v with + | nil => by ring_nf at h; exact h.elim + | @cons _ n' v vs => if h' : n' > 0 then vs.last h' else v + +/-- +Returns all but the `head` of the `Vector`. +-/ +def tail : Vector α n → 1 ≤ n → Vector α (n - 1) + | cons _ vs, _ => vs + +/-- +Appends an entry to the end of the `Vector`. +-/ +def snoc : Vector α n → α → Vector α (n + 1) + | nil, a => v[a] + | cons v vs, a => cons v (snoc vs a) + +end Vector diff --git a/common/lake-manifest.json b/bookshelf/lake-manifest.json similarity index 100% rename from common/lake-manifest.json rename to bookshelf/lake-manifest.json diff --git a/common/lakefile.lean b/bookshelf/lakefile.lean similarity index 59% rename from common/lakefile.lean rename to bookshelf/lakefile.lean index 033e036..fd40766 100644 --- a/common/lakefile.lean +++ b/bookshelf/lakefile.lean @@ -4,9 +4,9 @@ open Lake DSL require mathlib from git "https://github.com/leanprover-community/mathlib4.git" -package «Common» +package «Bookshelf» @[default_target] -lean_lib «Common» { - roots := #["Bookshelf"] +lean_lib «Bookshelf» { + -- add library configuration options here } diff --git a/bookshelf/theorem-proving-in-lean/lean-toolchain b/bookshelf/lean-toolchain similarity index 100% rename from bookshelf/theorem-proving-in-lean/lean-toolchain rename to bookshelf/lean-toolchain diff --git a/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean b/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean deleted file mode 100644 index 3216b75..0000000 --- a/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean +++ /dev/null @@ -1,6 +0,0 @@ -/- -# 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/common/Bookshelf/Tuple.lean b/common/Bookshelf/Tuple.lean deleted file mode 100644 index 6bc264d..0000000 --- a/common/Bookshelf/Tuple.lean +++ /dev/null @@ -1,93 +0,0 @@ -/- -# References - -1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: - Harcourt/Academic Press, 2001. -2. Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in - Mathematics. Cham: Springer International Publishing, 2015. - https://doi.org/10.1007/978-3-319-11080-6. --/ - -import Mathlib.Tactic.Ring - -universe u - -/--[1] -An `n`-tuple is defined recursively as: - - `⟨x₁, ..., xₙ₊₁⟩ = ⟨⟨x₁, ..., xₙ⟩, xₙ₊₁⟩` - -As [1] notes, it is useful to define `⟨x⟩ = x`. It is not clear this would be -possible in Lean though. - -Though [1] does not describe a notion of an empty tuple, [2] does (though under -the name of a "list"). ---/ -inductive Tuple : (α : Type u) → Nat → Type u where - | nil : Tuple α 0 - | snoc : {n : Nat} → Tuple α n → α → Tuple α (n + 1) - -syntax (priority := high) "⟨" term,+ "⟩" : term - --- Notice the ambiguity this syntax introduces. For example, pattern `⟨a, b⟩` --- could refer to a `2`-tuple or an `n`-tuple, where `a` is an `(n-1)`-tuple. -macro_rules - | `(⟨$x⟩) => `(Tuple.snoc Tuple.nil $x) - | `(⟨$xs:term,*, $x⟩) => `(Tuple.snoc ⟨$xs,*⟩ $x) - -namespace Tuple - -def length : Tuple α n → Nat - | Tuple.nil => 0 - | Tuple.snoc init _ => length init + 1 - -theorem nil_length_zero : length (@Tuple.nil α) = 0 := - rfl - -theorem snoc_length_succ : length (Tuple.snoc init last) = length init + 1 := - rfl - -theorem tuple_length {n : Nat} (t : Tuple α n) : length t = n := - Tuple.recOn t nil_length_zero - fun _ _ ih => by - rw [snoc_length_succ] - norm_num - exact ih - -def head : {n : Nat} → Tuple α n → n ≥ 1 → α - | n + 1, Tuple.snoc init last, h => by - by_cases k : 0 = n - · exact last - · have h' : 0 ≤ n := Nat.le_of_succ_le_succ h - exact head init (Nat.lt_of_le_of_ne h' k) - -def last : Tuple α n → n ≥ 1 → α - | Tuple.snoc _ last, _ => last - -def index : {n : Nat} → Tuple α n → (k : Nat) → 1 ≤ k ∧ k ≤ n → α - | 0, _, m, h => by - have ff : 1 ≤ 0 := Nat.le_trans h.left h.right - ring_nf at ff - exact False.elim ff - | n + 1, Tuple.snoc init last, k, h => by - by_cases hₖ : k = n + 1 - · exact last - · exact index init k $ And.intro - h.left - (Nat.le_of_lt_succ $ Nat.lt_of_le_of_ne h.right hₖ) - -/- - --- TODO: Prove `eq_by_index`. --- TODO: Prove Lemma 0A [1]. - -theorem eq_by_index (t₁ t₂ : Tuple α n) - : (t₁ = t₂) ↔ (∀ i : Nat, (p : 1 ≤ i ∧ i ≤ n) → index t₁ i p = index t₂ i p) := by - apply Iff.intro - · intro teq i hᵢ - sorry - · sorry - --/ - -end Tuple diff --git a/bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic.lean b/mathematical-introduction-logic/MathematicalIntroductionLogic.lean similarity index 100% rename from bookshelf/mathematical-introduction-logic/MathematicalIntroductionLogic.lean rename to mathematical-introduction-logic/MathematicalIntroductionLogic.lean diff --git a/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean b/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean new file mode 100644 index 0000000..d560c77 --- /dev/null +++ b/mathematical-introduction-logic/MathematicalIntroductionLogic/Chapter0.lean @@ -0,0 +1,109 @@ +/- +# References + +1. Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: + Harcourt/Academic Press, 2001. +-/ + +import Bookshelf.Tuple + +/-- +The following describes a so-called "generic" tuple. Like in `Bookshelf.Tuple`, +an `n`-tuple is defined recursively like so: + + `⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩` + +Unlike `Bookshelf.Tuple`, a "generic" tuple bends the syntax above further. For +example, both tuples above are equivalent to: + + `⟨⟨x₁, ..., xₘ⟩, xₘ₊₁, ..., xₙ⟩` + +for some `1 ≤ m ≤ n`. This distinction is purely syntactic, but necessary to +prove certain theorems found in [1] (e.g. `lemma_0a`). + +In general, prefer `Bookshelf.Tuple`. +-/ +inductive XTuple : (α : Type u) → (size : Nat × Nat) → Type u where + | nil : XTuple α (0, 0) + | snoc : XTuple α (p, q) → Tuple α r → XTuple α (p + q, r) + +syntax (priority := high) "x[" term,* "]" : term + +macro_rules + | `(x[]) => `(XTuple.nil) + | `(x[$x]) => `(XTuple.snoc x[] t[$x]) + | `(x[x[$xs:term,*], $ys:term,*]) => `(XTuple.snoc x[$xs,*] t[$ys,*]) + | `(x[$x, $xs:term,*]) => `(XTuple.snoc x[] t[$x, $xs,*]) + +namespace XTuple + +/-- +Converts an `XTuple` into "normal form". +-/ +def norm : XTuple α (m, n) → Tuple α (m + n) + | x[] => t[] + | snoc x[] ts => cast (by simp) ts + | snoc is ts => is.norm.concat ts + +/-- +Casts a tuple indexed by `m` to one indexed by `n`. +-/ +theorem cast_eq_size : (m = n) → (Tuple α m = Tuple α n) := + fun h => by rw [h] + +/-- +Implements Boolean equality for `XTuple α n` provided `α` has decidable +equality. +-/ +instance BEq [DecidableEq α] : BEq (XTuple α n) where + beq t₁ t₂ := t₁.norm == t₂.norm + +/-- +Returns the number of entries in the `XTuple`. +-/ +def size (_ : XTuple α n) := n + +/-- +Returns the number of entries in the "shallowest" portion of the `XTuple`. For +example, the length of `x[x[1, 2], 3, 4]` is `3`, despite its size being `4`. +-/ +def length : XTuple α n → Nat + | x[] => 0 + | snoc x[] ts => ts.size + | snoc _ ts => 1 + ts.size + +/-- +Returns the first component of our `XTuple`. For example, the first component of +tuple `x[x[1, 2], 3, 4]` is `t[1, 2]`. +-/ +def first : XTuple α (m, n) → 1 ≤ m → Tuple α m + | snoc ts _, _ => ts.norm + +section + +variable {k m n : Nat} +variable (p : n + (m - 1) = m + k) +variable (qₙ : 1 ≤ n) +variable (qₘ : 1 ≤ m) + +namespace Lemma_0a + +lemma aux1 : n = k + 1 := sorry + +lemma aux2 : 1 ≤ m → 1 ≤ k + 1 ∧ k + 1 ≤ m + k := sorry + +end Lemma_0a + +open Lemma_0a + +/--[1] +Assume that ⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩. Then x₁ = ⟨y₁, ..., yₖ₊₁⟩. +-/ +theorem lemma_0a (xs : XTuple α (n, m - 1)) (ys : Tuple α (m + k)) + : (cast (cast_eq_size p) xs.norm = ys) + → (cast (cast_eq_size aux1) (xs.first qₙ) = ys.take (k + 1) (aux2 qₘ)) + := sorry + +end + +end XTuple diff --git a/mathematical-introduction-logic/lake-manifest.json b/mathematical-introduction-logic/lake-manifest.json new file mode 100644 index 0000000..2810171 --- /dev/null +++ b/mathematical-introduction-logic/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": "7e974fd3806866272e9f6d9e44fa04c210a21f87", + "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/bookshelf/mathematical-introduction-logic/lakefile.lean b/mathematical-introduction-logic/lakefile.lean similarity index 82% rename from bookshelf/mathematical-introduction-logic/lakefile.lean rename to mathematical-introduction-logic/lakefile.lean index 60550a7..9ea98f4 100644 --- a/bookshelf/mathematical-introduction-logic/lakefile.lean +++ b/mathematical-introduction-logic/lakefile.lean @@ -3,6 +3,8 @@ open Lake DSL package «mathematical-introduction-logic» +require Bookshelf from "../bookshelf" + @[default_target] lean_lib «MathematicalIntroductionLogic» { -- add library configuration options here diff --git a/bookshelf/mathematical-introduction-logic/lean-toolchain b/mathematical-introduction-logic/lean-toolchain similarity index 100% rename from bookshelf/mathematical-introduction-logic/lean-toolchain rename to mathematical-introduction-logic/lean-toolchain diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean.lean b/theorem-proving-in-lean/TheoremProvingInLean.lean similarity index 100% rename from bookshelf/theorem-proving-in-lean/TheoremProvingInLean.lean rename to theorem-proving-in-lean/TheoremProvingInLean.lean diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean b/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean similarity index 100% rename from bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean rename to theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean b/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean similarity index 100% rename from bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean rename to theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean b/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean similarity index 100% rename from bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean rename to theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean b/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean similarity index 100% rename from bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean rename to theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean b/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean similarity index 100% rename from bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean rename to theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean b/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean similarity index 100% rename from bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean rename to theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean diff --git a/bookshelf/theorem-proving-in-lean/lake-manifest.json b/theorem-proving-in-lean/lake-manifest.json similarity index 100% rename from bookshelf/theorem-proving-in-lean/lake-manifest.json rename to theorem-proving-in-lean/lake-manifest.json diff --git a/bookshelf/theorem-proving-in-lean/lakefile.lean b/theorem-proving-in-lean/lakefile.lean similarity index 100% rename from bookshelf/theorem-proving-in-lean/lakefile.lean rename to theorem-proving-in-lean/lakefile.lean diff --git a/common/lean-toolchain b/theorem-proving-in-lean/lean-toolchain similarity index 100% rename from common/lean-toolchain rename to theorem-proving-in-lean/lean-toolchain