From cbf4528bbc6f6fc8ded92f1a08fa0acd487cd77e Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 14 Aug 2023 20:37:09 -0600 Subject: [PATCH] Enderton (logic). Begin writing out Lean proofs for Exercises 1. --- Bookshelf/Enderton/Logic.lean | 4 +- Bookshelf/Enderton/Logic.tex | 158 +++++++++++++++++--- Bookshelf/Enderton/Logic/Chapter_0.lean | 10 -- Bookshelf/Enderton/Logic/Chapter_1.lean | 184 ++++++++++++++++++++++++ Bookshelf/Enderton/Set.tex | 177 +++++++++++++++-------- Bookshelf/Enderton/Set/Chapter_3.lean | 4 +- Bookshelf/Enderton/Set/Relation.lean | 6 +- Common/Nat/Basic.lean | 7 + DocGen4/Output/Index.lean | 1 + 9 files changed, 459 insertions(+), 92 deletions(-) delete mode 100644 Bookshelf/Enderton/Logic/Chapter_0.lean create mode 100644 Bookshelf/Enderton/Logic/Chapter_1.lean diff --git a/Bookshelf/Enderton/Logic.lean b/Bookshelf/Enderton/Logic.lean index 085cec3..3edb997 100644 --- a/Bookshelf/Enderton/Logic.lean +++ b/Bookshelf/Enderton/Logic.lean @@ -1,3 +1 @@ -import Bookshelf.Enderton.Logic.Chapter_0 - -#check Iff \ No newline at end of file +import Bookshelf.Enderton.Logic.Chapter_1 \ No newline at end of file diff --git a/Bookshelf/Enderton/Logic.tex b/Bookshelf/Enderton/Logic.tex index a0892dc..9e49edf 100644 --- a/Bookshelf/Enderton/Logic.tex +++ b/Bookshelf/Enderton/Logic.tex @@ -62,13 +62,20 @@ & = (\alpha \Leftrightarrow \beta) \end{align*} - \lean{Init/Prelude}{Not} + \code*{Bookshelf/Enderton/Logic/Chapter\_1} + {Enderton.Logic.Chapter\_1.WFF} - \lean{Init/Prelude}{And} + \lean{Init/Prelude} + {Not} - \lean{Init/Prelude}{Or} + \lean{Init/Prelude} + {And} - \lean{Init/Core}{Iff} + \lean{Init/Prelude} + {Or} + + \lean{Init/Core} + {Iff} \section{\defined{\texorpdfstring{$n$}{n}-tuple}}% \hyperlabel{ref:n-tuple} @@ -78,7 +85,8 @@ for $n > 1$. We also define $\tuple{x} = x$. - \lean*{Init/Prelude}{Prod} + \lean*{Init/Prelude} + {Prod} \section{\defined{Well-Formed Formula}}% \hyperlabel{ref:well-formed-formula} @@ -87,6 +95,9 @@ be built up from the sentence symbols by applying some finite number of times the \nameref{ref:formula-building-operations}. + \code*{Bookshelf/Enderton/Logic/Chapter\_1} + {Enderton.Logic.Chapter\_1.WFF} + \endgroup % Reset counter to mirror Enderton's book. @@ -285,12 +296,18 @@ \end{answer} -\subsection{\unverified{Exercise 1.1.2}}% +\subsection{\pending{Exercise 1.1.2}}% \hyperlabel{sub:exercise-1.1.2} Show that there are no wffs of length 2, 3, or 6, but that any other positive length is possible. + \code*{Enderton.Logic.Chapter\_1} + {Enderton.Logic.Chapter\_1.exercise\_1\_1\_2\_i} + + \code{Enderton.Logic.Chapter\_1} + {Enderton.Logic.Chapter\_1.exercise\_1\_1\_2\_ii} + \begin{proof} Define $$S = \{ \phi \mid @@ -351,7 +368,7 @@ \end{proof} -\subsection{\sorry{Exercise 1.1.3}}% +\subsection{\pending{Exercise 1.1.3}}% \hyperlabel{sub:exercise-1.1.3} Let $\alpha$ be a wff; let $c$ be the number of places at which binary @@ -363,10 +380,64 @@ Show by using the induction principle that $s = c + 1$. \begin{proof} - TODO + + Define + \begin{equation} + \hyperlabel{sub:exercise-1.1.3-eq1} + S = \{\phi \mid \phi \text{ is a wff such that } s = c + 1\}. + \end{equation} + We prove that (i) all the sentence symbols are members of $S$ and (ii) + $S$ is closed under the five \nameref{ref:formula-building-operations}. + We then conclude with (iii) the proof of the theorem statement. + + \paragraph{(i)}% + \hyperlabel{par:exercise-1.1.3-i} + + Let $\phi = A_n$ be an arbitrary sentence symbol. + The number of places at which sentence symbols occur in $\phi$ is 1. + The number of places at which binary connective symbols occur in $\phi$ is + 0. + Hence $\phi \in S$. + + \paragraph{(ii)}% + \hyperlabel{par:exercise-1.1.3-ii} + + Let $\alpha, \beta \in S$. + Denote the number of places at which sentence symbols occur in each as + $s_\alpha$ and $s_\beta$ respectively. + Likewise, denote the number of places at which binary connective symbols + occur as $c_\alpha$ and $c_\beta$. + + By definition, $\mathcal{E}_{\neg}(\alpha) = (\neg\alpha)$. + The number of sentence and binary connective symbols in + $\mathcal{E}_{\neg}(\alpha)$ does not change. + Thus $\mathcal{E}_{\neg}(\alpha) \in S$. + Likewise, + $\mathcal{E}_{\square}(\phi, \psi) = (\phi \mathop{\square} \psi)$ + where $\square$ is one of the binary connectives $\land$, $\lor$, + $\Rightarrow$, $\Leftrightarrow$. + Therefore $\mathcal{E}_{\square}(\phi, \psi)$ has $s_\alpha + s_\beta$ + sentence symbols and $c_\alpha + c_\beta + 1$ binary connective symbols. + But \eqref{sub:exercise-1.1.3-eq1} implies + \begin{align*} + s_\alpha + s_\beta + & = (c_\alpha + 1) + (c_\beta + 1) \\ + & = (c_\alpha + c_\beta + 1) + 1, + \end{align*} + meaning $\mathcal{E}_{\square}(\phi, \psi) \in S$. + + Hence $S$ is closed under the five formula-building operations. + + \paragraph{(iii)}% + \hyperlabel{par:exercise-1.1.3-iii} + + By \nameref{par:exercise-1.1.3-i} and \nameref{par:exercise-1.1.3-ii}, the + \nameref{sub:induction-principle-1} indicates $S$ is the set of all + wffs. + \end{proof} -\subsection{\sorry{Exercise 1.1.4}}% +\subsection{\unverified{Exercise 1.1.4}}% \hyperlabel{sub:exercise-1.1.4} Assume we have a construction sequence ending in $\phi$, where $\phi$ does not @@ -376,20 +447,75 @@ Show that the result is still a legal construction sequence. \begin{proof} - TODO + + + Let $S$ denote a \nameref{ref:construction-sequence} + $\ltuple{\epsilon_1}{\epsilon_n}$ such that $\epsilon_n = \phi$. + Let $S' = \ltuple{\epsilon_{i_1}}{\epsilon_{i_m}}$ denote the construction + sequence resulting from deleting all expressions in $S$ containing $A_4$. + Fix $1 \leq j \leq m$. + Then there exists some $1 \leq k \leq n$ such that + $\epsilon_{i_j} = \epsilon_k$. + By definition of a construction sequence, there are three cases to consider: + + \paragraph{Case 1}% + + Suppose $\epsilon_k$ is a sentence symbol. + Then $\epsilon_{i_j}$ is also sentence symbol. + + \paragraph{Case 2}% + + Suppose $\epsilon_k = \mathcal{E}_{\neg}(\epsilon_a)$ for some $a < k$. + It must be that $A_4$ is not found in $\epsilon_a$, else an immediate + contradiction is raised. + Therefore $\epsilon_a$ is a member of $S'$ that precedes $\epsilon_{i_j}$. + Hence $\epsilon_{i_j} = \mathcal{E}_{\neg}(\epsilon_{i_a})$ for some + $a < j$. + + \paragraph{Case 3}% + + Suppose $\epsilon_k = \mathcal{E}_{\square}(\epsilon_a, \epsilon_b)$ for + some $a, b < k$ where $\square$ is one of the binary connectives + $\land$, $\lor$, $\Rightarrow$, $\Leftrightarrow$. + It must be that $A_4$ is found in neither $\epsilon_a$ nor $\epsilon_b$, + else an immediate contradiction is raised. + Therefore $\epsilon_a$ and $\epsilon_b$ is a member of $S'$, both of which + precede $\epsilon_{i_j}$. + Hence + $\epsilon_{i_j} = \mathcal{E}_{\square}(\epsilon_{i_a}, \epsilon_{i_b})$ + for some $a, b < j$. + + \paragraph{Conclusion}% + + Since the above cases are exhaustive and apply to an arbitrary member of + $S'$, it must be that every member of $S'$ is valid. + Hence $S'$ is still a legal construction sequence. + \end{proof} \subsection{\sorry{Exercise 1.1.5}}% \hyperlabel{sub:exercise-1.1.5} Suppose that $\alpha$ is a wff not containing the negation symbol $\neg$. - \begin{enumerate}[(a)] - \item Show that the length of $\alpha$ (i.e., the number of symbols in the - string) is odd. - \item Show that more than a quarter of the symbols are sentence symbols. - \end{enumerate} + +\subsubsection{\sorry{Exercise 1.1.5a}}% +\hyperlabel{ssub:exercise-1.1.5-a} + + Show that the length of $\alpha$ (i.e., the number of symbols in the string) + is odd. \textit{Suggestion}: Apply induction to show that the length is of the form - $4k + 1$ and the number of sentence symbols is $k + 1$. + $4k + 1$. + + \begin{proof} + TODO + \end{proof} + +\subsubsection{\sorry{Exercise 1.1.6a}}% +\hyperlabel{ssub:exercise-1.1.6-a} + + Show that more than a quarter of the symbols are sentence symbols. + \textit{Suggestion}: Apply induction to show that the number of sentence + symbols is $k + 1$. \begin{proof} TODO diff --git a/Bookshelf/Enderton/Logic/Chapter_0.lean b/Bookshelf/Enderton/Logic/Chapter_0.lean deleted file mode 100644 index 2280256..0000000 --- a/Bookshelf/Enderton/Logic/Chapter_0.lean +++ /dev/null @@ -1,10 +0,0 @@ -/-! # Enderton.Logic.Chapter_0 - -Useful Facts About Sets --/ - -namespace Enderton.Logic.Chapter_0 - --- TODO - -end Enderton.Logic.Chapter_0 diff --git a/Bookshelf/Enderton/Logic/Chapter_1.lean b/Bookshelf/Enderton/Logic/Chapter_1.lean new file mode 100644 index 0000000..f108e99 --- /dev/null +++ b/Bookshelf/Enderton/Logic/Chapter_1.lean @@ -0,0 +1,184 @@ +import Common.Nat.Basic +import Mathlib.Data.Nat.Basic +import Mathlib.Tactic.NormNum + +/-! # Enderton.Logic.Chapter_1 + +Sentential Logic +-/ + +namespace Enderton.Logic.Chapter_1 + +/-- +An abstract representation of a well-formed formula as defined by Enderton. +-/ +inductive Wff where + | SS : Nat → Wff -- e.g. **S**entence **S**ymbol `Aₙ` + | Not : Wff → Wff -- e.g. `(¬ α)` + | And : Wff → Wff → Wff -- e.g. `(α ∧ β)` + | Or : Wff → Wff → Wff -- e.g. `(α ∨ β)` + | Cond : Wff → Wff → Wff -- e.g. `(α → β)` + | Iff : Wff → Wff → Wff -- e.g. `(α ↔ β)` + +namespace Wff + +/-- +Returns the length of the expression, including symbols. +-/ +def length : Wff → ℕ + | Wff.SS _ => 1 + | Wff.Not e => length e + 3 + | Wff.And e₁ e₂ + | Wff.Or e₁ e₂ + | Wff.Cond e₁ e₂ + | Wff.Iff e₁ e₂ => length e₁ + length e₂ + 3 + +/-- +Every well-formed formula has a positive length. +-/ +theorem length_gt_zero (φ : Wff) + : length φ > 0 := by + unfold length + match φ with + | SS _ + | Not _ + | And _ _ + | Or _ _ + | Cond _ _ + | Iff _ _ => simp + +end Wff + +/-! #### Exercise 1.1.2 + +Show that there are no wffs of length `2`, `3`, or `6`, but that any other +positive length is possible. +-/ + +section Exercise_1_1_2 + +private lemma eq_3_by_cases (m n : ℕ) (h : m + n = 3) + : m = 0 ∧ n = 3 ∨ + m = 1 ∧ n = 2 ∨ + m = 2 ∧ n = 1 ∨ + m = 3 ∧ n = 0 := by + have m_le_3 : m ≤ 3 := by + have : m = 3 - n := Eq.symm $ Nat.sub_eq_of_eq_add (Eq.symm h) + rw [this] + norm_num + apply Or.elim (Nat.lt_or_eq_of_le m_le_3) + · intro hm₁ + apply Or.elim (Nat.lt_or_eq_of_lt hm₁) + · intro hm₂ + apply Or.elim (Nat.lt_or_eq_of_lt hm₂) + · intro hm₃ + refine Or.elim (Nat.lt_or_eq_of_lt hm₃) (by simp) ?_ + intro m_eq_0 + rw [m_eq_0, zero_add] at h + left + exact ⟨m_eq_0, h⟩ + · intro m_eq_1 + rw [m_eq_1, add_comm] at h + norm_num at h + right; left + exact ⟨m_eq_1, h⟩ + · intro m_eq_2 + rw [m_eq_2, add_comm] at h + norm_num at h + right; right; left + exact ⟨m_eq_2, h⟩ + · intro m_eq_3 + rw [m_eq_3, add_comm] at h + norm_num at h + right; right; right + exact ⟨m_eq_3, h⟩ + +theorem exercise_1_1_2_i (φ : Wff) + : φ.length ≠ 2 ∧ φ.length ≠ 3 ∧ φ.length ≠ 6 := by + induction φ with + | SS c => + unfold Wff.length + simp + | Not e ih => + unfold Wff.length + refine ⟨by norm_num, ?_, ?_⟩ + · intro h + norm_num at h + have := e.length_gt_zero + rw [h] at this + simp at this + · intro h + norm_num at h + rw [h] at ih + simp at ih + | And e₁ e₂ ih₁ ih₂ + | Or e₁ e₂ ih₁ ih₂ + | Cond e₁ e₂ ih₁ ih₂ + | Iff e₁ e₂ ih₁ ih₂ => + unfold Wff.length + refine ⟨by norm_num, ?_, ?_⟩ + · intro h + norm_num at h + have := e₁.length_gt_zero + rw [h.left] at this + simp at this + · intro h + norm_num at h + apply Or.elim (eq_3_by_cases e₁.length e₂.length h) + · intro h₁ + have := e₁.length_gt_zero + rw [h₁.left] at this + simp at this + · intro h₁ + apply Or.elim h₁ + · intro h₂ + exact absurd h₂.right ih₂.left + intro h₂ + apply Or.elim h₂ + · intro h₃ + exact absurd h₃.left ih₁.left + intro h₃ + exact absurd h₃.left ih₁.right.left + +theorem exercise_1_1_2_ii (n : ℕ) (h : n ≠ 2 ∧ n ≠ 3 ∧ n ≠ 6) + : ∃ φ : Wff, φ.length = n := by + let φ₁ := Wff.SS 1 + let φ₂ := Wff.And φ₁ (Wff.SS 2) + let φ₃ := Wff.And φ₂ (Wff.SS 3) + sorry + +end Exercise_1_1_2 + +/-! #### Exercise 1.1.3 + +Let `α` be a wff; let `c` be the number of places at which binary connective +symbols (`∧`, `∨`, `→`, `↔`) occur in `α`; let `s` be the number of places at +which sentence symbols occur in `α`. (For example, if `α` is `(A → (¬ A))` then +`c = 1` and `s = 2`.) Show by using the induction principle that `s = c + 1`. +-/ + +section Exercise_1_1_3 + +private def binary_symbol_count : Wff → ℕ + | Wff.SS _ => 0 + | Wff.Not e => binary_symbol_count e + | Wff.And e₁ e₂ + | Wff.Or e₁ e₂ + | Wff.Cond e₁ e₂ + | Wff.Iff e₁ e₂ => binary_symbol_count e₁ + binary_symbol_count e₂ + 1 + +private def sentence_symbol_count : Wff → ℕ + | Wff.SS _ => 1 + | Wff.Not e => sentence_symbol_count e + | Wff.And e₁ e₂ + | Wff.Or e₁ e₂ + | Wff.Cond e₁ e₂ + | Wff.Iff e₁ e₂ => sentence_symbol_count e₁ + sentence_symbol_count e₂ + +theorem exercise_1_1_3 (φ : Wff) + : sentence_symbol_count φ = binary_symbol_count φ + 1 := by + sorry + +end Exercise_1_1_3 + +end Enderton.Logic.Chapter_1 diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index e26076c..170ae80 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -35,7 +35,8 @@ \textbf{Addition} ($+$) is the \nameref{ref:binary-operation} on $\omega$ such that for any $m$ and $n$ in $\omega$, $$m + n = A_m(n).$$ - \lean{Init/Prelude}{Add.add} + \lean{Init/Prelude} + {Add.add} \section{\defined{Axiom of Choice, First Form}}% \hyperlabel{ref:axiom-of-choice-1} @@ -43,7 +44,8 @@ For any relation $R$ there is a function $H \subseteq R$ with $\dom{H} = \dom{R}$. - \lean*{Init/Prelude}{Classical.choice} + \lean*{Init/Prelude} + {Classical.choice} \section{\defined{Axiom of Choice, Second Form}}% \hyperlabel{ref:axiom-of-choice-2} @@ -51,7 +53,8 @@ For any set $I$ and any function $H$ with domain $I$, if $H(i) \neq \emptyset$ for all $i \in I$, then $$\bigtimes_{i \in I} H(i) \neq \emptyset.$$ - \lean{Init/Prelude}{Classical.choice} + \lean{Init/Prelude} + {Classical.choice} \section{\defined{Binary Operation}}% \hyperlabel{ref:binary-operation} @@ -79,7 +82,8 @@ only if for all $x$ and $y$ in $A$, $$xRy \Rightarrow F(x)RF(y).$$ - \lean{Init/Core}{Quotient.lift} + \lean{Init/Core} + {Quotient.lift} \section{\defined{Composition}}% \hyperlabel{ref:composition} @@ -87,9 +91,11 @@ The \textbf{composition} of sets $F$ and $G$ is $$F \circ G = \{\tuple{u, v} \mid \exists t(uGt \land tFv)\}.$$ - \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.comp} + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.comp} - \lean{Mathlib/Data/Rel}{Rel.comp} + \lean{Mathlib/Data/Rel} + {Rel.comp} \section{\defined{Connected}}% \hyperlabel{ref:connected} @@ -105,9 +111,11 @@ The \textbf{domain} of set $R$, denoted $\dom{R}$, is given by $$x \in \dom{R} \iff \exists y \tuple{x, y} \in R.$$ - \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.dom} + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.dom} - \lean{Mathlib/Data/Rel}{Rel.dom} + \lean{Mathlib/Data/Rel} + {Rel.dom} \section{\defined{Empty Set Axiom}}% \hyperlabel{ref:empty-set-axiom} @@ -122,7 +130,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and only if there is a one-to-one \nameref{ref:function} from $A$ onto $B$. - \lean*{Mathlib/Init/Function}{Function.Bijective} + \lean*{Mathlib/Init/Function} + {Function.Bijective} \section{\defined{Equivalence Class}}% \hyperlabel{ref:equivalence-class} @@ -133,7 +142,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and (\textbf{modulo $R$}). If the relation $R$ is fixed by the context, we may write just $[x]$. - \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.modEquiv} + \code*{Bookshelf/Enderton/Set/Relation} + {Set.Relation.modEquiv} \section{\defined{Equivalence Relation}}% \hyperlabel{ref:equivalence-relation} @@ -142,7 +152,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and $R$ is a binary \nameref{ref:relation} on $A$ that is \nameref{ref:reflexive} on $A$, \nameref{ref:symmetric}, and \nameref{ref:transitive}. - \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isEquivalence} + \code*{Bookshelf/Enderton/Set/Relation} + {Set.Relation.isEquivalence} \section{\defined{Exponentiation}}% \hyperlabel{ref:exponentiation} @@ -157,7 +168,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and \textbf{Exponentiation} is the \nameref{ref:binary-operation} on $\omega$ such that for any $m$ and $n$ in $\omega$, $$m^n = E_m(n).$$ - \lean{Init/Prelude}{Pow.pow} + \lean{Init/Prelude} + {Pow.pow} \section{\defined{Extensionality Axiom}}% \hyperlabel{ref:extensionality-axiom} @@ -166,7 +178,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and $$\forall A, \forall B, \left[\forall x, (x \in A \iff x \in B) \Rightarrow A = B\right].$$ - \lean{Mathlib/Init/Set}{Set.ext} + \lean{Mathlib/Init/Set} + {Set.ext} \section{\defined{Field}}% \hyperlabel{ref:field} @@ -174,7 +187,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and Given \nameref{ref:relation} $R$, the \textbf{field} of $R$, denoted $\fld{R}$, is given by $$\fld{R} = \dom{R} \cup \ran{R}.$$ - \lean{Bookshelf/Enderton/Set/Relation}{Set.Relation.fld} + \lean{Bookshelf/Enderton/Set/Relation} + {Set.Relation.fld} \section{\defined{Finite Set}}% \hyperlabel{ref:finite-set} @@ -182,7 +196,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and A set is \textbf{finite} if and only if it is \nameref{ref:equinumerous} to a \nameref{ref:natural-number}. - \lean{Mathlib/Data/Finset/Basic}{Finset} + \lean{Mathlib/Data/Finset/Basic} + {Finset} \section{\defined{Function}}% \hyperlabel{ref:function} @@ -200,11 +215,14 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and only one $x$ such that $xFy$. One-to-one functions are sometimes called \textbf{injections}. - \lean*{Mathlib/Init/Function}{Function.Injective} + \lean*{Mathlib/Init/Function} + {Function.Injective} - \lean{Mathlib/Init/Function}{Function.Surjective} + \lean{Mathlib/Init/Function} + {Function.Surjective} - \lean{Mathlib/Init/Function}{Function.Bijective} + \lean{Mathlib/Init/Function} + {Function.Bijective} \section{\defined{Image}}% \hyperlabel{ref:image} @@ -217,9 +235,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and & = \{v \mid (\exists u \in A) uFv\}. \end{align*} - \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.image} + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.image} - \lean{Mathlib/Data/Rel}{Rel.image} + \lean{Mathlib/Data/Rel} + {Rel.image} \section{\defined{Inductive Set}}% \hyperlabel{ref:inductive-set} @@ -228,9 +248,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and and it is "closed under \nameref{ref:successor}", i.e. $$(\forall a \in A) a^+ \in A.$$ - \lean{Prelude}{Nat} + \lean{Prelude} + {Nat} - \lean{Mathlib/Init/Set}{Set.univ} + \lean{Mathlib/Init/Set} + {Set.univ} \begin{note} Induction is baked into Lean's type system. @@ -252,9 +274,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and $$(\exists A)\left[ \emptyset \in A \land (\forall a \in A) a^+ \in A\right].$$ - \lean{Prelude}{Nat} + \lean{Prelude} + {Nat} - \lean{Mathlib/Init/Set}{Set.univ} + \lean{Mathlib/Init/Set} + {Set.univ} \section{\defined{Inverse}}% \hyperlabel{ref:inverse} @@ -262,9 +286,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and The \textbf{inverse} of a set $F$ is the set $$F^{-1} = \{\tuple{u, v} \mid vFu\}.$$ - \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.inv} + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.inv} - \lean{Mathlib/Data/Rel}{Rel.inv} + \lean{Mathlib/Data/Rel} + {Rel.inv} \section{\defined{Irreflexive}}% \hyperlabel{ref:irreflexive} @@ -272,7 +298,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and A binary relation $R$ on set $A$ is \textbf{irreflexive} if there is no $x \in A$ for which $xRx$. - \lean*{Mathlib/Init/Algebra/Classes}{IsIrrefl} + \lean*{Mathlib/Init/Algebra/Classes} + {IsIrrefl} \section{\defined{Linear Ordering}} \hyperlabel{ref:linear-ordering} @@ -287,7 +314,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and \item $R$ is \nameref{ref:trichotomous}. \end{enumerate} - \lean{Mathlib/Init/Algebra/Classes}{IsStrictTotalOrder} + \lean{Mathlib/Init/Algebra/Classes} + {IsStrictTotalOrder} \begin{note} This definition does not agree with how Lean defines a linear order. @@ -320,7 +348,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and \textbf{Multiplication} ($\cdot$) is the \nameref{ref:binary-operation} on $\omega$ such that for any $m$ and $n$ in $\omega$, $$m \cdot n = M_m(n).$$ - \lean{Init/Prelude}{Mul.mul} + \lean{Init/Prelude} + {Mul.mul} \section{\defined{Natural Number}}% \hyperlabel{ref:natural-number} @@ -329,7 +358,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and The set of all natural numbers exists by virtue of \nameref{sub:theorem-4a}. This set is denoted as $\omega$. - \lean*{Prelude}{Nat} + \lean*{Prelude} + {Nat} \section{\defined{Ordered Pair}}% \hyperlabel{ref:ordered-pair} @@ -337,9 +367,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and For any sets $u$ and $v$, the \textbf{ordered pair} $\tuple{u, v}$ is the set $\{\{u\}, \{u, v\}\}$. - \code*{Bookshelf/Enderton/Set/OrderedPair}{OrderedPair} + \code*{Bookshelf/Enderton/Set/OrderedPair} + {OrderedPair} - \lean{Prelude}{Prod} + \lean{Prelude} + {Prod} \section{\defined{Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}}% \hyperlabel{ref:ordering-natural-numbers} @@ -356,7 +388,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and & \iff m < n \lor m = n. \end{align*} - \lean{Init/Prelude}{Nat.lt} + \lean{Init/Prelude} + {Nat.lt} \section{\defined{Pair Set}}% \hyperlabel{ref:pair-set} @@ -364,9 +397,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and For any sets $u$ and $v$, the \textbf{pair set $\{u, v\}$} is the set whose only members are $u$ and $v$. - \lean*{Mathlib/Init/Set}{Set.insert} + \lean*{Mathlib/Init/Set} + {Set.insert} - \lean{Mathlib/Init/Set}{Set.singleton} + \lean{Mathlib/Init/Set} + {Set.singleton} \section{\defined{Pairing Axiom}}% \hyperlabel{ref:pairing-axiom} @@ -375,9 +410,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and $$\forall u, \forall v, \exists B, \forall x, (x \in B \iff x = u \text{ or } x = v).$$ - \lean{Mathlib/Init/Set}{Set.insert} + \lean{Mathlib/Init/Set} + {Set.insert} - \lean{Mathlib/Init/Set}{Set.singleton} + \lean{Mathlib/Init/Set} + {Set.singleton} \section{\defined{Partition}}% \hyperlabel{ref:partition} @@ -389,7 +426,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and \item each element of $A$ is in some set in $\Pi$. \end{enumerate} - \lean{Mathlib/Data/Setoid/Partition}{Setoid.IsPartition} + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.Partition} + + \lean{Mathlib/Data/Setoid/Partition} + {Setoid.IsPartition} \section{\defined{Peano System}}% \hyperlabel{ref:peano-system} @@ -404,7 +445,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and itself. \end{enumerate} - \code{Common/Set/Peano}{Peano.System} + \code{Common/Set/Peano} + {Peano.System} \section{\defined{Power Set}}% \hyperlabel{ref:power-set} @@ -412,7 +454,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and For any set $a$, the \textbf{power set $\powerset{a}$} is the set whose members are exactly the subsets of $a$. - \lean*{Mathlib/Init/Set}{Set.powerset} + \lean*{Mathlib/Init/Set} + {Set.powerset} \section{\defined{Power Set Axiom}}% \hyperlabel{ref:power-set-axiom} @@ -420,7 +463,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and For any set $a$, there is a set whose members are exactly the subsets of $a$: $$\forall a, \exists B, \forall x, (x \in B \iff x \subseteq a).$$ - \lean{Mathlib/Init/Set}{Set.powerset} + \lean{Mathlib/Init/Set} + {Set.powerset} \section{\defined{Proper Subset}}% \hyperlabel{ref:proper-subset} @@ -429,7 +473,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and only if it is a subset of $B$ that is unequal to $B$. $$A \subset B \iff A \subseteq B \land A \neq B.$$ - \lean{Std/Classes/SetNotation}{HasSSubset} + \lean{Std/Classes/SetNotation} + {HasSSubset} \section{\defined{Quotient Set}}% \hyperlabel{ref:quotient-set} @@ -439,7 +484,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and are the equivalence classes. The expression $A / R$ is read "$A$ modulo $R$. - \lean*{Init/Core}{Quotient} + \lean*{Init/Core} + {Quotient} \section{\defined{Range}}% \hyperlabel{ref:range} @@ -447,9 +493,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and The \textbf{range} of set $R$, denoted $\ran{R}$, is given by $$x \in \ran{R} \iff \exists t \tuple{t, x} \in R.$$ - \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.ran} + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.ran} - \lean{Mathlib/Data/Rel}{Rel.codom} + \lean{Mathlib/Data/Rel} + {Rel.codom} \section{\defined{Reflexive}}% \hyperlabel{ref:reflexive} @@ -457,16 +505,19 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and A binary relation $R$ is \textbf{reflexive} on $A$ if and only if $xRx$ for all $x \in A$. - \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isReflexive} + \code*{Bookshelf/Enderton/Set/Relation} + {Set.Relation.isReflexive} - \lean{Mathlib/Init/Algebra/Classes}{IsRefl} + \lean{Mathlib/Init/Algebra/Classes} + {IsRefl} \section{\defined{Relation}}% \hyperlabel{ref:relation} A \textbf{relation} is a set of \nameref{ref:ordered-pair}s. - \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation} + \code*{Bookshelf/Enderton/Set/Relation} + {Set.Relation} \lean{Mathlib/Data/Rel}{Rel} @@ -476,14 +527,16 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and The \textbf{restriction} of a set $F$ to set $A$ is the set $$F \restriction A = \{\tuple{u, v} \mid uFv \land u \in A\}.$$ - \code{Bookshelf/Enderton/Set/Relation}{Set.Relation.restriction} + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.restriction} \section{\defined{Successor}}% \hyperlabel{ref:successor} For any set $a$, its \textbf{successor} is defined by $$a^+ = a \cup \{a\}.$$ - \lean{Prelude}{Nat.succ} + \lean{Prelude} + {Nat.succ} \begin{note} The corresponding Lean definition refers to the `Nat.succ` constructor. @@ -498,7 +551,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and $$\forall t_1, \cdots \forall t_k, \forall c, \exists B, \forall x, (x \in B \iff x \in c \land \phi).$$ - \lean{Mathlib/Init/Set}{Set.Subset} + \lean{Mathlib/Init/Set} + {Set.Subset} \section{\defined{Symmetric}}% \hyperlabel{ref:symmetric} @@ -506,7 +560,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and A binary relation $R$ is \textbf{symmetric} if and only if whenever $xRy$ then $yRx$. - \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isSymmetric} + \code*{Bookshelf/Enderton/Set/Relation} + {Set.Relation.isSymmetric} \section{\defined{Symmetric Difference}}% \hyperlabel{ref:symmetric-difference} @@ -514,7 +569,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and The \textbf{symmetric difference} $A + B$ of sets $A$ and $B$ is the set $(A - B) \cup (B - A)$. - \lean*{Mathlib/Data/Set/Basic}{symmDiff\_def} + \lean*{Mathlib/Data/Set/Basic} + {symmDiff\_def} \section{\defined{Transitive}}% \hyperlabel{ref:transitive} @@ -522,9 +578,11 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and A binary relation $R$ is \textbf{transitive} if and only if whenever $xRy$ and $yRz$, then $xRz$. - \code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isTransitive} + \code*{Bookshelf/Enderton/Set/Relation} + {Set.Relation.isTransitive} - \lean{Mathlib/Init/Algebra/Classes}{IsTrans} + \lean{Mathlib/Init/Algebra/Classes} + {IsTrans} \section{\defined{Transitive Set}}% \hyperlabel{ref:transitive-set} @@ -541,7 +599,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and $$xRy, \quad x = y, \quad yRx$$ holds. - \lean*{Mathlib/Init/Algebra/Classes}{IsTrichotomous} + \lean*{Mathlib/Init/Algebra/Classes} + {IsTrichotomous} \section{\defined{Union Axiom}}% \hyperlabel{ref:union-axiom} @@ -551,7 +610,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and $$\forall A, \exists B, \forall x \left[ x \in B \iff (\exists b \in A) x \in b \right]$$ - \lean{Mathlib/Data/Set/Lattice}{Set.sUnion} + \lean{Mathlib/Data/Set/Lattice} + {Set.sUnion} \section{\defined{Union Axiom, Preliminary Form}}% \hyperlabel{ref:union-axiom-preliminary-form} @@ -561,7 +621,8 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and $$\forall a, \forall b, \exists B, \forall x, (x \in B \iff x \in a \text{ or } x \in b).$$ - \lean{Mathlib/Init/Set}{Set.union} + \lean{Mathlib/Init/Set} + {Set.union} \endgroup diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index f6a116e..36732be 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -1941,7 +1941,7 @@ Show that `Rₚ` is an equivalence relation on `A`. (This is a formalized versio of the discussion at the beginning of this section.) -/ theorem exercise_3_37 {P : Set (Set α)} {A : Set α} - (hP : isPartition P A) (Rₚ : Set.Relation α) + (hP : Partition P A) (Rₚ : Set.Relation α) (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B) : isEquivalence Rₚ A := by have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by @@ -2014,7 +2014,7 @@ equivalence relation on `A`. Show that if we start with the equivalence relation `Rₚ` of the preceding exercise, then the partition `A / Rₚ` is just `P`. -/ theorem exercise_3_38 {P : Set (Set α)} {A : Set α} - (hP : isPartition P A) (Rₚ : Set.Relation α) + (hP : Partition P A) (Rₚ : Set.Relation α) (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B) : modEquiv (exercise_3_37 hP Rₚ hRₚ) = P := by have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by diff --git a/Bookshelf/Enderton/Set/Relation.lean b/Bookshelf/Enderton/Set/Relation.lean index 7c989e6..e4eee6e 100644 --- a/Bookshelf/Enderton/Set/Relation.lean +++ b/Bookshelf/Enderton/Set/Relation.lean @@ -575,7 +575,7 @@ theorem neighborhood_mem_imp_relate {R : Set.Relation α} {A : Set α} A **partition** `Π` of a set `A` is a set of nonempty subsets of `A` that is disjoint and exhaustive. -/ -structure isPartition (P : Set (Set α)) (A : Set α) : Prop where +structure Partition (P : Set (Set α)) (A : Set α) : Prop where p_subset : ∀ p ∈ P, p ⊆ A nonempty : ∀ p ∈ P, Set.Nonempty p disjoint : ∀ a ∈ P, ∀ b, b ∈ P → a ≠ b → a ∩ b = ∅ @@ -585,7 +585,7 @@ structure isPartition (P : Set (Set α)) (A : Set α) : Prop where Membership of sets within `P` is unique. -/ theorem partition_mem_mem_eq {P : Set (Set α)} {A : Set α} - (hP : isPartition P A) (hx : x ∈ A) + (hP : Partition P A) (hx : x ∈ A) : ∃! B, B ∈ P ∧ x ∈ B := by have ⟨B, hB⟩ := hP.exhaustive x hx refine ⟨B, hB, ?_⟩ @@ -606,7 +606,7 @@ def modEquiv {A : Set α} {R : Relation α} (_ : isEquivalence R A) := Show the sets formed by `modEquiv` do indeed form a `partition`. -/ theorem modEquiv_partition {A : Set α} {R : Relation α} (hR : isEquivalence R A) - : isPartition (modEquiv hR) A := by + : Partition (modEquiv hR) A := by refine ⟨?_, ?_, ?_, ?_⟩ · intro p hp have ⟨x, hx⟩ := hp diff --git a/Common/Nat/Basic.lean b/Common/Nat/Basic.lean index 9af48ad..393c68b 100644 --- a/Common/Nat/Basic.lean +++ b/Common/Nat/Basic.lean @@ -1,7 +1,14 @@ import Mathlib.Data.Set.Basic +import Mathlib.Tactic.NormNum namespace Nat +/-- +If `n < m⁺`, then `n < m` or `n = m`. +-/ +theorem lt_or_eq_of_lt {n m : Nat} (h : n < m.succ) : n < m ∨ n = m := + lt_or_eq_of_le (lt_succ.mp h) + /-- The following cancellation law holds for `m`, `n`, and `p` in `ω`: ``` diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index 8186d56..c042e40 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -44,6 +44,7 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
  • Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.
    • +

    Legend

    A color/symbol code is used on generated PDF headers to indicate their status: