diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index df7a282..bd31d82 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -6950,7 +6950,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \begin{proof} - \lean{Init/Prelude}{Nat.succ} + \lean{Std/Data/Nat/Lemmas}{Nat.succ\_eq\_one\_add} Let \begin{equation} @@ -7605,7 +7605,7 @@ Formulate an analogue to Exercise 9 for a function \end{proof} -\subsection{\sorry{Exercise 4.13}}% +\subsection{\verified{Exercise 4.13}}% \hyperlabel{sub:exercise-4.13} Let $m$ and $n$ be natural numbers such that $m \cdot n = 0$. @@ -7613,11 +7613,29 @@ Show that either $m = 0$ or $n = 0$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.exercise\_4\_13} + + Suppose $m \cdot n = 0$. + For the sake of contradiction, assume $m \neq 0$ and $n \neq 0$. + By \nameref{sub:theorem-4c}, there exists some $p, q \in \omega$ such that + $p^+ = m$ and $q^+ = n$. + Thus + \begin{align*} + m \cdot n + & = m \cdot q^+ \\ + & = m \cdot q + m & \textref{sub:theorem-4j} \\ + & = m \cdot q + p^+ \\ + & = (m \cdot q + p)^+. & \textref{sub:theorem-4i} + \end{align*} + By definition of a \nameref{ref:successor}, + $m \cdot n = (m \cdot q + p)^+ \neq \emptyset = 0$, a contradiction. + Therefore our original assumption was wrong. + Hence $m = 0$ or $n = 0$. \end{proof} -\subsection{\sorry{Exercise 4.14}}% +\subsection{\verified{Exercise 4.14}}% \hyperlabel{sub:exercise-4.14} Call a natural number \textit{even} if it has the form $2 \cdot m$ for some $m$. @@ -7626,7 +7644,98 @@ Show that each natural number is either even or odd, but never both. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.exercise\_4\_14} + + Let $$S = \{n \in \omega \mid n \text{ is even or odd but not both}\}.$$ + We show that (i) $0 \in S$ and (ii) if $n \in S$ then $n^+ \in S$ as well. + Afterward we prove (iii) that the theorem statement holds. + + \paragraph{(i)}% + \hyperlabel{par:exercise-4.14a-i} + + $0$ is even since $2 \cdot 0 = 0$ by \nameref{sub:theorem-4j}. + Furthermore, $0$ is not odd since that would imply there exists some + $p$ such that $(2 \cdot p)^+ = 0$. + By definition of \nameref{ref:successor}, this is not possible. + Thus $0 \in S$. + + \paragraph{(ii)}% + \hyperlabel{par:exercise-4.14a-ii} + + Suppose $n \in S$. + Then $n$ is even or odd but not both. + + \subparagraph{Case 1}% + + Suppose $n$ is even and not odd. + Then there exists some $m \in \omega$ such that $2 \cdot m = n$. + Since the successor operation is one-to-one, $(2 \cdot m)^+ = n^+$. + Thus $n^+$ is odd. + + For the sake of contradiction, suppose $n^+$ is even. + Then there exists some $p$ such that $2 \cdot p = n^+$. + We consider two additional cases: + + \vspace{8pt}\quad + \textbf{Case 1a}: Suppose $p = 0$. + Then, by \nameref{sub:theorem-4j}, $2 \cdot p = 0 = n^+$. + By definition of \nameref{ref:successor}, this is not possible. + + \vspace{8pt}\quad + \textbf{Case 1b}: Suppose $p \neq 0$. + Then \nameref{sub:theorem-4c} implies there exists some $q$ such that + $q^+ = p$. + Thus + \begin{align*} + n^+ + & = 2 \cdot p \\ + & = 2 \cdot q^+ \\ + & = q^+ + q^+ \\ + & = (q^+ + q)^+. & \textref{sub:theorem-4i} + \end{align*} + Since the successor operation is one-to-one, $n = q^+ + q$. + But then + \begin{align*} + n + & = q^+ + q \\ + & = q + q^+ & \textref{sub:theorem-4k-2} \\ + & = (q + q)^+ & \textref{sub:theorem-4i} \\ + & = (2 \cdot q)^+, + \end{align*} + indicating $n$ is odd. + This is a contradiction. + + \vspace{8pt}\quad + \textbf{Conclusion}: Since the above two cases are exhaustive, it follows + our original assumption is wrong. + That is, $n^+$ is odd but not even. + + \subparagraph{Case 2}% + + Suppose $n$ is odd and not even. + Then there exists some $p \in \omega$ such that $(2 \cdot p)^+ = n$. + Since the successor operation is one-to-one, + $(2 \cdot p)^{++} = (2 \cdot p^+) = n^+$. + Thus $n^+$ is even. + + For the sake of contradiction, suppose $n^+$ is odd. + Then there exists some $q$ such that $(2 \cdot q)^+ = n^+$. + Since the successor operation is one-to-one, it follows $2 \cdot q = n$. + But this implies $n$ is even, a contradiction. + Thus our original assumption is wrong. + That is, $n^+$ is even but not odd. + + \subparagraph{Conclusion}% + + Since the foregoing cases are exhaustive, it follows $n^+ \in S$. + + \paragraph{(iii)}% + + By \nameref{par:exercise-4.14a-i} and \nameref{par:exercise-4.14a-ii}, + $S$ is an \nameref{ref:inductive-set}. + By \nameref{sub:theorem-4b}, $S = \omega$. + Thus every natural number is either even or odd, but not both. \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_4.lean b/Bookshelf/Enderton/Set/Chapter_4.lean index 7da5f45..ffedbf6 100644 --- a/Bookshelf/Enderton/Set/Chapter_4.lean +++ b/Bookshelf/Enderton/Set/Chapter_4.lean @@ -1,3 +1,4 @@ +import Common.Logic.Basic import Mathlib.Data.Set.Basic /-! # Enderton.Set.Chapter_4 @@ -24,4 +25,84 @@ Show that `1 ≠ 3` i.e., that `∅⁺ ≠ ∅⁺⁺⁺`. theorem exercise_4_1 : 1 ≠ 3 := by simp +/-- #### Exercise 4.13 + +Let `m` and `n` be natural numbers such that `m ⬝ n = 0`. Show that either +`m = 0` or `n = 0`. +-/ +theorem exercise_4_13 (m n : ℕ) (h : m * n = 0) + : m = 0 ∨ n = 0 := by + by_contra nh + rw [not_or_de_morgan] at nh + have ⟨p, hp⟩ : ∃ p, m = p.succ := Nat.exists_eq_succ_of_ne_zero nh.left + have ⟨q, hq⟩ : ∃ q, n = q.succ := Nat.exists_eq_succ_of_ne_zero nh.right + have : m * n = (m * q + p).succ := calc m * n + _ = m * q.succ := by rw [hq] + _ = m * q + m := rfl + _ = m * q + p.succ := by rw [hp] + _ = (m * q + p).succ := rfl + rw [this] at h + simp only [Nat.succ_ne_zero] at h + +/-- +Call a natural number *even* if it has the form `2 ⬝ m` for some `m`. +-/ +def even (n : ℕ) : Prop := ∃ m, 2 * m = n + +/-- +Call a natural number *odd* if it has the form `(2 ⬝ p) + 1` for some `p`. +-/ +def odd (n : ℕ) : Prop := ∃ p, (2 * p) + 1 = n + +/-- #### Exercise 4.14 + +Show that each natural number is either even or odd, but never both. +-/ +theorem exercise_4_14 (n : ℕ) + : (even n ∧ ¬ odd n) ∨ (¬ even n ∧ odd n) := by + induction n with + | zero => + left + refine ⟨⟨0, by simp⟩, ?_⟩ + intro ⟨p, hp⟩ + simp only [Nat.zero_eq, Nat.succ_ne_zero] at hp + | succ n ih => + apply Or.elim ih + · -- Assumes `n` is even meaning `n⁺` is odd. + intro ⟨⟨m, hm⟩, h⟩ + right + refine ⟨?_, ⟨m, by rw [← hm]⟩⟩ + by_contra nh + have ⟨p, hp⟩ := nh + by_cases hp' : p = 0 + · rw [hp'] at hp + simp at hp + · have ⟨q, hq⟩ := Nat.exists_eq_succ_of_ne_zero hp' + rw [hq] at hp + have hq₁ : (q.succ + q).succ = n.succ := calc (q.succ + q).succ + _ = q.succ + q.succ := rfl + _ = 2 * q.succ := by rw [Nat.two_mul] + _ = n.succ := hp + injection hq₁ with hq₂ + have : odd n := by + refine ⟨q, ?_⟩ + calc 2 * q + 1 + _ = q + q + 1 := by rw [Nat.two_mul] + _ = q + q.succ := rfl + _ = q.succ + q := by rw [Nat.add_comm] + _ = n := hq₂ + exact absurd this h + · -- Assumes `n` is odd meaning `n⁺` is even. + intro ⟨h, ⟨p, hp⟩⟩ + have hp' : 2 * p.succ = n.succ := congrArg Nat.succ hp + left + refine ⟨⟨p.succ, by rw [← hp']⟩, ?_⟩ + by_contra nh + unfold odd at nh + have ⟨q, hq⟩ := nh + injection hq with hq' + simp only [Nat.add_eq, Nat.add_zero] at hq' + have : even n := ⟨q, hq'⟩ + exact absurd this h + end Enderton.Set.Chapter_4 \ No newline at end of file