From 83699dd58ef38001a4a5aec05be58493d185071c Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 9 Aug 2023 15:44:40 -0600 Subject: [PATCH] Enderton. Continue actually verifying set theorems. --- Bookshelf/Enderton/Set.tex | 125 ++++++---- Bookshelf/Enderton/Set/Chapter_2.lean | 87 ++++++- Bookshelf/Enderton/Set/Chapter_3.lean | 2 +- Bookshelf/Enderton/Set/Chapter_4.lean | 322 +++++++++++++++++++++++--- Common/Set/Basic.lean | 40 ++++ 5 files changed, 494 insertions(+), 82 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index eb286a6..83d0a12 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -1456,7 +1456,7 @@ Let $A$ and $B$ be sets. $x \not\in A + B$ if and only if either $x \in A \cap B$ or $x \not\in A \cup B$. - \code*{Bookshelf/Enderton/Set/Basic} + \code*{Common/Set/Basic} {Set.not\_mem\_symm\_diff\_inter\_or\_not\_union} \begin{proof} @@ -1948,7 +1948,7 @@ \end{align*} \end{proof} -\subsection{\pending{Exercise 2.15a}}% +\subsection{\verified{Exercise 2.15a}}% \hyperlabel{sub:exercise-2.15a} Show that $A \cap (B + C) = (A \cap B) + (A \cap C)$. @@ -1956,6 +1956,9 @@ \lean*{Mathlib/Data/Set/Basic} {Set.inter\_symmDiff\_distrib\_left} + \code{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_2\_15a} + \begin{proof} By definition of the intersection, \nameref{ref:symmetric-difference}, and relative complement of sets, @@ -1984,13 +1987,15 @@ \end{align*} \end{proof} -\subsection{\pending{Exercise 2.15b}}% +\subsection{\verified{Exercise 2.15b}}% \hyperlabel{sub:exercise-2.15b} Show that $A + (B + C) = (A + B) + C$. - \lean*{Mathlib/Data/Set/Basic} - {Set.symmDiff\_assoc} + \lean*{Mathlib/Order/SymmDiff}{symmDiff\_assoc} + + \code{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_2\_15b} \begin{proof} Let $A$, $B$, and $C$ be sets. @@ -2658,11 +2663,6 @@ pairs $\pair{x, y}$ with $x \in A$ and $y \in B$. \end{theorem} - \begin{note} - The below Lean proof is a definition (i.e. an axiom). - It does not prove such a set's existence from first principles. - \end{note} - \lean{Mathlib/SetTheory/ZFC/Basic}{Set.prod} \begin{proof} @@ -2830,7 +2830,7 @@ \hyperlabel{sub:lemma-1} \hyperlabel{sub:one-to-one-inverse} - \begin{lemma} + \begin{lemma}[1] For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \end{lemma} @@ -3985,7 +3985,7 @@ showing it can be represented as an ordered $1$-tuple as well. \end{answer} -\subsection{\pending{Exercise 3.11}}% +\subsection{\unverified{Exercise 3.11}}% \hyperlabel{sub:exercise-3.11} Prove the following version (for functions) of the extensionality principle: @@ -6083,7 +6083,7 @@ \section{Arithmetic}% \hyperlabel{sec:arithmetic} -\subsection{\pending{Theorem 4I}} +\subsection{\verified{Theorem 4I}} \hyperlabel{sub:theorem-4i} \begin{theorem}[4I] @@ -6098,6 +6098,9 @@ \lean{Init/Prelude}{Nat.add} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4i} + \begin{proof} \paragraph{\eqref{sub:theorem-4i-eq1}}% @@ -6115,7 +6118,7 @@ \end{proof} -\subsection{\pending{Theorem 4J}} +\subsection{\verified{Theorem 4J}} \hyperlabel{sub:theorem-4j} \begin{theorem}[4J] @@ -6130,6 +6133,9 @@ \lean{Init/Prelude}{Nat.mul} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4j} + \begin{proof} \paragraph{\eqref{sub:theorem-4j-eq1}}% @@ -6145,7 +6151,7 @@ \end{proof} -\subsection{\pending{Left Additive Identity}}% +\subsection{\verified{Left Additive Identity}}% \hyperlabel{sub:left-additive-identity} \begin{lemma} @@ -6155,6 +6161,9 @@ \lean{Init/Data/Nat/Basic}{Nat.zero\_add} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.left\_additive\_identity} + \begin{proof} Let $S = \{n \in \omega \mid 0 + n = n\}$. @@ -6185,17 +6194,20 @@ \end{proof} -\subsection{\pending{Lemma 3}}% -\hyperlabel{sub:lemma-3} +\subsection{\verified{Lemma 2}}% +\hyperlabel{sub:lemma-2} \hyperlabel{sub:succ-add-eq-add-succ} - \begin{lemma} + \begin{lemma}[2] For all $m, n \in \omega$, $A_{m^+}(n) = A_m(n^+)$. In other words, $$m^+ + n = m + n^+.$$ \end{lemma} \lean{Std/Data/Nat/Lemmas}{Nat.succ\_add\_eq\_succ\_add} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.lemma\_2} + \begin{proof} Let $m \in \omega$ and define @@ -6204,14 +6216,14 @@ Afterwards we show that (iii) our theorem holds. \paragraph{(i)}% - \hyperlabel{par:lemma-3-i} + \hyperlabel{par:lemma-2-i} By \nameref{sub:theorem-4i}, $m^+ + 0 = m^+$. Likewise, $m + 0^+ = (m + 0)^+ = m^+$. Thus $0 \in S$. \paragraph{(ii)}% - \hyperlabel{par:lemma-3-ii} + \hyperlabel{par:lemma-2-ii} Suppose $n \in S$. By \nameref{sub:theorem-4i}, $m^+ + n^+ = (m^+ + n)^+$. @@ -6221,13 +6233,13 @@ \paragraph{(iii)}% - By \nameref{par:lemma-3-i} and \nameref{par:lemma-3-ii}, $S$ is inductive. + By \nameref{par:lemma-2-i} and \nameref{par:lemma-2-ii}, $S$ is inductive. Hence \nameref{sub:theorem-4b} implies $S = \omega$. Thus for all $n \in \omega$, $m^+ + n = m + n^+$. \end{proof} -\subsection{\pending{Theorem 4K-1}}% +\subsection{\verified{Theorem 4K-1}}% \hyperlabel{sub:theorem-4k-1} \begin{theorem}[4K-1] @@ -6235,7 +6247,10 @@ For $m, n, p \in \omega$, $$m + (n + p) = (m + n) + p.$$ \end{theorem} - \lean{Mathlib/Algebra/Group/Defs}{add\_assoc} + \lean{Init/Data/Nat/Basic}{Nat.add\_assoc} + + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4k\_1} \begin{proof} @@ -6281,7 +6296,7 @@ \end{proof} -\subsection{\pending{Theorem 4K-2}}% +\subsection{\verified{Theorem 4K-2}}% \hyperlabel{sub:theorem-4k-2} \begin{theorem}[4K-2] @@ -6289,7 +6304,10 @@ For $m, n \in \omega$, $$m + n = n + m.$$ \end{theorem} - \lean{Mathlib/Algebra/Group/Defs}{add\_comm} + \lean{Init/Data/Nat/Basic}{Nat.add\_comm} + + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4k\_2} \begin{proof} @@ -6331,7 +6349,7 @@ \end{proof} -\subsection{\pending{Zero Multiplicand}}% +\subsection{\verified{Zero Multiplicand}}% \hyperlabel{sub:zero-multiplicand} \begin{lemma} @@ -6341,6 +6359,9 @@ \lean{Init/Data/Nat/Basic}{Nat.zero\_mul} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.zero\_multiplicand} + \begin{proof} Define @@ -6365,8 +6386,8 @@ \begin{align*} 0 \cdot n^+ & = 0 \cdot n + 0 & \textref{sub:theorem-4j} \\ - & = 0 + 0 & \eqref{sub:zero-multiplicand-eq1} \\ - & = 0. & \textref{ref:addition} + & = 0 \cdot n & \textref{sub:theorem-4i} \\ + & = 0. & \eqref{sub:zero-multiplicand-eq1} \end{align*} Thus $n^+ \in S$. @@ -6380,7 +6401,7 @@ \end{proof} -\subsection{\pending{Successor Distribution}}% +\subsection{\verified{Successor Distribution}}% \hyperlabel{sub:successor-distribution} \begin{lemma} @@ -6390,6 +6411,9 @@ \lean{Init/Data/Nat/Basic}{Nat.succ\_mul} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.succ\_distrib} + \begin{proof} Let $m \in \omega$ and define @@ -6434,7 +6458,7 @@ \end{proof} -\subsection{\pending{Theorem 4K-3}} +\subsection{\verified{Theorem 4K-3}} \hyperlabel{sub:theorem-4k-3} \begin{theorem}[4K-3] @@ -6444,6 +6468,9 @@ \lean{Init/Data/Nat/Basic}{Nat.left\_distrib} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4k\_3} + \begin{proof} Fix $n, p \in \omega$ and define @@ -6494,7 +6521,7 @@ \end{proof} -\subsection{\pending{Successor Identity}}% +\subsection{\verified{Successor Identity}}% \hyperlabel{sub:successor-identity} \begin{lemma} @@ -6504,6 +6531,9 @@ \lean{Std/Data/Nat/Lemmas}{Nat.succ\_eq\_one\_add} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.succ\_identity} + \begin{proof} Let @@ -6545,7 +6575,7 @@ \end{proof} -\subsection{\pending{Right Multiplicative Identity}}% +\subsection{\verified{Right Multiplicative Identity}}% \hyperlabel{sub:right-multiplicative-identity} \begin{lemma} @@ -6553,7 +6583,10 @@ In other words, $$m \cdot 1 = m.$$ \end{lemma} - \lean{Init/Data/Nat/Basic}{mul\_one} + \lean{Init/Data/Nat/Basic}{Nat.mul\_one} + + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.right\_mul\_id} \begin{proof} @@ -6594,7 +6627,7 @@ \end{proof} -\subsection{\pending{Theorem 4K-5}} +\subsection{\verified{Theorem 4K-5}} \hyperlabel{sub:theorem-4k-5} \begin{theorem}[4K-5] @@ -6607,7 +6640,10 @@ two properties in the opposite direction. \end{note} - \lean{Mathlib/Algebra/Group/Defs}{mul\_comm} + \lean{Init/Data/Nat/Basic}{Nat.mul\_comm} + + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4k\_5} \begin{proof} @@ -6652,7 +6688,7 @@ \end{proof} -\subsection{\pending{Theorem 4K-4}}% +\subsection{\verified{Theorem 4K-4}}% \hyperlabel{sub:theorem-4k-4} \begin{theorem}[4K-4] @@ -6660,7 +6696,10 @@ For $m, n, p \in \omega$, $$m \cdot (n \cdot p) = (m \cdot n) \cdot p.$$ \end{theorem} - \lean{Mathlib/Algebra/Group/Defs}{mul\_assoc} + \lean{Init/Data/Nat/Basic}{Nat.mul\_assoc} + + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4k\_4} \begin{proof} @@ -6708,7 +6747,7 @@ \section{Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}% \hyperlabel{sec:ordering-natural-numbers} -\subsection{\pending{Ordering on Successor}}% +\subsection{\unverified{Ordering on Successor}}% \hyperlabel{sub:ordering-successor} \begin{lemma} @@ -6746,7 +6785,7 @@ Thus $m \in n \iff m \in \omega \land m \in n$. \end{proof} -\subsection{\pending{Lemma 4L(a)}}% +\subsection{\unverified{Lemma 4L(a)}}% \hyperlabel{sub:lemma-4l-a} \begin{lemma}[4L(a)] @@ -6804,8 +6843,7 @@ Suppose $m^+ \in n^+$. The definition of \nameref{ref:successor} immediately implies that $m \in m^+$. - By \nameref{sec:ordering-natural-numbers}, $m^+ \in n^+$ implies - $m^+ \in n$ or $m^+ = n$. + Likewise, $m^+ \in n^+$ implies $m^+ \in n$ or $m^+ = n$. If the latter, $m \in n$ immediately follows. If the former, we note $n$ is a transitive set by \nameref{sub:theorem-4f}. @@ -6813,7 +6851,7 @@ \end{proof} -\subsection{\pending{Lemma 4L(b)}}% +\subsection{\verified{Lemma 4L(b)}}% \hyperlabel{sub:lemma-4l-b} \begin{lemma}[4L(b)] @@ -6822,6 +6860,9 @@ \lean{Init/Prelude}{Nat.lt\_irrefl} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4l\_b} + \begin{proof} Define diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean index 07e949e..945345a 100644 --- a/Bookshelf/Enderton/Set/Chapter_2.lean +++ b/Bookshelf/Enderton/Set/Chapter_2.lean @@ -1,6 +1,7 @@ import Bookshelf.Enderton.Set.Chapter_1 import Common.Set.Basic import Mathlib.Data.Set.Lattice +import Mathlib.Order.SymmDiff /-! # Enderton.Set.Chapter_2 @@ -261,7 +262,7 @@ theorem anti_monotonicity_ii (A B : Set (Set α)) (h : A ⊆ B) #check Set.sInter_subset_sInter -/-- #### ∩/- Associativity +/-- #### Intersection/Difference Associativity Let `A`, `B`, and `C` be sets. Then `A ∩ (B - C) = (A ∩ B) - C`. -/ @@ -271,7 +272,8 @@ theorem inter_diff_assoc (A B C : Set α) _ = { x | x ∈ A ∧ (x ∈ B ∧ x ∉ C) } := rfl _ = { x | (x ∈ A ∧ x ∈ B) ∧ x ∉ C } := by ext _ - sorry + simp only [Set.mem_setOf_eq] + rw [and_assoc] _ = { x | x ∈ A ∩ B ∧ x ∉ C } := rfl _ = (A ∩ B) \ C := rfl @@ -667,6 +669,87 @@ theorem exercise_2_14 : A \ (B \ C) ≠ (A \ B) \ C := by end +/-- #### Exercise 2.15 (a) + +Show that `A ∩ (B + C) = (A ∩ B) + (A ∩ C)`. +-/ +theorem exercise_2_15a (A B C : Set α) + : A ∩ (B ∆ C) = (A ∩ B) ∆ (A ∩ C) := Eq.symm $ + calc (A ∩ B) ∆ (A ∩ C) + _ = ((A ∩ B) \ (A ∩ C)) ∪ ((A ∩ C) \ (A ∩ B)) := rfl + _ = ((A ∩ B) \ A) ∪ + ((A ∩ B) \ C) ∪ + (((A ∩ C) \ A) ∪ + ((A ∩ C) \ B)) := by + iterate 2 rw [Set.diff_inter] + _ = (A ∩ (B \ A)) ∪ + (A ∩ (B \ C)) ∪ + ((A ∩ (C \ A)) ∪ + (A ∩ (C \ B))) := by + iterate 4 rw [Set.inter_diff_assoc] + _ = ∅ ∪ (A ∩ (B \ C)) ∪ (∅ ∪ (A ∩ (C \ B))) := by + iterate 2 rw [Set.inter_diff_self] + _ = (A ∩ (B \ C)) ∪ (A ∩ (C \ B)) := by + simp only [Set.empty_union] + _ = A ∩ ((B \ C) ∪ (C \ B)) := by + rw [Set.inter_distrib_left] + _ = A ∩ (B ∆ C) := rfl + +#check Set.inter_symmDiff_distrib_left + +/-- #### Exercise 2.15 (b) + +Show that `A + (B + C) = (A + B) + C`. +-/ +theorem exercise_2_15b (A B C : Set α) + : A ∆ (B ∆ C) = (A ∆ B) ∆ C := by + rw [Set.Subset.antisymm_iff] + apply And.intro + · show ∀ x, x ∈ A ∆ (B ∆ C) → x ∈ (A ∆ B) ∆ C + intro x hx + apply Or.elim hx + · intro ⟨hA, nBC⟩ + rw [Set.not_mem_symm_diff_inter_or_not_union] at nBC + apply Or.elim nBC + · intro h + have : x ∉ A ∆ B := Set.symm_diff_mem_both_not_mem hA h.left + exact Set.symm_diff_mem_right this h.right + · intro h + have ⟨nB, nC⟩ : x ∉ B ∧ x ∉ C := not_or_de_morgan.mp h + have : x ∈ A ∆ B := Set.symm_diff_mem_left hA nB + exact Set.symm_diff_mem_left this nC + · intro ⟨hx₁, hx₂⟩ + apply Or.elim hx₁ + · intro ⟨hB, nC⟩ + have : x ∈ A ∆ B := Set.symm_diff_mem_right hx₂ hB + exact Set.symm_diff_mem_left this nC + · intro ⟨hC, nB⟩ + have : x ∉ A ∆ B := Set.symm_diff_not_mem_both_not_mem hx₂ nB + exact Set.symm_diff_mem_right this hC + · show ∀ x, x ∈ (A ∆ B) ∆ C → x ∈ A ∆ (B ∆ C) + intro x hx + apply Or.elim hx + · intro ⟨hAB, nC⟩ + apply Or.elim hAB + · intro ⟨hA, nB⟩ + have : x ∉ B ∆ C := Set.symm_diff_not_mem_both_not_mem nB nC + exact Set.symm_diff_mem_left hA this + · intro ⟨hB, nA⟩ + have : x ∈ B ∆ C := Set.symm_diff_mem_left hB nC + exact Set.symm_diff_mem_right nA this + · intro ⟨hC, nAB⟩ + rw [Set.not_mem_symm_diff_inter_or_not_union] at nAB + apply Or.elim nAB + · intro ⟨hA, hB⟩ + have : x ∉ B ∆ C := Set.symm_diff_mem_both_not_mem hB hC + exact Set.symm_diff_mem_left hA this + · intro h + have ⟨nA, nB⟩ : x ∉ A ∧ x ∉ B := not_or_de_morgan.mp h + have : x ∈ B ∆ C := Set.symm_diff_mem_right nB hC + exact Set.symm_diff_mem_right nA this + +#check symmDiff_assoc + /-- #### Exercise 2.16 Simplify: diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index bcb908f..f6a116e 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -19,7 +19,7 @@ namespace Enderton.Set.Chapter_3 If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`. -/ -theorem lemma_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C) +lemma lemma_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C) : OrderedPair x y ∈ 𝒫 𝒫 C := by have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy diff --git a/Bookshelf/Enderton/Set/Chapter_4.lean b/Bookshelf/Enderton/Set/Chapter_4.lean index b6a6351..8659b7d 100644 --- a/Bookshelf/Enderton/Set/Chapter_4.lean +++ b/Bookshelf/Enderton/Set/Chapter_4.lean @@ -18,6 +18,291 @@ theorem theorem_4c (n : ℕ) | 0 => simp | m + 1 => simp +#check Nat.exists_eq_succ_of_ne_zero + +/-- #### Theorem 4I + +For natural numbers `m` and `n`, +``` +m + 0 = m, +m + n⁺ = (m + n)⁺ +``` +-/ +theorem theorem_4i (m n : ℕ) + : m + 0 = m ∧ m + n.succ = (m + n).succ := ⟨rfl, rfl⟩ + +/-- #### Theorem 4J + +For natural numbers `m` and `n`, +``` +m ⬝ 0 = 0, +m ⬝ n⁺ = m ⬝ n + m . +``` +-/ +theorem theorem_4j (m n : ℕ) + : m * 0 = 0 ∧ m * n.succ = m * n + m := ⟨rfl, rfl⟩ + +/-- #### Left Additive Identity + +For all `n ∈ ω`, `A₀(n) = n`. In other words, `0 + n = n`. +-/ +lemma left_additive_identity (n : ℕ) + : 0 + n = n := by + induction n with + | zero => simp + | succ n ih => + calc 0 + n.succ + _ = (0 + n).succ := rfl + _ = n.succ := by rw [ih] + +#check Nat.zero_add + +/-- #### Lemma 2 + +For all `m, n ∈ ω`, `Aₘ₊(n) = Aₘ(n⁺)`. In other words, `m⁺ + n = m + n⁺`. +-/ +lemma lemma_2 (m n : ℕ) + : m.succ + n = m + n.succ := by + induction n with + | zero => rfl + | succ n ih => + calc m.succ + n.succ + _ = (m.succ + n).succ := rfl + _ = (m + n.succ).succ := by rw [ih] + _ = m + n.succ.succ := rfl + +#check Nat.succ_add_eq_succ_add + +/-- #### Theorem 4K-1 + +Associatve law for addition. For `m, n, p ∈ ω`, +``` +m + (n + p) = (m + n) + p. +``` +-/ +theorem theorem_4k_1 (m n p : ℕ) + : m + (n + p) = (m + n) + p := by + induction m with + | zero => simp + | succ m ih => + calc m.succ + (n + p) + _ = m + (n + p).succ := by rw [lemma_2] + _ = (m + (n + p)).succ := rfl + _ = ((m + n) + p).succ := by rw [ih] + _ = (m + n) + p.succ := rfl + _ = (m + n).succ + p := by rw [lemma_2] + _ = (m + n.succ) + p := rfl + _ = (m.succ + n) + p := by rw [lemma_2] + +#check Nat.add_assoc + +/-- #### Theorem 4K-2 + +Commutative law for addition. For `m, n ∈ ω`, +``` +m + n = n + m. +``` +-/ +theorem theorem_4k_2 {m n : ℕ} + : m + n = n + m := by + induction m with + | zero => simp + | succ m ih => + calc m.succ + n + _ = m + n.succ := by rw [lemma_2] + _ = (m + n).succ := rfl + _ = (n + m).succ := by rw [ih] + _ = n + m.succ := by rfl + +#check Nat.add_comm + +/-- #### Zero Multiplicand + +For all `n ∈ ω`, `M₀(n) = 0`. In other words, `0 ⬝ n = 0`. +-/ +theorem zero_multiplicand (n : ℕ) + : 0 * n = 0 := by + induction n with + | zero => simp + | succ n ih => + calc 0 * n.succ + _ = 0 * n + 0 := rfl + _ = 0 * n := rfl + _ = 0 := by rw [ih] + +#check Nat.zero_mul + +/-- #### Successor Distribution + +For all `m, n ∈ ω`, `Mₘ₊(n) = Mₘ(n) + n`. In other words, +``` +m⁺ ⬝ n = m ⬝ n + n. +``` +-/ +theorem succ_distrib (m n : ℕ) + : m.succ * n = m * n + n := by + induction n with + | zero => simp + | succ n ih => + calc m.succ * n.succ + _ = m.succ * n + m.succ := rfl + _ = (m * n + n) + m.succ := by rw [ih] + _ = m * n + (n + m.succ) := by rw [theorem_4k_1] + _ = m * n + (n.succ + m) := by rw [lemma_2] + _ = m * n + (m + n.succ) := by + conv => left; arg 2; rw [theorem_4k_2] + _ = (m * n + m) + n.succ := by rw [theorem_4k_1] + _ = m * n.succ + n.succ := rfl + +#check Nat.succ_mul + +/-- #### Theorem 4K-3 + +Distributive law. For `m, n, p ∈ ω`, +``` +m ⬝ (n + p) = m ⬝ n + m ⬝ p. +``` +-/ +theorem theorem_4k_3 (m n p : ℕ) + : m * (n + p) = m * n + m * p := by + induction m with + | zero => simp + | succ m ih => + calc m.succ * (n + p) + _ = m * (n + p) + (n + p) := by rw [succ_distrib] + _ = m * (n + p) + n + p := by rw [← theorem_4k_1] + _ = m * n + m * p + n + p := by rw [ih] + _ = m * n + (m * p + n) + p := by rw [theorem_4k_1] + _ = m * n + (n + m * p) + p := by + conv => left; arg 1; arg 2; rw [theorem_4k_2] + _ = (m * n + n) + (m * p + p) := by rw [theorem_4k_1, theorem_4k_1] + _ = m.succ * n + m.succ * p := by rw [succ_distrib, succ_distrib] + +/-- #### Successor Identity + +For all `m ∈ ω`, `Aₘ(1) = m⁺`. In other words, `m + 1 = m⁺`. +-/ +theorem succ_identity (m : ℕ) + : m + 1 = m.succ := by + induction m with + | zero => simp + | succ m ih => + calc m.succ + 1 + _ = m + (Nat.succ Nat.zero).succ := by rw [lemma_2] + _ = (m + 1).succ := rfl + _ = m.succ.succ := by rw [ih] + +#check Nat.succ_eq_one_add + +/-- #### Right Multiplicative Identity + +For all `m ∈ ω`, `Mₘ(1) = m`. In other words, `m ⬝ 1 = m`. +-/ +theorem right_mul_id (m : ℕ) + : m * 1 = m := by + induction m with + | zero => simp + | succ m ih => + calc m.succ * 1 + _ = m * 1 + 1 := by rw [succ_distrib] + _ = m + 1 := by rw [ih] + _ = m.succ := by rw [succ_identity] + +#check Nat.mul_one + +/-- #### Theorem 4K-5 + +Commutative law for multiplication. For `m, n ∈ ω`, `m ⬝ n = n ⬝ m`. +-/ +theorem theorem_4k_5 (m n : ℕ) + : m * n = n * m := by + induction m with + | zero => simp + | succ m ih => + calc m.succ * n + _ = m * n + n := by rw [succ_distrib] + _ = n * m + n := by rw [ih] + _ = n * m + n * 1 := by + conv => left; arg 2; rw [← right_mul_id n] + _ = n * (m + 1) := by rw [← theorem_4k_3] + _ = n * m.succ := by rw [succ_identity] + +#check Nat.mul_comm + +/-- #### Theorem 4K-4 + +Associative law for multiplication. For `m, n, p ∈ ω`, +``` +m ⬝ (n ⬝ p) = (m ⬝ n) ⬝ p. +``` +-/ +theorem theorem_4k_4 (m n p : ℕ) + : m * (n * p) = (m * n) * p := by + induction p with + | zero => simp + | succ p ih => + calc m * (n * p.succ) + _ = m * (n * p + n) := rfl + _ = m * (n * p) + m * n := by rw [theorem_4k_3] + _ = (m * n) * p + m * n := by rw [ih] + _ = p * (m * n) + m * n := by rw [theorem_4k_5] + _ = p.succ * (m * n) := by rw [succ_distrib] + _ = (m * n) * p.succ := by rw [theorem_4k_5] + +#check Nat.mul_assoc + +/-- #### Lemma 4L(b) + +No natural number is a member of itself. +-/ +lemma lemma_4l_b (n : ℕ) + : ¬ n < n := by + induction n with + | zero => simp + | succ n ih => + by_contra nh + rw [Nat.succ_lt_succ_iff] at nh + exact absurd nh ih + +#check Nat.lt_irrefl + +/-- #### Lemma 10 + +For every natural number `n ≠ 0`, `0 ∈ n`. +-/ +theorem zero_least_nat (n : ℕ) + : 0 = n ∨ 0 < n := by + by_cases h : n = 0 + · left + rw [h] + · right + have ⟨m, hm⟩ := Nat.exists_eq_succ_of_ne_zero h + rw [hm] + exact Nat.succ_pos m + +/-- #### Trichotomy Law for ω + +For any natural numbers `m` and `n`, exactly one of the three conditions +``` +m ∈ n, m = n, n ∈ m +``` +holds. +-/ +theorem trichotomy_law_for_nat + : IsAsymm ℕ LT.lt ∧ IsTrichotomous ℕ LT.lt := + ⟨instIsAsymmLtToLT, instIsTrichotomousLtToLTToPreorderToPartialOrder⟩ + +/-- #### Linear Ordering on ω + +Relation +``` +∈_ω = {⟨m, n⟩ ∈ ω × ω | m ∈ n} +``` +is a linear ordering on `ω`. +-/ +theorem linear_ordering_on_nat + : IsStrictTotalOrder ℕ LT.lt := isStrictTotalOrder_of_linearOrder + /-- #### Exercise 4.1 Show that `1 ≠ 3` i.e., that `∅⁺ ≠ ∅⁺⁺⁺`. @@ -105,41 +390,4 @@ theorem exercise_4_14 (n : ℕ) have : even n := ⟨q, hq'⟩ exact absurd this h -/-- #### Lemma 10 - -For every natural number `n ≠ 0`, `0 ∈ n`. --/ -theorem zero_least_nat (n : ℕ) - : 0 = n ∨ 0 < n := by - by_cases h : n = 0 - · left - rw [h] - · right - have ⟨m, hm⟩ := Nat.exists_eq_succ_of_ne_zero h - rw [hm] - exact Nat.succ_pos m - -/-- #### Trichotomy Law for ω - -For any natural numbers `m` and `n`, exactly one of the three conditions -``` -m ∈ n, m = n, n ∈ m -``` -holds. --/ -theorem trichotomy_law_for_nat - : IsAsymm ℕ LT.lt ∧ IsTrichotomous ℕ LT.lt := - ⟨instIsAsymmLtToLT, instIsTrichotomousLtToLTToPreorderToPartialOrder⟩ - -/-- #### Linear Ordering on ω - -Relation -``` -∈_ω = {⟨m, n⟩ ∈ ω × ω | m ∈ n} -``` -is a linear ordering on `ω`. --/ -theorem linear_ordering_on_nat - : IsStrictTotalOrder ℕ LT.lt := isStrictTotalOrder_of_linearOrder - end Enderton.Set.Chapter_4 \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index 9a6c8e3..aec46e6 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -156,6 +156,46 @@ theorem prod_nonempty_nonempty_imp_nonempty_prod {A : Set α} {B : Set β} /-! ## Symmetric Difference -/ +/-- +If `x ∈ A` and `x ∉ B`, then `x ∈ A ∆ B`. +-/ +theorem symm_diff_mem_left {A B : Set α} (hA : x ∈ A) (hB : x ∉ B) + : x ∈ A ∆ B := by + left + exact ⟨hA, hB⟩ + +/-- +If `x ∉ A` and `x ∈ B`, then `x ∈ A ∆ B`. +-/ +theorem symm_diff_mem_right {A B : Set α} (hA : x ∉ A) (hB : x ∈ B) + : x ∈ A ∆ B := by + right + exact ⟨hB, hA⟩ + +/-- +If `x ∈ A` and `x ∈ B`, then `x ∉ A ∆ B`. +-/ +theorem symm_diff_mem_both_not_mem {A B : Set α} (hA : x ∈ A) (hB : x ∈ B) + : x ∉ A ∆ B := by + intro h + apply Or.elim h + · intro ⟨_, nB⟩ + exact absurd hB nB + · intro ⟨_, nA⟩ + exact absurd hA nA + +/-- +If `x ∉ A` and `x ∉ B`, then `x ∉ A ∆ B`. +-/ +theorem symm_diff_not_mem_both_not_mem {A B : Set α} (nA : x ∉ A) (nB : x ∉ B) + : x ∉ A ∆ B := by + intro h + apply Or.elim h + · intro ⟨hA, _⟩ + exact absurd hA nA + · intro ⟨hB, _⟩ + exact absurd hB nB + /-- `x` is a member of the `symmDiff` of `A` and `B` **iff** `x ∈ A ∧ x ∉ B` or `x ∉ A ∧ x ∈ B`.