These theorems tell us that the gcd of a and b is the same as the gcd of b and a % b, which suggests that the following recursive definition should compute the gcd of a and b:
def gcd (a b : Nat) : Nat :=
+def **gcd:: (a b : Nat) : Nat :=
match b with
| 0 => a
- | n + 1 => **gcd (n + 1) (a % (n + 1))::
-Unfortunately, Lean puts a red squiggle under gcd (n + 1) (a % (n + 1)), and it displays in the Infoview a long error message that begins fail to show termination. What is Lean complaining about?
+ | n + 1 => gcd (n + 1) (a % (n + 1))Unfortunately, Lean puts a red squiggle under gcd, and it displays in the Infoview a long error message that begins fail to show termination. What is Lean complaining about?
The problem is that recursive definitions are dangerous. To understand the danger, consider the following recursive definition:
def loop (n : Nat) : Nat := loop (n + 1)Suppose we try to use this definition to compute loop 3. The definition would lead us to perform the following calculation:
Lean’s error message suggests several ways to fix the problem with our recursive definition. We’ll use the first suggestion: Use `have` expressions to prove the remaining goals. Here, finally, is the definition of gcd that Lean is willing to accept:
def gcd (a b : Nat) : Nat :=
- match b with
- | 0 => a
- | n + 1 =>
- have : a % (n + 1) < n + 1 := mod_succ_lt a n
- gcd (n + 1) (a % (n + 1))
- termination_by bLean’s error message suggests several ways to fix the problem with our recursive definition. We’ll use the first suggestion: Use `have`-expressions to prove the remaining goals. Here, finally, is the definition of gcd that Lean is willing to accept. (You can ignore the initial line @[semireducible]. For technical reasons that we won’t go into, this line is needed to make this complicated recursive definition work in proofs the same way that our previous, simpler recursive definitions did.)
@[semireducible]
+def gcd (a b : Nat) : Nat :=
+ match b with
+ | 0 => a
+ | n + 1 =>
+ have : a % (n + 1) < n + 1 := mod_succ_lt a n
+ gcd (n + 1) (a % (n + 1))
+ termination_by bNotice that in the have expression, we have not bothered to specify an identifier for the assertion being proven, since we never need to refer to it. Let’s try out our gcd function:
++#eval:: gcd 672 161 --Answer: 7. Note 672 = 7 * 96 and 161 = 7 * 23.To establish the main properties of gcd a b we’ll need several lemmas. We prove some of them and leave others as exercises.
We will use these equations as the basis for recursive definitions of Lean functions gcd_c1 and gcd_c2 such that the required coefficients can be obtained from the formulas s = gcd_c1 a b and t = gcd_c2 a b. Notice that s and t could be negative, so they must have type Int, not Nat. As a result, in definitions and theorems involving gcd_c1 and gcd_c2 we will sometimes have to deal with coercion of natural numbers to integers.
The functions gcd_c1 and gcd_c2 will be mutually recursive; in other words, each will be defined not only in terms of itself but also in terms of the other. Fortunately, Lean allows for such mutual recursion. Here are the definitions we will use.
mutual
- def gcd_c1 (a b : Nat) : Int :=
- match b with
- | 0 => 1
- | n + 1 =>
- have : a % (n + 1) < n + 1 := mod_succ_lt a n
- gcd_c2 (n + 1) (a % (n + 1))
- --Corresponds to s = t'
- termination_by b
-
- def gcd_c2 (a b : Nat) : Int :=
- match b with
- | 0 => 0
- | n + 1 =>
- have : a % (n + 1) < n + 1 := mod_succ_lt a n
- gcd_c1 (n + 1) (a % (n + 1)) -
- (gcd_c2 (n + 1) (a % (n + 1))) * ↑(a / (n + 1))
- --Corresponds to t = s' - t'q
- termination_by b
-endNotice that in the definition of gcd_c2, the quotient a / (n + 1) is computed using natural-number division, but it is then coerced to be an integer so that it can be multiplied by the integer gcd_c2 (n + 1) (a % (n + 1)).
Our main theorem about these functions is that they give the coefficients needed to write gcd a b as a linear combination of a and b. As usual, stating a few lemmas first helps with the proof. We leave the proofs of two of them as exercises for you (hint: imitate the proof of gcd_nonzero above).
lemma gcd_c1_base (a : Nat) : gcd_c1 a 0 = 1 := by rfl
@@ -652,10 +655,10 @@ 7.2. Prime Factorizati
Before we can prove the existence of prime factorizations, we will need one more fact: every member of a list of natural numbers divides the product of the list. The proof will be by induction on the length of the list, so we will need to know how to work with lengths of lists in Lean. If l is a list, then the length of l is List.length l, which can also be written more briefly as l.length. We’ll need a few more theorems about lists:
@List.length_eq_zero : ∀ {α : Type u_1} {l : List α},
- List.length l = 0 ↔ l = []
+ l.length = 0 ↔ l = []
@List.length_cons : ∀ {α : Type u_1} (a : α) (as : List α),
- List.length (a :: as) = Nat.succ (List.length as)
+ (a :: as).length = as.length + 1
@List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α},
l ≠ [] → ∃ (b : α) (L : List α), l = b :: L
@@ -679,7 +682,7 @@ 7.2. Prime Factorizati
done
· -- Induction Step
fix n : Nat
- assume ih : ∀ (l : List Nat), List.length l = n → a ∈ l → a ∣ prod l
+ assume ih : ∀ (l : List Nat), l.length = n → a ∈ l → a ∣ prod l
fix l : List Nat
assume h1 : l.length = n + 1 --Goal : a ∈ l → a ∣ prod l
obtain (b : Nat) (h2 : ∃ (L : List Nat),
diff --git a/docs/Chap8.html b/docs/Chap8.html
index 09a0301..c953240 100644
--- a/docs/Chap8.html
+++ b/docs/Chap8.html
@@ -1922,7 +1922,7 @@ 8.2. Counta
apply Iff.intro
· -- (→)
assume h1 : l ∈ seq_by_length A 0
- define at h1 --h1 : l ∈ seq A ∧ List.length l = 0
+ define at h1 --h1 : l ∈ seq A ∧ l.length = 0
rewrite [List.length_eq_zero] at h1
define
show l = [] from h1.right
@@ -1930,7 +1930,7 @@ 8.2. Counta
· -- (←)
assume h1 : l ∈ {[]}
define at h1 --h1 : l = []
- define --Goal : l ∈ seq A ∧ List.length l = 0
+ define --Goal : l ∈ seq A ∧ l.length = 0
apply And.intro _ (List.length_eq_zero.rtl h1)
define --Goal : ∀ x ∈ l, x ∈ A
fix x : U
diff --git a/docs/How-To-Prove-It-With-Lean.pdf b/docs/How-To-Prove-It-With-Lean.pdf
index f909684..ebc1d60 100644
Binary files a/docs/How-To-Prove-It-With-Lean.pdf and b/docs/How-To-Prove-It-With-Lean.pdf differ
diff --git a/docs/search.json b/docs/search.json
index 386e32f..43e7178 100644
--- a/docs/search.json
+++ b/docs/search.json
@@ -291,14 +291,14 @@
"href": "Chap7.html#greatest-common-divisors",
"title": "7 Number Theory",
"section": "7.1. Greatest Common Divisors",
- "text": "7.1. Greatest Common Divisors\nThe proofs in this chapter and the next are significantly longer than those in previous chapters. As a result, we will skip some details in the text, leaving proofs of a number of theorems as exercises for you. The most interesting of these exercises are included in the exercise lists at the ends of the sections; for the rest, you can compare your solutions to proofs that can be found in the Lean package that accompanies this book. Also, we will occasionally use theorems that we have not used before without explanation. If necessary, you can use #check to look up what they say.\nSection 7.1 of HTPI introduces the Euclidean algorithm for computing the greatest common divisor (gcd) of two positive integers \\(a\\) and \\(b\\). The motivation for the algorithm is the fact that if \\(r\\) is the remainder when \\(a\\) is divided by \\(b\\), then any natural number that divides both \\(a\\) and \\(b\\) also divides \\(r\\), and any natural number that divides both \\(b\\) and \\(r\\) also divides \\(a\\).\nLet’s prove these statements in Lean. Recall that in Lean, the remainder when a is divided by b is called a mod b, and it is denoted a % b. We’ll prove the first statement, and leave the second as an exercise for you. It will be convenient for our work with greatest common divisors in Lean to let a and b be natural numbers rather than positive integers (thus allowing either of them to be zero).\ntheorem dvd_mod_of_dvd_a_b {a b d : Nat}\n (h1 : d ∣ a) (h2 : d ∣ b) : d ∣ (a % b) := by\n set q : Nat := a / b\n have h3 : b * q + a % b = a := Nat.div_add_mod a b\n obtain (j : Nat) (h4 : a = d * j) from h1\n obtain (k : Nat) (h5 : b = d * k) from h2\n define --Goal : ∃ (c : Nat), a % b = d * c\n apply Exists.intro (j - k * q)\n show a % b = d * (j - k * q) from\n calc a % b\n _ = b * q + a % b - b * q := (Nat.add_sub_cancel_left _ _).symm\n _ = a - b * q := by rw [h3]\n _ = d * j - d * (k * q) := by rw [h4, h5, mul_assoc]\n _ = d * (j - k * q) := (Nat.mul_sub_left_distrib _ _ _).symm\n done\n\ntheorem dvd_a_of_dvd_b_mod {a b d : Nat}\n (h1 : d ∣ b) (h2 : d ∣ (a % b)) : d ∣ a := sorry\nThese theorems tell us that the gcd of a and b is the same as the gcd of b and a % b, which suggests that the following recursive definition should compute the gcd of a and b:\ndef gcd (a b : Nat) : Nat :=\n match b with\n | 0 => a\n | n + 1 => **gcd (n + 1) (a % (n + 1))::\nUnfortunately, Lean puts a red squiggle under gcd (n + 1) (a % (n + 1)), and it displays in the Infoview a long error message that begins fail to show termination. What is Lean complaining about?\nThe problem is that recursive definitions are dangerous. To understand the danger, consider the following recursive definition:\ndef loop (n : Nat) : Nat := loop (n + 1)\nSuppose we try to use this definition to compute loop 3. The definition would lead us to perform the following calculation:\n\nloop 3 = loop 4 = loop 5 = loop 6 = ...\n\nClearly this calculation will go on forever and will never produce an answer. So the definition of loop does not actually succeed in defining a function from Nat to Nat.\nLean insists that recursive definitions must avoid such nonterminating calculations. Why did it accept all of our previous recursive definitions? The reason is that in each case, the definition of the value of the function at a natural number n referred only to values of the function at numbers smaller than n. Since a decreasing list of natural numbers cannot go on forever, such definitions lead to calculations that are guaranteed to terminate.\nWhat about our recursive definition of gcd a b? This function has two arguments, a and b, and when b = n + 1, the definition asks us to compute gcd (n + 1) (a % (n + 1)). The first argument here could actually be larger than the first argument in the value we are trying to compute, gcd a b. But the second argument will always be smaller, and that will suffice to guarantee that the calculation terminates. We can tell Lean to focus on the second argument b by adding a termination_by clause to the end of our recursive definition:\ndef gcd (a b : Nat) : Nat :=\n match b with\n | 0 => a\n | n + 1 => **gcd (n + 1) (a % (n + 1))::\n termination_by b\nUnfortunately, Lean still isn’t satisfied, but the error message this time is more helpful. The message says that Lean failed to prove termination, and at the end of the message it says that the goal it failed to prove is a % (n + 1) < n + 1, which is precisely what is needed to show that the second argument of gcd (n + 1) (a % (n + 1)) is smaller than the second argument of gcd a b when b = n + 1. We’ll need to provide a proof of this goal to convince Lean to accept our recursive definition. Fortunately, it’s not hard to prove:\nlemma mod_succ_lt (a n : Nat) : a % (n + 1) < n + 1 := by\n have h : n + 1 > 0 := Nat.succ_pos n\n show a % (n + 1) < n + 1 from Nat.mod_lt a h\n done\nLean’s error message suggests several ways to fix the problem with our recursive definition. We’ll use the first suggestion: Use `have` expressions to prove the remaining goals. Here, finally, is the definition of gcd that Lean is willing to accept:\ndef gcd (a b : Nat) : Nat :=\n match b with\n | 0 => a\n | n + 1 =>\n have : a % (n + 1) < n + 1 := mod_succ_lt a n\n gcd (n + 1) (a % (n + 1))\n termination_by b\nNotice that in the have expression, we have not bothered to specify an identifier for the assertion being proven, since we never need to refer to it. Let’s try out our gcd function:\n++#eval:: gcd 672 161 --Answer: 7. Note 672 = 7 * 96 and 161 = 7 * 23.\nTo establish the main properties of gcd a b we’ll need several lemmas. We prove some of them and leave others as exercises.\nlemma gcd_base (a : Nat) : gcd a 0 = a := by rfl\n\nlemma gcd_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :\n gcd a b = gcd b (a % b) := by\n obtain (n : Nat) (h2 : b = n + 1) from exists_eq_add_one_of_ne_zero h\n rewrite [h2] --Goal : gcd a (n + 1) = gcd (n + 1) (a % (n + 1))\n rfl\n done\n\nlemma mod_nonzero_lt (a : Nat) {b : Nat} (h : b ≠ 0) : a % b < b := sorry\n\nlemma dvd_self (n : Nat) : n ∣ n := sorry\nOne of the most important properties of gcd a b is that it divides both a and b. We prove it by strong induction on b.\ntheorem gcd_dvd : ∀ (b a : Nat), (gcd a b) ∣ a ∧ (gcd a b) ∣ b := by\n by_strong_induc\n fix b : Nat\n assume ih : ∀ b_1 < b, ∀ (a : Nat), (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1\n fix a : Nat\n by_cases h1 : b = 0\n · -- Case 1. h1 : b = 0\n rewrite [h1, gcd_base] --Goal: a ∣ a ∧ a ∣ 0\n apply And.intro (dvd_self a)\n define\n apply Exists.intro 0\n rfl\n done\n · -- Case 2. h1 : b ≠ 0\n rewrite [gcd_nonzero a h1]\n --Goal : gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b\n have h2 : a % b < b := mod_nonzero_lt a h1\n have h3 : (gcd b (a % b)) ∣ b ∧ (gcd b (a % b)) ∣ (a % b) :=\n ih (a % b) h2 b\n apply And.intro _ h3.left\n show (gcd b (a % b)) ∣ a from dvd_a_of_dvd_b_mod h3.left h3.right\n done\n done\nYou may wonder why we didn’t start the proof like this:\ntheorem gcd_dvd : ∀ (a b : Nat), (gcd a b) ∣ a ∧ (gcd a b) ∣ b := by\n fix a : Nat\n by_strong_induc\n fix b : Nat\n assume ih : ∀ b_1 < b, (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1\nIn fact, this approach wouldn’t have worked. It is an interesting exercise to try to complete this version of the proof and see why it fails.\nAnother interesting question is why we asserted both (gcd a b) ∣ a and (gcd a b) ∣ b in the same theorem. Wouldn’t it have been easier to give separate proofs of the statements ∀ (b a : Nat), (gcd a b) ∣ a and ∀ (b a : Nat), (gcd a b) ∣ b? Again, you might find it enlightening to see why that wouldn’t have worked. However, now that we have proven both divisibility statements, we can state them as separate theorems:\ntheorem gcd_dvd_left (a b : Nat) : (gcd a b) ∣ a := (gcd_dvd b a).left\n\ntheorem gcd_dvd_right (a b : Nat) : (gcd a b) ∣ b := (gcd_dvd b a).right\nNext we turn to Theorem 7.1.4 in HTPI, which says that there are integers \\(s\\) and \\(t\\) such that \\(\\text{gcd}(a, b) = s a + t b\\). (We say that \\(\\text{gcd}(a, b)\\) can be written as a linear combination of \\(a\\) and \\(b\\).) In HTPI, this is proven by using an extended version of the Euclidean algorithm to compute the coefficients \\(s\\) and \\(t\\). Here we will use a different recursive procedure to compute \\(s\\) and \\(t\\). If \\(b = 0\\), then \\(\\text{gcd}(a, b) = a = 1 \\cdot a + 0 \\cdot b\\), so we can use the values \\(s = 1\\) and \\(t = 0\\). Otherwise, let \\(q\\) and \\(r\\) be the quotient and remainder when \\(a\\) is divided by \\(b\\). Then \\(a = bq + r\\) and \\(\\text{gcd}(a, b) = \\text{gcd}(b, r)\\). Now suppose that we have already computed integers \\(s'\\) and \\(t'\\) such that \\[\n\\text{gcd}(b, r) = s' b + t' r.\n\\] Then \\[\\begin{align*}\n\\text{gcd}(a, b) &= \\text{gcd}(b, r) = s' b + t' r\\\\\n&= s' b + t' (a - bq) = t' a + (s' - t'q)b.\n\\end{align*}\\] Thus, to write \\(\\text{gcd}(a, b) = s a + t b\\) we can use the values \\[\\begin{equation}\\tag{$*$}\ns = t', \\qquad t = s' - t'q.\n\\end{equation}\\]\nWe will use these equations as the basis for recursive definitions of Lean functions gcd_c1 and gcd_c2 such that the required coefficients can be obtained from the formulas s = gcd_c1 a b and t = gcd_c2 a b. Notice that s and t could be negative, so they must have type Int, not Nat. As a result, in definitions and theorems involving gcd_c1 and gcd_c2 we will sometimes have to deal with coercion of natural numbers to integers.\nThe functions gcd_c1 and gcd_c2 will be mutually recursive; in other words, each will be defined not only in terms of itself but also in terms of the other. Fortunately, Lean allows for such mutual recursion. Here are the definitions we will use.\nmutual\n def gcd_c1 (a b : Nat) : Int :=\n match b with\n | 0 => 1\n | n + 1 =>\n have : a % (n + 1) < n + 1 := mod_succ_lt a n\n gcd_c2 (n + 1) (a % (n + 1))\n --Corresponds to s = t'\n termination_by b\n\n def gcd_c2 (a b : Nat) : Int :=\n match b with\n | 0 => 0\n | n + 1 =>\n have : a % (n + 1) < n + 1 := mod_succ_lt a n\n gcd_c1 (n + 1) (a % (n + 1)) -\n (gcd_c2 (n + 1) (a % (n + 1))) * ↑(a / (n + 1))\n --Corresponds to t = s' - t'q\n termination_by b\nend\nNotice that in the definition of gcd_c2, the quotient a / (n + 1) is computed using natural-number division, but it is then coerced to be an integer so that it can be multiplied by the integer gcd_c2 (n + 1) (a % (n + 1)).\nOur main theorem about these functions is that they give the coefficients needed to write gcd a b as a linear combination of a and b. As usual, stating a few lemmas first helps with the proof. We leave the proofs of two of them as exercises for you (hint: imitate the proof of gcd_nonzero above).\nlemma gcd_c1_base (a : Nat) : gcd_c1 a 0 = 1 := by rfl\n\nlemma gcd_c1_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :\n gcd_c1 a b = gcd_c2 b (a % b) := sorry\n\nlemma gcd_c2_base (a : Nat) : gcd_c2 a 0 = 0 := by rfl\n\nlemma gcd_c2_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :\n gcd_c2 a b = gcd_c1 b (a % b) - (gcd_c2 b (a % b)) * ↑(a / b) := sorry\nWith that preparation, we are ready to prove that gcd_c1 a b and gcd_c2 a b give coefficients for expressing gcd a b as a linear combination of a and b. Of course, the theorem is proven by strong induction. For clarity, we’ll write the coercions explicitly in this proof. We’ll make a few comments after the proof that may help you follow the details.\ntheorem gcd_lin_comb : ∀ (b a : Nat),\n (gcd_c1 a b) * ↑a + (gcd_c2 a b) * ↑b = ↑(gcd a b) := by\n by_strong_induc\n fix b : Nat\n assume ih : ∀ b_1 < b, ∀ (a : Nat),\n (gcd_c1 a b_1) * ↑a + (gcd_c2 a b_1) * ↑b_1 = ↑(gcd a b_1)\n fix a : Nat\n by_cases h1 : b = 0\n · -- Case 1. h1 : b = 0\n rewrite [h1, gcd_c1_base, gcd_c2_base, gcd_base]\n --Goal : 1 * ↑a + 0 * ↑0 = ↑a\n ring\n done\n · -- Case 2. h1 : b ≠ 0\n rewrite [gcd_c1_nonzero a h1, gcd_c2_nonzero a h1, gcd_nonzero a h1]\n --Goal : gcd_c2 b (a % b) * ↑a +\n -- (gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)) * ↑b =\n -- ↑(gcd b (a % b))\n set r : Nat := a % b\n set q : Nat := a / b\n set s : Int := gcd_c1 b r\n set t : Int := gcd_c2 b r\n --Goal : t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)\n have h2 : r < b := mod_nonzero_lt a h1\n have h3 : s * ↑b + t * ↑r = ↑(gcd b r) := ih r h2 b\n have h4 : b * q + r = a := Nat.div_add_mod a b\n rewrite [←h3, ←h4]\n rewrite [Nat.cast_add, Nat.cast_mul]\n --Goal : t * (↑b * ↑q + ↑r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r\n ring\n done\n done\nIn case 2, we have introduced the variables r, q, s, and t to simplify the notation. Notice that the set tactic automatically plugs in this notation in the goal. After the step rewrite [←h3, ←h4], the goal contains the expression ↑(b * q + r). You can use the #check command to see why Nat.cast_add and Nat.cast_mul convert this expression to first ↑(b * q) + ↑r and then ↑b * ↑q + ↑r. Without those steps, the ring tactic would not have been able to complete the proof.\nWe can try out the functions gcd_c1 and gcd_c2 as follows:\n++#eval:: gcd_c1 672 161 --Answer: 6\n++#eval:: gcd_c2 672 161 --Answer: -25\n --Note 6 * 672 - 25 * 161 = 4032 - 4025 = 7 = gcd 672 161\nFinally, we turn to Theorem 7.1.6 in HTPI, which expresses one of the senses in which gcd a b is the greatest common divisor of a and b. Our proof follows the strategy of the proof in HTPI, with one additional step: we begin by using the theorem Int.natCast_dvd_natCast to change the goal from d ∣ gcd a b to ↑d ∣ ↑(gcd a b) (where the coercions are from Nat to Int), so that the rest of the proof can work with integer algebra rather than natural-number algebra.\ntheorem Theorem_7_1_6 {d a b : Nat} (h1 : d ∣ a) (h2 : d ∣ b) :\n d ∣ gcd a b := by\n rewrite [←Int.natCast_dvd_natCast] --Goal : ↑d ∣ ↑(gcd a b)\n set s : Int := gcd_c1 a b\n set t : Int := gcd_c2 a b\n have h3 : s * ↑a + t * ↑b = ↑(gcd a b) := gcd_lin_comb b a\n rewrite [←h3] --Goal : ↑d ∣ s * ↑a + t * ↑b\n obtain (j : Nat) (h4 : a = d * j) from h1\n obtain (k : Nat) (h5 : b = d * k) from h2\n rewrite [h4, h5, Nat.cast_mul, Nat.cast_mul]\n --Goal : ↑d ∣ s * (↑d * ↑j) + t * (↑d * ↑k)\n define\n apply Exists.intro (s * ↑j + t * ↑k)\n ring\n done\nWe will ask you in the exercises to prove that, among the common divisors of a and b, gcd a b is the greatest with respect to the usual ordering of the natural numbers (as long as gcd a b ≠ 0).\n\nExercises\n\ntheorem dvd_a_of_dvd_b_mod {a b d : Nat}\n (h1 : d ∣ b) (h2 : d ∣ (a % b)) : d ∣ a := sorry\n\n\nlemma gcd_comm_lt {a b : Nat} (h : a < b) : gcd a b = gcd b a := sorry\n\ntheorem gcd_comm (a b : Nat) : gcd a b = gcd b a := sorry\n\n\ntheorem Exercise_7_1_5 (a b : Nat) (n : Int) :\n (∃ (s t : Int), s * a + t * b = n) ↔ (↑(gcd a b) : Int) ∣ n := sorry\n\n\ntheorem Exercise_7_1_6 (a b c : Nat) :\n gcd a b = gcd (a + b * c) b := sorry\n\n\ntheorem gcd_is_nonzero {a b : Nat} (h : a ≠ 0 ∨ b ≠ 0) :\n gcd a b ≠ 0 := sorry\n\n\ntheorem gcd_greatest {a b d : Nat} (h1 : gcd a b ≠ 0)\n (h2 : d ∣ a) (h3 : d ∣ b) : d ≤ gcd a b := sorry\n\n\nlemma Lemma_7_1_10a {a b : Nat}\n (n : Nat) (h : a ∣ b) : (n * a) ∣ (n * b) := sorry\n\nlemma Lemma_7_1_10b {a b n : Nat}\n (h1 : n ≠ 0) (h2 : (n * a) ∣ (n * b)) : a ∣ b := sorry\n\nlemma Lemma_7_1_10c {a b : Nat}\n (h1 : a ∣ b) (h2 : b ∣ a) : a = b := sorry\n\ntheorem Exercise_7_1_10 (a b n : Nat) :\n gcd (n * a) (n * b) = n * gcd a b := sorry"
+ "text": "7.1. Greatest Common Divisors\nThe proofs in this chapter and the next are significantly longer than those in previous chapters. As a result, we will skip some details in the text, leaving proofs of a number of theorems as exercises for you. The most interesting of these exercises are included in the exercise lists at the ends of the sections; for the rest, you can compare your solutions to proofs that can be found in the Lean package that accompanies this book. Also, we will occasionally use theorems that we have not used before without explanation. If necessary, you can use #check to look up what they say.\nSection 7.1 of HTPI introduces the Euclidean algorithm for computing the greatest common divisor (gcd) of two positive integers \\(a\\) and \\(b\\). The motivation for the algorithm is the fact that if \\(r\\) is the remainder when \\(a\\) is divided by \\(b\\), then any natural number that divides both \\(a\\) and \\(b\\) also divides \\(r\\), and any natural number that divides both \\(b\\) and \\(r\\) also divides \\(a\\).\nLet’s prove these statements in Lean. Recall that in Lean, the remainder when a is divided by b is called a mod b, and it is denoted a % b. We’ll prove the first statement, and leave the second as an exercise for you. It will be convenient for our work with greatest common divisors in Lean to let a and b be natural numbers rather than positive integers (thus allowing either of them to be zero).\ntheorem dvd_mod_of_dvd_a_b {a b d : Nat}\n (h1 : d ∣ a) (h2 : d ∣ b) : d ∣ (a % b) := by\n set q : Nat := a / b\n have h3 : b * q + a % b = a := Nat.div_add_mod a b\n obtain (j : Nat) (h4 : a = d * j) from h1\n obtain (k : Nat) (h5 : b = d * k) from h2\n define --Goal : ∃ (c : Nat), a % b = d * c\n apply Exists.intro (j - k * q)\n show a % b = d * (j - k * q) from\n calc a % b\n _ = b * q + a % b - b * q := (Nat.add_sub_cancel_left _ _).symm\n _ = a - b * q := by rw [h3]\n _ = d * j - d * (k * q) := by rw [h4, h5, mul_assoc]\n _ = d * (j - k * q) := (Nat.mul_sub_left_distrib _ _ _).symm\n done\n\ntheorem dvd_a_of_dvd_b_mod {a b d : Nat}\n (h1 : d ∣ b) (h2 : d ∣ (a % b)) : d ∣ a := sorry\nThese theorems tell us that the gcd of a and b is the same as the gcd of b and a % b, which suggests that the following recursive definition should compute the gcd of a and b:\ndef **gcd:: (a b : Nat) : Nat :=\n match b with\n | 0 => a\n | n + 1 => gcd (n + 1) (a % (n + 1))\nUnfortunately, Lean puts a red squiggle under gcd, and it displays in the Infoview a long error message that begins fail to show termination. What is Lean complaining about?\nThe problem is that recursive definitions are dangerous. To understand the danger, consider the following recursive definition:\ndef loop (n : Nat) : Nat := loop (n + 1)\nSuppose we try to use this definition to compute loop 3. The definition would lead us to perform the following calculation:\n\nloop 3 = loop 4 = loop 5 = loop 6 = ...\n\nClearly this calculation will go on forever and will never produce an answer. So the definition of loop does not actually succeed in defining a function from Nat to Nat.\nLean insists that recursive definitions must avoid such nonterminating calculations. Why did it accept all of our previous recursive definitions? The reason is that in each case, the definition of the value of the function at a natural number n referred only to values of the function at numbers smaller than n. Since a decreasing list of natural numbers cannot go on forever, such definitions lead to calculations that are guaranteed to terminate.\nWhat about our recursive definition of gcd a b? This function has two arguments, a and b, and when b = n + 1, the definition asks us to compute gcd (n + 1) (a % (n + 1)). The first argument here could actually be larger than the first argument in the value we are trying to compute, gcd a b. But the second argument will always be smaller, and that will suffice to guarantee that the calculation terminates. We can tell Lean to focus on the second argument b by adding a termination_by clause to the end of our recursive definition:\ndef gcd (a b : Nat) : Nat :=\n match b with\n | 0 => a\n | n + 1 => **gcd (n + 1) (a % (n + 1))::\n termination_by b\nUnfortunately, Lean still isn’t satisfied, but the error message this time is more helpful. The message says that Lean failed to prove termination, and at the end of the message it says that the goal it failed to prove is a % (n + 1) < n + 1, which is precisely what is needed to show that the second argument of gcd (n + 1) (a % (n + 1)) is smaller than the second argument of gcd a b when b = n + 1. We’ll need to provide a proof of this goal to convince Lean to accept our recursive definition. Fortunately, it’s not hard to prove:\nlemma mod_succ_lt (a n : Nat) : a % (n + 1) < n + 1 := by\n have h : n + 1 > 0 := Nat.succ_pos n\n show a % (n + 1) < n + 1 from Nat.mod_lt a h\n done\nLean’s error message suggests several ways to fix the problem with our recursive definition. We’ll use the first suggestion: Use `have`-expressions to prove the remaining goals. Here, finally, is the definition of gcd that Lean is willing to accept. (You can ignore the initial line @[semireducible]. For technical reasons that we won’t go into, this line is needed to make this complicated recursive definition work in proofs the same way that our previous, simpler recursive definitions did.)\n@[semireducible]\ndef gcd (a b : Nat) : Nat :=\n match b with\n | 0 => a\n | n + 1 =>\n have : a % (n + 1) < n + 1 := mod_succ_lt a n\n gcd (n + 1) (a % (n + 1))\n termination_by b\nNotice that in the have expression, we have not bothered to specify an identifier for the assertion being proven, since we never need to refer to it. Let’s try out our gcd function:\n++#eval:: gcd 672 161 --Answer: 7. Note 672 = 7 * 96 and 161 = 7 * 23.\nTo establish the main properties of gcd a b we’ll need several lemmas. We prove some of them and leave others as exercises.\nlemma gcd_base (a : Nat) : gcd a 0 = a := by rfl\n\nlemma gcd_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :\n gcd a b = gcd b (a % b) := by\n obtain (n : Nat) (h2 : b = n + 1) from exists_eq_add_one_of_ne_zero h\n rewrite [h2] --Goal : gcd a (n + 1) = gcd (n + 1) (a % (n + 1))\n rfl\n done\n\nlemma mod_nonzero_lt (a : Nat) {b : Nat} (h : b ≠ 0) : a % b < b := sorry\n\nlemma dvd_self (n : Nat) : n ∣ n := sorry\nOne of the most important properties of gcd a b is that it divides both a and b. We prove it by strong induction on b.\ntheorem gcd_dvd : ∀ (b a : Nat), (gcd a b) ∣ a ∧ (gcd a b) ∣ b := by\n by_strong_induc\n fix b : Nat\n assume ih : ∀ b_1 < b, ∀ (a : Nat), (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1\n fix a : Nat\n by_cases h1 : b = 0\n · -- Case 1. h1 : b = 0\n rewrite [h1, gcd_base] --Goal: a ∣ a ∧ a ∣ 0\n apply And.intro (dvd_self a)\n define\n apply Exists.intro 0\n rfl\n done\n · -- Case 2. h1 : b ≠ 0\n rewrite [gcd_nonzero a h1]\n --Goal : gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b\n have h2 : a % b < b := mod_nonzero_lt a h1\n have h3 : (gcd b (a % b)) ∣ b ∧ (gcd b (a % b)) ∣ (a % b) :=\n ih (a % b) h2 b\n apply And.intro _ h3.left\n show (gcd b (a % b)) ∣ a from dvd_a_of_dvd_b_mod h3.left h3.right\n done\n done\nYou may wonder why we didn’t start the proof like this:\ntheorem gcd_dvd : ∀ (a b : Nat), (gcd a b) ∣ a ∧ (gcd a b) ∣ b := by\n fix a : Nat\n by_strong_induc\n fix b : Nat\n assume ih : ∀ b_1 < b, (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1\nIn fact, this approach wouldn’t have worked. It is an interesting exercise to try to complete this version of the proof and see why it fails.\nAnother interesting question is why we asserted both (gcd a b) ∣ a and (gcd a b) ∣ b in the same theorem. Wouldn’t it have been easier to give separate proofs of the statements ∀ (b a : Nat), (gcd a b) ∣ a and ∀ (b a : Nat), (gcd a b) ∣ b? Again, you might find it enlightening to see why that wouldn’t have worked. However, now that we have proven both divisibility statements, we can state them as separate theorems:\ntheorem gcd_dvd_left (a b : Nat) : (gcd a b) ∣ a := (gcd_dvd b a).left\n\ntheorem gcd_dvd_right (a b : Nat) : (gcd a b) ∣ b := (gcd_dvd b a).right\nNext we turn to Theorem 7.1.4 in HTPI, which says that there are integers \\(s\\) and \\(t\\) such that \\(\\text{gcd}(a, b) = s a + t b\\). (We say that \\(\\text{gcd}(a, b)\\) can be written as a linear combination of \\(a\\) and \\(b\\).) In HTPI, this is proven by using an extended version of the Euclidean algorithm to compute the coefficients \\(s\\) and \\(t\\). Here we will use a different recursive procedure to compute \\(s\\) and \\(t\\). If \\(b = 0\\), then \\(\\text{gcd}(a, b) = a = 1 \\cdot a + 0 \\cdot b\\), so we can use the values \\(s = 1\\) and \\(t = 0\\). Otherwise, let \\(q\\) and \\(r\\) be the quotient and remainder when \\(a\\) is divided by \\(b\\). Then \\(a = bq + r\\) and \\(\\text{gcd}(a, b) = \\text{gcd}(b, r)\\). Now suppose that we have already computed integers \\(s'\\) and \\(t'\\) such that \\[\n\\text{gcd}(b, r) = s' b + t' r.\n\\] Then \\[\\begin{align*}\n\\text{gcd}(a, b) &= \\text{gcd}(b, r) = s' b + t' r\\\\\n&= s' b + t' (a - bq) = t' a + (s' - t'q)b.\n\\end{align*}\\] Thus, to write \\(\\text{gcd}(a, b) = s a + t b\\) we can use the values \\[\\begin{equation}\\tag{$*$}\ns = t', \\qquad t = s' - t'q.\n\\end{equation}\\]\nWe will use these equations as the basis for recursive definitions of Lean functions gcd_c1 and gcd_c2 such that the required coefficients can be obtained from the formulas s = gcd_c1 a b and t = gcd_c2 a b. Notice that s and t could be negative, so they must have type Int, not Nat. As a result, in definitions and theorems involving gcd_c1 and gcd_c2 we will sometimes have to deal with coercion of natural numbers to integers.\nThe functions gcd_c1 and gcd_c2 will be mutually recursive; in other words, each will be defined not only in terms of itself but also in terms of the other. Fortunately, Lean allows for such mutual recursion. Here are the definitions we will use.\nmutual\n @[semireducible]\n def gcd_c1 (a b : Nat) : Int :=\n match b with\n | 0 => 1\n | n + 1 =>\n have : a % (n + 1) < n + 1 := mod_succ_lt a n\n gcd_c2 (n + 1) (a % (n + 1))\n --Corresponds to s = t'\n termination_by b\n\n @[semireducible]\n def gcd_c2 (a b : Nat) : Int :=\n match b with\n | 0 => 0\n | n + 1 =>\n have : a % (n + 1) < n + 1 := mod_succ_lt a n\n gcd_c1 (n + 1) (a % (n + 1)) -\n (gcd_c2 (n + 1) (a % (n + 1))) * ↑(a / (n + 1))\n --Corresponds to t = s' - t'q\n termination_by b\nend\nNotice that in the definition of gcd_c2, the quotient a / (n + 1) is computed using natural-number division, but it is then coerced to be an integer so that it can be multiplied by the integer gcd_c2 (n + 1) (a % (n + 1)).\nOur main theorem about these functions is that they give the coefficients needed to write gcd a b as a linear combination of a and b. As usual, stating a few lemmas first helps with the proof. We leave the proofs of two of them as exercises for you (hint: imitate the proof of gcd_nonzero above).\nlemma gcd_c1_base (a : Nat) : gcd_c1 a 0 = 1 := by rfl\n\nlemma gcd_c1_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :\n gcd_c1 a b = gcd_c2 b (a % b) := sorry\n\nlemma gcd_c2_base (a : Nat) : gcd_c2 a 0 = 0 := by rfl\n\nlemma gcd_c2_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :\n gcd_c2 a b = gcd_c1 b (a % b) - (gcd_c2 b (a % b)) * ↑(a / b) := sorry\nWith that preparation, we are ready to prove that gcd_c1 a b and gcd_c2 a b give coefficients for expressing gcd a b as a linear combination of a and b. Of course, the theorem is proven by strong induction. For clarity, we’ll write the coercions explicitly in this proof. We’ll make a few comments after the proof that may help you follow the details.\ntheorem gcd_lin_comb : ∀ (b a : Nat),\n (gcd_c1 a b) * ↑a + (gcd_c2 a b) * ↑b = ↑(gcd a b) := by\n by_strong_induc\n fix b : Nat\n assume ih : ∀ b_1 < b, ∀ (a : Nat),\n (gcd_c1 a b_1) * ↑a + (gcd_c2 a b_1) * ↑b_1 = ↑(gcd a b_1)\n fix a : Nat\n by_cases h1 : b = 0\n · -- Case 1. h1 : b = 0\n rewrite [h1, gcd_c1_base, gcd_c2_base, gcd_base]\n --Goal : 1 * ↑a + 0 * ↑0 = ↑a\n ring\n done\n · -- Case 2. h1 : b ≠ 0\n rewrite [gcd_c1_nonzero a h1, gcd_c2_nonzero a h1, gcd_nonzero a h1]\n --Goal : gcd_c2 b (a % b) * ↑a +\n -- (gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)) * ↑b =\n -- ↑(gcd b (a % b))\n set r : Nat := a % b\n set q : Nat := a / b\n set s : Int := gcd_c1 b r\n set t : Int := gcd_c2 b r\n --Goal : t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)\n have h2 : r < b := mod_nonzero_lt a h1\n have h3 : s * ↑b + t * ↑r = ↑(gcd b r) := ih r h2 b\n have h4 : b * q + r = a := Nat.div_add_mod a b\n rewrite [←h3, ←h4]\n rewrite [Nat.cast_add, Nat.cast_mul]\n --Goal : t * (↑b * ↑q + ↑r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r\n ring\n done\n done\nIn case 2, we have introduced the variables r, q, s, and t to simplify the notation. Notice that the set tactic automatically plugs in this notation in the goal. After the step rewrite [←h3, ←h4], the goal contains the expression ↑(b * q + r). You can use the #check command to see why Nat.cast_add and Nat.cast_mul convert this expression to first ↑(b * q) + ↑r and then ↑b * ↑q + ↑r. Without those steps, the ring tactic would not have been able to complete the proof.\nWe can try out the functions gcd_c1 and gcd_c2 as follows:\n++#eval:: gcd_c1 672 161 --Answer: 6\n++#eval:: gcd_c2 672 161 --Answer: -25\n --Note 6 * 672 - 25 * 161 = 4032 - 4025 = 7 = gcd 672 161\nFinally, we turn to Theorem 7.1.6 in HTPI, which expresses one of the senses in which gcd a b is the greatest common divisor of a and b. Our proof follows the strategy of the proof in HTPI, with one additional step: we begin by using the theorem Int.natCast_dvd_natCast to change the goal from d ∣ gcd a b to ↑d ∣ ↑(gcd a b) (where the coercions are from Nat to Int), so that the rest of the proof can work with integer algebra rather than natural-number algebra.\ntheorem Theorem_7_1_6 {d a b : Nat} (h1 : d ∣ a) (h2 : d ∣ b) :\n d ∣ gcd a b := by\n rewrite [←Int.natCast_dvd_natCast] --Goal : ↑d ∣ ↑(gcd a b)\n set s : Int := gcd_c1 a b\n set t : Int := gcd_c2 a b\n have h3 : s * ↑a + t * ↑b = ↑(gcd a b) := gcd_lin_comb b a\n rewrite [←h3] --Goal : ↑d ∣ s * ↑a + t * ↑b\n obtain (j : Nat) (h4 : a = d * j) from h1\n obtain (k : Nat) (h5 : b = d * k) from h2\n rewrite [h4, h5, Nat.cast_mul, Nat.cast_mul]\n --Goal : ↑d ∣ s * (↑d * ↑j) + t * (↑d * ↑k)\n define\n apply Exists.intro (s * ↑j + t * ↑k)\n ring\n done\nWe will ask you in the exercises to prove that, among the common divisors of a and b, gcd a b is the greatest with respect to the usual ordering of the natural numbers (as long as gcd a b ≠ 0).\n\nExercises\n\ntheorem dvd_a_of_dvd_b_mod {a b d : Nat}\n (h1 : d ∣ b) (h2 : d ∣ (a % b)) : d ∣ a := sorry\n\n\nlemma gcd_comm_lt {a b : Nat} (h : a < b) : gcd a b = gcd b a := sorry\n\ntheorem gcd_comm (a b : Nat) : gcd a b = gcd b a := sorry\n\n\ntheorem Exercise_7_1_5 (a b : Nat) (n : Int) :\n (∃ (s t : Int), s * a + t * b = n) ↔ (↑(gcd a b) : Int) ∣ n := sorry\n\n\ntheorem Exercise_7_1_6 (a b c : Nat) :\n gcd a b = gcd (a + b * c) b := sorry\n\n\ntheorem gcd_is_nonzero {a b : Nat} (h : a ≠ 0 ∨ b ≠ 0) :\n gcd a b ≠ 0 := sorry\n\n\ntheorem gcd_greatest {a b d : Nat} (h1 : gcd a b ≠ 0)\n (h2 : d ∣ a) (h3 : d ∣ b) : d ≤ gcd a b := sorry\n\n\nlemma Lemma_7_1_10a {a b : Nat}\n (n : Nat) (h : a ∣ b) : (n * a) ∣ (n * b) := sorry\n\nlemma Lemma_7_1_10b {a b n : Nat}\n (h1 : n ≠ 0) (h2 : (n * a) ∣ (n * b)) : a ∣ b := sorry\n\nlemma Lemma_7_1_10c {a b : Nat}\n (h1 : a ∣ b) (h2 : b ∣ a) : a = b := sorry\n\ntheorem Exercise_7_1_10 (a b n : Nat) :\n gcd (n * a) (n * b) = n * gcd a b := sorry"
},
{
"objectID": "Chap7.html#prime-factorization",
"href": "Chap7.html#prime-factorization",
"title": "7 Number Theory",
"section": "7.2. Prime Factorization",
- "text": "7.2. Prime Factorization\nA natural number \\(n\\) is said to be prime if it is at least 2 and it cannot be written as a product of two smaller natural numbers. Of course, we can write this definition in Lean.\ndef prime (n : Nat) : Prop :=\n 2 ≤ n ∧ ¬∃ (a b : Nat), a * b = n ∧ a < n ∧ b < n\nThe main goal of Section 7.2 of HTPI is to prove that every positive integer has a unique prime factorization; that is, it can be written in a unique way as the product of a nondecreasing list of prime numbers. To get started on this goal, we first prove that every number greater than or equal to 2 has a prime factor. We leave one lemma as an exercise for you (it is a natural-number version of Theorem_3_3_7).\ndef prime_factor (p n : Nat) : Prop := prime p ∧ p ∣ n\n\nlemma dvd_trans {a b c : Nat} (h1 : a ∣ b) (h2 : b ∣ c) : a ∣ c := sorry\n\nlemma exists_prime_factor : ∀ (n : Nat), 2 ≤ n →\n ∃ (p : Nat), prime_factor p n := by\n by_strong_induc\n fix n : Nat\n assume ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ (p : Nat), prime_factor p n_1\n assume h1 : 2 ≤ n\n by_cases h2 : prime n\n · -- Case 1. h2 : prime n\n apply Exists.intro n\n define --Goal : prime n ∧ n ∣ n\n show prime n ∧ n ∣ n from And.intro h2 (dvd_self n)\n done\n · -- Case 2. h2 : ¬prime n\n define at h2\n --h2 : ¬(2 ≤ n ∧ ¬∃ (a b : Nat), a * b = n ∧ a < n ∧ b < n)\n demorgan at h2\n disj_syll h2 h1\n obtain (a : Nat) (h3 : ∃ (b : Nat), a * b = n ∧ a < n ∧ b < n) from h2\n obtain (b : Nat) (h4 : a * b = n ∧ a < n ∧ b < n) from h3\n have h5 : 2 ≤ a := by\n by_contra h6\n have h7 : a ≤ 1 := by linarith\n have h8 : n ≤ b :=\n calc n\n _ = a * b := h4.left.symm\n _ ≤ 1 * b := by rel [h7]\n _ = b := by ring\n linarith --n ≤ b contradicts b < n\n done\n have h6 : ∃ (p : Nat), prime_factor p a := ih a h4.right.left h5\n obtain (p : Nat) (h7 : prime_factor p a) from h6\n apply Exists.intro p\n define --Goal : prime p ∧ p ∣ n\n define at h7 --h7 : prime p ∧ p ∣ a\n apply And.intro h7.left\n have h8 : a ∣ n := by\n apply Exists.intro b\n show n = a * b from (h4.left).symm\n done\n show p ∣ n from dvd_trans h7.right h8\n done\n done\nOf course, by the well-ordering principle, an immediate consequence of this lemma is that every number greater than or equal to 2 has a smallest prime factor.\nlemma exists_least_prime_factor {n : Nat} (h : 2 ≤ n) :\n ∃ (p : Nat), prime_factor p n ∧\n ∀ (q : Nat), prime_factor q n → p ≤ q := by\n set S : Set Nat := {p : Nat | prime_factor p n}\n have h2 : ∃ (p : Nat), p ∈ S := exists_prime_factor n h\n show ∃ (p : Nat), prime_factor p n ∧\n ∀ (q : Nat), prime_factor q n → p ≤ q from well_ord_princ S h2\n done\nTo talk about prime factorizations of positive integers, we’ll need to introduce a new type. If U is any type, then List U is the type of lists of objects of type U. Such a list is written in square brackets, with the entries separated by commas. For example, [3, 7, 1] has type List Nat. The notation [] denotes the empty list, and if a has type U and l has type List U, then a :: l denotes the list consisting of a followed by the entries of l. The empty list is sometimes called the nil list, and the operation of constructing a list a :: l from a and l is called cons (short for construct). Every list can be constructed by applying the cons operation repeatedly, starting with the nil list. For example,\n\n[3, 7, 1] = 3 :: [7, 1] = 3 :: (7 :: [1]) = 3 :: (7 :: (1 :: [])).\n\nIf l has type List U and a has type U, then a ∈ l means that a is one of the entries in the list l. For example, 7 ∈ [3, 7, 1]. Lean knows several theorems about this notation:\n\n@List.not_mem_nil : ∀ {α : Type u_1} (a : α),\n a ∉ []\n\n@List.mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α},\n a ∈ b :: l ↔ a = b ∨ a ∈ l\n\n@List.mem_cons_self : ∀ {α : Type u_1} (a : α) (l : List α),\n a ∈ a :: l\n\n@List.mem_cons_of_mem : ∀ {α : Type u_1} (y : α) {a : α} {l : List α},\n a ∈ l → a ∈ y :: l\n\nThe first two theorems give the conditions under which something is a member of the nil list or a list constructed by cons, and the last two are easy consequences of the second.\nTo define prime factorizations, we must define several concepts first. Some of these concepts are most easily defined recursively.\ndef all_prime (l : List Nat) : Prop := ∀ p ∈ l, prime p\n\ndef nondec (l : List Nat) : Prop :=\n match l with\n | [] => True --Of course, True is a proposition that is always true\n | n :: L => (∀ m ∈ L, n ≤ m) ∧ nondec L\n\ndef nondec_prime_list (l : List Nat) : Prop := all_prime l ∧ nondec l\n\ndef prod (l : List Nat) : Nat :=\n match l with\n | [] => 1\n | n :: L => n * (prod L)\n\ndef prime_factorization (n : Nat) (l : List Nat) : Prop :=\n nondec_prime_list l ∧ prod l = n\nAccording to these definitions, all_prime l means that every member of the list l is prime, nondec l means that every member of l is less than or equal to all later members, prod l is the product of all members of l, and prime_factorization n l means that l is a nondecreasing list of prime numbers whose product is n. It will be convenient to spell out some consequences of these definitions in several lemmas:\nlemma all_prime_nil : all_prime [] := by\n define --Goal : ∀ p ∈ [], prime p\n fix p : Nat\n contrapos --Goal : ¬prime p → p ∉ []\n assume h1 : ¬prime p\n show p ∉ [] from List.not_mem_nil p\n done\n\nlemma all_prime_cons (n : Nat) (L : List Nat) :\n all_prime (n :: L) ↔ prime n ∧ all_prime L := by\n apply Iff.intro\n · -- (→)\n assume h1 : all_prime (n :: L) --Goal : prime n ∧ all_prime L\n define at h1 --h1 : ∀ p ∈ n :: L, prime p\n apply And.intro (h1 n (List.mem_cons_self n L))\n define --Goal : ∀ p ∈ L, prime p\n fix p : Nat\n assume h2 : p ∈ L\n show prime p from h1 p (List.mem_cons_of_mem n h2)\n done\n · -- (←)\n assume h1 : prime n ∧ all_prime L --Goal : all_prime (n :: l)\n define : all_prime L at h1\n define\n fix p : Nat\n assume h2 : p ∈ n :: L\n rewrite [List.mem_cons] at h2 --h2 : p = n ∨ p ∈ L\n by_cases on h2\n · -- Case 1. h2 : p = n\n rewrite [h2]\n show prime n from h1.left\n done\n · -- Case 2. h2 : p ∈ L\n show prime p from h1.right p h2\n done\n done\n done\n\nlemma nondec_nil : nondec [] := by\n define --Goal : True\n trivial --trivial proves some obviously true statements, such as True\n done\n\nlemma nondec_cons (n : Nat) (L : List Nat) :\n nondec (n :: L) ↔ (∀ m ∈ L, n ≤ m) ∧ nondec L := by rfl\n\nlemma prod_nil : prod [] = 1 := by rfl\n\nlemma prod_cons : prod (n :: L) = n * (prod L) := by rfl\nBefore we can prove the existence of prime factorizations, we will need one more fact: every member of a list of natural numbers divides the product of the list. The proof will be by induction on the length of the list, so we will need to know how to work with lengths of lists in Lean. If l is a list, then the length of l is List.length l, which can also be written more briefly as l.length. We’ll need a few more theorems about lists:\n\n@List.length_eq_zero : ∀ {α : Type u_1} {l : List α},\n List.length l = 0 ↔ l = []\n\n@List.length_cons : ∀ {α : Type u_1} (a : α) (as : List α),\n List.length (a :: as) = Nat.succ (List.length as)\n\n@List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α},\n l ≠ [] → ∃ (b : α) (L : List α), l = b :: L\n\nAnd we’ll need one more lemma, which follows from the three theorems above; we leave the proof as an exercise for you:\nlemma exists_cons_of_length_eq_succ {A : Type}\n {l : List A} {n : Nat} (h : l.length = n + 1) :\n ∃ (a : A) (L : List A), l = a :: L ∧ L.length = n := sorry\nWe can now prove that every member of a list of natural numbers divides the product of the list. After proving it by induction on the length of the list, we restate the lemma in a more convenient form.\nlemma list_elt_dvd_prod_by_length (a : Nat) : ∀ (n : Nat),\n ∀ (l : List Nat), l.length = n → a ∈ l → a ∣ prod l := by\n by_induc\n · --Base Case\n fix l : List Nat\n assume h1 : l.length = 0\n rewrite [List.length_eq_zero] at h1 --h1 : l = []\n rewrite [h1] --Goal : a ∈ [] → a ∣ prod []\n contrapos\n assume h2 : ¬a ∣ prod []\n show a ∉ [] from List.not_mem_nil a\n done\n · -- Induction Step\n fix n : Nat\n assume ih : ∀ (l : List Nat), List.length l = n → a ∈ l → a ∣ prod l\n fix l : List Nat\n assume h1 : l.length = n + 1 --Goal : a ∈ l → a ∣ prod l\n obtain (b : Nat) (h2 : ∃ (L : List Nat),\n l = b :: L ∧ L.length = n) from exists_cons_of_length_eq_succ h1\n obtain (L : List Nat) (h3 : l = b :: L ∧ L.length = n) from h2\n have h4 : a ∈ L → a ∣ prod L := ih L h3.right\n assume h5 : a ∈ l\n rewrite [h3.left, prod_cons] --Goal : a ∣ b * prod L\n rewrite [h3.left, List.mem_cons] at h5 --h5 : a = b ∨ a ∈ L\n by_cases on h5\n · -- Case 1. h5 : a = b\n apply Exists.intro (prod L)\n rewrite [h5]\n rfl\n done\n · -- Case 2. h5 : a ∈ L\n have h6 : a ∣ prod L := h4 h5\n have h7 : prod L ∣ b * prod L := by\n apply Exists.intro b\n ring\n done\n show a ∣ b * prod L from dvd_trans h6 h7\n done\n done\n done\n\nlemma list_elt_dvd_prod {a : Nat} {l : List Nat}\n (h : a ∈ l) : a ∣ prod l := by\n set n : Nat := l.length\n have h1 : l.length = n := by rfl\n show a ∣ prod l from list_elt_dvd_prod_by_length a n l h1 h\n done\nThe proof that every positive integer has a prime factorization is now long but straightforward.\nlemma exists_prime_factorization : ∀ (n : Nat), n ≥ 1 →\n ∃ (l : List Nat), prime_factorization n l := by\n by_strong_induc\n fix n : Nat\n assume ih : ∀ n_1 < n, n_1 ≥ 1 →\n ∃ (l : List Nat), prime_factorization n_1 l\n assume h1 : n ≥ 1\n by_cases h2 : n = 1\n · -- Case 1. h2 : n = 1\n apply Exists.intro []\n define\n apply And.intro\n · -- Proof of nondec_prime_list []\n define\n show all_prime [] ∧ nondec [] from\n And.intro all_prime_nil nondec_nil\n done\n · -- Proof of prod [] = n\n rewrite [prod_nil, h2]\n rfl\n done\n done\n · -- Case 2. h2 : n ≠ 1\n have h3 : n ≥ 2 := lt_of_le_of_ne' h1 h2\n obtain (p : Nat) (h4 : prime_factor p n ∧ ∀ (q : Nat),\n prime_factor q n → p ≤ q) from exists_least_prime_factor h3\n have p_prime_factor : prime_factor p n := h4.left\n define at p_prime_factor\n have p_prime : prime p := p_prime_factor.left\n have p_dvd_n : p ∣ n := p_prime_factor.right\n have p_least : ∀ (q : Nat), prime_factor q n → p ≤ q := h4.right\n obtain (m : Nat) (n_eq_pm : n = p * m) from p_dvd_n\n have h5 : m ≠ 0 := by\n contradict h1 with h6\n have h7 : n = 0 :=\n calc n\n _ = p * m := n_eq_pm\n _ = p * 0 := by rw [h6]\n _ = 0 := by ring\n rewrite [h7]\n decide\n done\n have m_pos : 0 < m := Nat.pos_of_ne_zero h5\n have m_lt_n : m < n := by\n define at p_prime\n show m < n from\n calc m\n _ < m + m := by linarith\n _ = 2 * m := by ring\n _ ≤ p * m := by rel [p_prime.left]\n _ = n := n_eq_pm.symm\n done\n obtain (L : List Nat) (h6 : prime_factorization m L)\n from ih m m_lt_n m_pos\n define at h6\n have ndpl_L : nondec_prime_list L := h6.left\n define at ndpl_L\n apply Exists.intro (p :: L)\n define\n apply And.intro\n · -- Proof of nondec_prime_list (p :: L)\n define\n apply And.intro\n · -- Proof of all_prime (p :: L)\n rewrite [all_prime_cons]\n show prime p ∧ all_prime L from And.intro p_prime ndpl_L.left\n done\n · -- Proof of nondec (p :: L)\n rewrite [nondec_cons]\n apply And.intro _ ndpl_L.right\n fix q : Nat\n assume q_in_L : q ∈ L\n have h7 : q ∣ prod L := list_elt_dvd_prod q_in_L\n rewrite [h6.right] at h7 --h7 : q ∣ m\n have h8 : m ∣ n := by\n apply Exists.intro p\n rewrite [n_eq_pm]\n ring\n done\n have q_dvd_n : q ∣ n := dvd_trans h7 h8\n have ap_L : all_prime L := ndpl_L.left\n define at ap_L\n have q_prime_factor : prime_factor q n :=\n And.intro (ap_L q q_in_L) q_dvd_n\n show p ≤ q from p_least q q_prime_factor\n done\n done\n · -- Proof of prod (p :: L) = n\n rewrite [prod_cons, h6.right, n_eq_pm]\n rfl\n done\n done\n done\nWe now turn to the proof that the prime factorization of a positive integer is unique. In preparation for that proof, HTPI defines two numbers to be relatively prime if their greatest common divisor is 1, and then it uses that concept to prove two theorems, 7.2.2 and 7.2.3. Here are similar proofs of those theorems in Lean, with the proof of one lemma left as an exercise. In the proof of Theorem 7.2.2, we begin, as we did in the proof of Theorem 7.1.6, by converting the goal from natural numbers to integers so that we can use integer algebra.\ndef rel_prime (a b : Nat) : Prop := gcd a b = 1\n\ntheorem Theorem_7_2_2 {a b c : Nat}\n (h1 : c ∣ a * b) (h2 : rel_prime a c) : c ∣ b := by\n rewrite [←Int.natCast_dvd_natCast] --Goal : ↑c ∣ ↑b\n define at h1; define at h2; define\n obtain (j : Nat) (h3 : a * b = c * j) from h1\n set s : Int := gcd_c1 a c\n set t : Int := gcd_c2 a c\n have h4 : s * ↑a + t * ↑c = ↑(gcd a c) := gcd_lin_comb c a\n rewrite [h2, Nat.cast_one] at h4 --h4 : s * ↑a + t * ↑c = (1 : Int)\n apply Exists.intro (s * ↑j + t * ↑b)\n show ↑b = ↑c * (s * ↑j + t * ↑b) from\n calc ↑b\n _ = (1 : Int) * ↑b := (one_mul _).symm\n _ = (s * ↑a + t * ↑c) * ↑b := by rw [h4]\n _ = s * (↑a * ↑b) + t * ↑c * ↑b := by ring\n _ = s * (↑c * ↑j) + t * ↑c * ↑b := by\n rw [←Nat.cast_mul a b, h3, Nat.cast_mul c j]\n _ = ↑c * (s * ↑j + t * ↑b) := by ring\n done\n\nlemma dvd_prime {a p : Nat}\n (h1 : prime p) (h2 : a ∣ p) : a = 1 ∨ a = p := sorry\n\nlemma rel_prime_of_prime_not_dvd {a p : Nat}\n (h1 : prime p) (h2 : ¬p ∣ a) : rel_prime a p := by\n have h3 : gcd a p ∣ a := gcd_dvd_left a p\n have h4 : gcd a p ∣ p := gcd_dvd_right a p\n have h5 : gcd a p = 1 ∨ gcd a p = p := dvd_prime h1 h4\n have h6 : gcd a p ≠ p := by\n contradict h2 with h6\n rewrite [h6] at h3\n show p ∣ a from h3\n done\n disj_syll h5 h6\n show rel_prime a p from h5\n done\n\ntheorem Theorem_7_2_3 {a b p : Nat}\n (h1 : prime p) (h2 : p ∣ a * b) : p ∣ a ∨ p ∣ b := by\n or_right with h3\n have h4 : rel_prime a p := rel_prime_of_prime_not_dvd h1 h3\n show p ∣ b from Theorem_7_2_2 h2 h4\n done\nTheorem 7.2.4 in HTPI extends Theorem 7.2.3 to show that if a prime number divides the product of a list of natural numbers, then it divides one of the numbers in the list. (Theorem 7.2.3 is the case of a list of length two.) The proof in HTPI is by induction on the length of the list, and we could use that method to prove the theorem in Lean. But look back at our proof of the lemma list_elt_dvd_prod_by_length, which also used induction on the length of a list. In the base case, we ended up proving that the nil list has the property stated in the lemma, and in the induction step we proved that if a list L has the property, then so does any list of the form b :: L. We could think of this as a kind of “induction on lists.” As we observed earlier, every list can be constructed by starting with the nil list and applying cons finitely many times. It follows that if the nil list has some property, and applying the cons operation to a list with the property produces another list with the property, then all lists have the property. (In fact, a similar principle was at work in our recursive definitions of nondec l and prod l.)\nLean has a theorem called List.rec that can be used to justify induction on lists. This is a little more convenient than induction on the length of a list, so we’ll use it to prove Theorem 7.2.4. The proof uses two lemmas, whose proofs we leave as exercises for you.\nlemma eq_one_of_dvd_one {n : Nat} (h : n ∣ 1) : n = 1 := sorry\n\nlemma prime_not_one {p : Nat} (h : prime p) : p ≠ 1 := sorry\n\ntheorem Theorem_7_2_4 {p : Nat} (h1 : prime p) :\n ∀ (l : List Nat), p ∣ prod l → ∃ a ∈ l, p ∣ a := by\n apply List.rec\n · -- Base Case. Goal : p ∣ prod [] → ∃ a ∈ [], p ∣ a\n rewrite [prod_nil]\n assume h2 : p ∣ 1\n show ∃ a ∈ [], p ∣ a from\n absurd (eq_one_of_dvd_one h2) (prime_not_one h1)\n done\n · -- Induction Step\n fix b : Nat\n fix L : List Nat\n assume ih : p ∣ prod L → ∃ a ∈ L, p ∣ a\n --Goal : p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a\n assume h2 : p ∣ prod (b :: L)\n rewrite [prod_cons] at h2\n have h3 : p ∣ b ∨ p ∣ prod L := Theorem_7_2_3 h1 h2\n by_cases on h3\n · -- Case 1. h3 : p ∣ b\n apply Exists.intro b\n show b ∈ b :: L ∧ p ∣ b from\n And.intro (List.mem_cons_self b L) h3\n done\n · -- Case 2. h3 : p ∣ prod L\n obtain (a : Nat) (h4 : a ∈ L ∧ p ∣ a) from ih h3\n apply Exists.intro a\n show a ∈ b :: L ∧ p ∣ a from\n And.intro (List.mem_cons_of_mem b h4.left) h4.right\n done\n done\n done\nIn Theorem 7.2.4, if all members of the list l are prime, then we can conclude not merely that p divides some member of l, but that p is one of the members.\nlemma prime_in_list {p : Nat} {l : List Nat}\n (h1 : prime p) (h2 : all_prime l) (h3 : p ∣ prod l) : p ∈ l := by\n obtain (a : Nat) (h4 : a ∈ l ∧ p ∣ a) from Theorem_7_2_4 h1 l h3\n define at h2\n have h5 : prime a := h2 a h4.left\n have h6 : p = 1 ∨ p = a := dvd_prime h5 h4.right\n disj_syll h6 (prime_not_one h1)\n rewrite [h6]\n show a ∈ l from h4.left\n done\nThe uniqueness of prime factorizations follows from Theorem 7.2.5 of HTPI, which says that if two nondecreasing lists of prime numbers have the same product, then the two lists must be the same. In HTPI, a key step in the proof of Theorem 7.2.5 is to show that if two nondecreasing lists of prime numbers have the same product, then the last entry of one list is less than or equal to the last entry of the other. In Lean, because of the way the cons operation works, it is easier to work with the first entries of the lists.\nlemma first_le_first {p q : Nat} {l m : List Nat}\n (h1 : nondec_prime_list (p :: l)) (h2 : nondec_prime_list (q :: m))\n (h3 : prod (p :: l) = prod (q :: m)) : p ≤ q := by\n define at h1; define at h2\n have h4 : q ∣ prod (p :: l) := by\n define\n apply Exists.intro (prod m)\n rewrite [←prod_cons]\n show prod (p :: l) = prod (q :: m) from h3\n done\n have h5 : all_prime (q :: m) := h2.left\n rewrite [all_prime_cons] at h5\n have h6 : q ∈ p :: l := prime_in_list h5.left h1.left h4\n have h7 : nondec (p :: l) := h1.right\n rewrite [nondec_cons] at h7\n rewrite [List.mem_cons] at h6\n by_cases on h6\n · -- Case 1. h6 : q = p\n linarith\n done\n · -- Case 2. h6 : q ∈ l\n have h8 : ∀ m ∈ l, p ≤ m := h7.left\n show p ≤ q from h8 q h6\n done\n done\nThe proof of Theorem 7.2.5 is another proof by induction on lists. It uses a few more lemmas whose proofs we leave as exercises.\nlemma nondec_prime_list_tail {p : Nat} {l : List Nat}\n (h : nondec_prime_list (p :: l)) : nondec_prime_list l := sorry\n\nlemma cons_prod_not_one {p : Nat} {l : List Nat}\n (h : nondec_prime_list (p :: l)) : prod (p :: l) ≠ 1 := sorry\n\nlemma list_nil_iff_prod_one {l : List Nat} (h : nondec_prime_list l) :\n l = [] ↔ prod l = 1 := sorry\n\nlemma prime_pos {p : Nat} (h : prime p) : p > 0 := sorry\n\ntheorem Theorem_7_2_5 : ∀ (l1 l2 : List Nat),\n nondec_prime_list l1 → nondec_prime_list l2 →\n prod l1 = prod l2 → l1 = l2 := by\n apply List.rec\n · -- Base Case. Goal : ∀ (l2 : List Nat), nondec_prime_list [] →\n -- nondec_prime_list l2 → prod [] = prod l2 → [] = l2\n fix l2 : List Nat\n assume h1 : nondec_prime_list []\n assume h2 : nondec_prime_list l2\n assume h3 : prod [] = prod l2\n rewrite [prod_nil, eq_comm, ←list_nil_iff_prod_one h2] at h3\n show [] = l2 from h3.symm\n done\n · -- Induction Step\n fix p : Nat\n fix L1 : List Nat\n assume ih : ∀ (L2 : List Nat), nondec_prime_list L1 →\n nondec_prime_list L2 → prod L1 = prod L2 → L1 = L2\n -- Goal : ∀ (l2 : List Nat), nondec_prime_list (p :: L1) →\n -- nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2\n fix l2 : List Nat\n assume h1 : nondec_prime_list (p :: L1)\n assume h2 : nondec_prime_list l2\n assume h3 : prod (p :: L1) = prod l2\n have h4 : ¬prod (p :: L1) = 1 := cons_prod_not_one h1\n rewrite [h3, ←list_nil_iff_prod_one h2] at h4\n obtain (q : Nat) (h5 : ∃ (L : List Nat), l2 = q :: L) from\n List.exists_cons_of_ne_nil h4\n obtain (L2 : List Nat) (h6 : l2 = q :: L2) from h5\n rewrite [h6] at h2 --h2 : nondec_prime_list (q :: L2)\n rewrite [h6] at h3 --h3 : prod (p :: L1) = prod (q :: L2)\n have h7 : p ≤ q := first_le_first h1 h2 h3\n have h8 : q ≤ p := first_le_first h2 h1 h3.symm\n have h9 : p = q := by linarith\n rewrite [h9, prod_cons, prod_cons] at h3\n --h3 : q * prod L1 = q * prod L2\n have h10 : nondec_prime_list L1 := nondec_prime_list_tail h1\n have h11 : nondec_prime_list L2 := nondec_prime_list_tail h2\n define at h2\n have h12 : all_prime (q :: L2) := h2.left\n rewrite [all_prime_cons] at h12\n have h13 : q > 0 := prime_pos h12.left\n have h14 : prod L1 = prod L2 := Nat.eq_of_mul_eq_mul_left h13 h3\n have h15 : L1 = L2 := ih L2 h10 h11 h14\n rewrite [h6, h9, h15]\n rfl\n done\n done\nPutting it all together, we can finally prove the fundamental theorem of arithmetic, which is stated as Theorem 7.2.6 in HTPI:\ntheorem fund_thm_arith (n : Nat) (h : n ≥ 1) :\n ∃! (l : List Nat), prime_factorization n l := by\n exists_unique\n · -- Existence\n show ∃ (l : List Nat), prime_factorization n l from\n exists_prime_factorization n h\n done\n · -- Uniqueness\n fix l1 : List Nat; fix l2 : List Nat\n assume h1 : prime_factorization n l1\n assume h2 : prime_factorization n l2\n define at h1; define at h2\n have h3 : prod l1 = n := h1.right\n rewrite [←h2.right] at h3\n show l1 = l2 from Theorem_7_2_5 l1 l2 h1.left h2.left h3\n done\n done\n\nExercises\n\nlemma dvd_prime {a p : Nat}\n (h1 : prime p) (h2 : a ∣ p) : a = 1 ∨ a = p := sorry\n\n\n--Hints: Start with apply List.rec.\n--You may find the theorem mul_ne_zero useful.\ntheorem prod_nonzero_nonzero : ∀ (l : List Nat),\n (∀ a ∈ l, a ≠ 0) → prod l ≠ 0 := sorry\n\n\ntheorem rel_prime_iff_no_common_factor (a b : Nat) :\n rel_prime a b ↔ ¬∃ (p : Nat), prime p ∧ p ∣ a ∧ p ∣ b := sorry\n\n\ntheorem rel_prime_symm {a b : Nat} (h : rel_prime a b) :\n rel_prime b a := sorry\n\n\nlemma in_prime_factorization_iff_prime_factor {a : Nat} {l : List Nat}\n (h1 : prime_factorization a l) (p : Nat) :\n p ∈ l ↔ prime_factor p a := sorry\n\n\ntheorem Exercise_7_2_5 {a b : Nat} {l m : List Nat}\n (h1 : prime_factorization a l) (h2 : prime_factorization b m) :\n rel_prime a b ↔ (¬∃ (p : Nat), p ∈ l ∧ p ∈ m) := sorry\n\n\ntheorem Exercise_7_2_6 (a b : Nat) :\n rel_prime a b ↔ ∃ (s t : Int), s * a + t * b = 1 := sorry\n\n\ntheorem Exercise_7_2_7 {a b a' b' : Nat}\n (h1 : rel_prime a b) (h2 : a' ∣ a) (h3 : b' ∣ b) :\n rel_prime a' b' := sorry\n\n\ntheorem Exercise_7_2_9 {a b j k : Nat}\n (h1 : gcd a b ≠ 0) (h2 : a = j * gcd a b) (h3 : b = k * gcd a b) :\n rel_prime j k := sorry\n\n\ntheorem Exercise_7_2_17a (a b c : Nat) :\n gcd a (b * c) ∣ gcd a b * gcd a c := sorry"
+ "text": "7.2. Prime Factorization\nA natural number \\(n\\) is said to be prime if it is at least 2 and it cannot be written as a product of two smaller natural numbers. Of course, we can write this definition in Lean.\ndef prime (n : Nat) : Prop :=\n 2 ≤ n ∧ ¬∃ (a b : Nat), a * b = n ∧ a < n ∧ b < n\nThe main goal of Section 7.2 of HTPI is to prove that every positive integer has a unique prime factorization; that is, it can be written in a unique way as the product of a nondecreasing list of prime numbers. To get started on this goal, we first prove that every number greater than or equal to 2 has a prime factor. We leave one lemma as an exercise for you (it is a natural-number version of Theorem_3_3_7).\ndef prime_factor (p n : Nat) : Prop := prime p ∧ p ∣ n\n\nlemma dvd_trans {a b c : Nat} (h1 : a ∣ b) (h2 : b ∣ c) : a ∣ c := sorry\n\nlemma exists_prime_factor : ∀ (n : Nat), 2 ≤ n →\n ∃ (p : Nat), prime_factor p n := by\n by_strong_induc\n fix n : Nat\n assume ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ (p : Nat), prime_factor p n_1\n assume h1 : 2 ≤ n\n by_cases h2 : prime n\n · -- Case 1. h2 : prime n\n apply Exists.intro n\n define --Goal : prime n ∧ n ∣ n\n show prime n ∧ n ∣ n from And.intro h2 (dvd_self n)\n done\n · -- Case 2. h2 : ¬prime n\n define at h2\n --h2 : ¬(2 ≤ n ∧ ¬∃ (a b : Nat), a * b = n ∧ a < n ∧ b < n)\n demorgan at h2\n disj_syll h2 h1\n obtain (a : Nat) (h3 : ∃ (b : Nat), a * b = n ∧ a < n ∧ b < n) from h2\n obtain (b : Nat) (h4 : a * b = n ∧ a < n ∧ b < n) from h3\n have h5 : 2 ≤ a := by\n by_contra h6\n have h7 : a ≤ 1 := by linarith\n have h8 : n ≤ b :=\n calc n\n _ = a * b := h4.left.symm\n _ ≤ 1 * b := by rel [h7]\n _ = b := by ring\n linarith --n ≤ b contradicts b < n\n done\n have h6 : ∃ (p : Nat), prime_factor p a := ih a h4.right.left h5\n obtain (p : Nat) (h7 : prime_factor p a) from h6\n apply Exists.intro p\n define --Goal : prime p ∧ p ∣ n\n define at h7 --h7 : prime p ∧ p ∣ a\n apply And.intro h7.left\n have h8 : a ∣ n := by\n apply Exists.intro b\n show n = a * b from (h4.left).symm\n done\n show p ∣ n from dvd_trans h7.right h8\n done\n done\nOf course, by the well-ordering principle, an immediate consequence of this lemma is that every number greater than or equal to 2 has a smallest prime factor.\nlemma exists_least_prime_factor {n : Nat} (h : 2 ≤ n) :\n ∃ (p : Nat), prime_factor p n ∧\n ∀ (q : Nat), prime_factor q n → p ≤ q := by\n set S : Set Nat := {p : Nat | prime_factor p n}\n have h2 : ∃ (p : Nat), p ∈ S := exists_prime_factor n h\n show ∃ (p : Nat), prime_factor p n ∧\n ∀ (q : Nat), prime_factor q n → p ≤ q from well_ord_princ S h2\n done\nTo talk about prime factorizations of positive integers, we’ll need to introduce a new type. If U is any type, then List U is the type of lists of objects of type U. Such a list is written in square brackets, with the entries separated by commas. For example, [3, 7, 1] has type List Nat. The notation [] denotes the empty list, and if a has type U and l has type List U, then a :: l denotes the list consisting of a followed by the entries of l. The empty list is sometimes called the nil list, and the operation of constructing a list a :: l from a and l is called cons (short for construct). Every list can be constructed by applying the cons operation repeatedly, starting with the nil list. For example,\n\n[3, 7, 1] = 3 :: [7, 1] = 3 :: (7 :: [1]) = 3 :: (7 :: (1 :: [])).\n\nIf l has type List U and a has type U, then a ∈ l means that a is one of the entries in the list l. For example, 7 ∈ [3, 7, 1]. Lean knows several theorems about this notation:\n\n@List.not_mem_nil : ∀ {α : Type u_1} (a : α),\n a ∉ []\n\n@List.mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α},\n a ∈ b :: l ↔ a = b ∨ a ∈ l\n\n@List.mem_cons_self : ∀ {α : Type u_1} (a : α) (l : List α),\n a ∈ a :: l\n\n@List.mem_cons_of_mem : ∀ {α : Type u_1} (y : α) {a : α} {l : List α},\n a ∈ l → a ∈ y :: l\n\nThe first two theorems give the conditions under which something is a member of the nil list or a list constructed by cons, and the last two are easy consequences of the second.\nTo define prime factorizations, we must define several concepts first. Some of these concepts are most easily defined recursively.\ndef all_prime (l : List Nat) : Prop := ∀ p ∈ l, prime p\n\ndef nondec (l : List Nat) : Prop :=\n match l with\n | [] => True --Of course, True is a proposition that is always true\n | n :: L => (∀ m ∈ L, n ≤ m) ∧ nondec L\n\ndef nondec_prime_list (l : List Nat) : Prop := all_prime l ∧ nondec l\n\ndef prod (l : List Nat) : Nat :=\n match l with\n | [] => 1\n | n :: L => n * (prod L)\n\ndef prime_factorization (n : Nat) (l : List Nat) : Prop :=\n nondec_prime_list l ∧ prod l = n\nAccording to these definitions, all_prime l means that every member of the list l is prime, nondec l means that every member of l is less than or equal to all later members, prod l is the product of all members of l, and prime_factorization n l means that l is a nondecreasing list of prime numbers whose product is n. It will be convenient to spell out some consequences of these definitions in several lemmas:\nlemma all_prime_nil : all_prime [] := by\n define --Goal : ∀ p ∈ [], prime p\n fix p : Nat\n contrapos --Goal : ¬prime p → p ∉ []\n assume h1 : ¬prime p\n show p ∉ [] from List.not_mem_nil p\n done\n\nlemma all_prime_cons (n : Nat) (L : List Nat) :\n all_prime (n :: L) ↔ prime n ∧ all_prime L := by\n apply Iff.intro\n · -- (→)\n assume h1 : all_prime (n :: L) --Goal : prime n ∧ all_prime L\n define at h1 --h1 : ∀ p ∈ n :: L, prime p\n apply And.intro (h1 n (List.mem_cons_self n L))\n define --Goal : ∀ p ∈ L, prime p\n fix p : Nat\n assume h2 : p ∈ L\n show prime p from h1 p (List.mem_cons_of_mem n h2)\n done\n · -- (←)\n assume h1 : prime n ∧ all_prime L --Goal : all_prime (n :: l)\n define : all_prime L at h1\n define\n fix p : Nat\n assume h2 : p ∈ n :: L\n rewrite [List.mem_cons] at h2 --h2 : p = n ∨ p ∈ L\n by_cases on h2\n · -- Case 1. h2 : p = n\n rewrite [h2]\n show prime n from h1.left\n done\n · -- Case 2. h2 : p ∈ L\n show prime p from h1.right p h2\n done\n done\n done\n\nlemma nondec_nil : nondec [] := by\n define --Goal : True\n trivial --trivial proves some obviously true statements, such as True\n done\n\nlemma nondec_cons (n : Nat) (L : List Nat) :\n nondec (n :: L) ↔ (∀ m ∈ L, n ≤ m) ∧ nondec L := by rfl\n\nlemma prod_nil : prod [] = 1 := by rfl\n\nlemma prod_cons : prod (n :: L) = n * (prod L) := by rfl\nBefore we can prove the existence of prime factorizations, we will need one more fact: every member of a list of natural numbers divides the product of the list. The proof will be by induction on the length of the list, so we will need to know how to work with lengths of lists in Lean. If l is a list, then the length of l is List.length l, which can also be written more briefly as l.length. We’ll need a few more theorems about lists:\n\n@List.length_eq_zero : ∀ {α : Type u_1} {l : List α},\n l.length = 0 ↔ l = []\n\n@List.length_cons : ∀ {α : Type u_1} (a : α) (as : List α),\n (a :: as).length = as.length + 1\n\n@List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α},\n l ≠ [] → ∃ (b : α) (L : List α), l = b :: L\n\nAnd we’ll need one more lemma, which follows from the three theorems above; we leave the proof as an exercise for you:\nlemma exists_cons_of_length_eq_succ {A : Type}\n {l : List A} {n : Nat} (h : l.length = n + 1) :\n ∃ (a : A) (L : List A), l = a :: L ∧ L.length = n := sorry\nWe can now prove that every member of a list of natural numbers divides the product of the list. After proving it by induction on the length of the list, we restate the lemma in a more convenient form.\nlemma list_elt_dvd_prod_by_length (a : Nat) : ∀ (n : Nat),\n ∀ (l : List Nat), l.length = n → a ∈ l → a ∣ prod l := by\n by_induc\n · --Base Case\n fix l : List Nat\n assume h1 : l.length = 0\n rewrite [List.length_eq_zero] at h1 --h1 : l = []\n rewrite [h1] --Goal : a ∈ [] → a ∣ prod []\n contrapos\n assume h2 : ¬a ∣ prod []\n show a ∉ [] from List.not_mem_nil a\n done\n · -- Induction Step\n fix n : Nat\n assume ih : ∀ (l : List Nat), l.length = n → a ∈ l → a ∣ prod l\n fix l : List Nat\n assume h1 : l.length = n + 1 --Goal : a ∈ l → a ∣ prod l\n obtain (b : Nat) (h2 : ∃ (L : List Nat),\n l = b :: L ∧ L.length = n) from exists_cons_of_length_eq_succ h1\n obtain (L : List Nat) (h3 : l = b :: L ∧ L.length = n) from h2\n have h4 : a ∈ L → a ∣ prod L := ih L h3.right\n assume h5 : a ∈ l\n rewrite [h3.left, prod_cons] --Goal : a ∣ b * prod L\n rewrite [h3.left, List.mem_cons] at h5 --h5 : a = b ∨ a ∈ L\n by_cases on h5\n · -- Case 1. h5 : a = b\n apply Exists.intro (prod L)\n rewrite [h5]\n rfl\n done\n · -- Case 2. h5 : a ∈ L\n have h6 : a ∣ prod L := h4 h5\n have h7 : prod L ∣ b * prod L := by\n apply Exists.intro b\n ring\n done\n show a ∣ b * prod L from dvd_trans h6 h7\n done\n done\n done\n\nlemma list_elt_dvd_prod {a : Nat} {l : List Nat}\n (h : a ∈ l) : a ∣ prod l := by\n set n : Nat := l.length\n have h1 : l.length = n := by rfl\n show a ∣ prod l from list_elt_dvd_prod_by_length a n l h1 h\n done\nThe proof that every positive integer has a prime factorization is now long but straightforward.\nlemma exists_prime_factorization : ∀ (n : Nat), n ≥ 1 →\n ∃ (l : List Nat), prime_factorization n l := by\n by_strong_induc\n fix n : Nat\n assume ih : ∀ n_1 < n, n_1 ≥ 1 →\n ∃ (l : List Nat), prime_factorization n_1 l\n assume h1 : n ≥ 1\n by_cases h2 : n = 1\n · -- Case 1. h2 : n = 1\n apply Exists.intro []\n define\n apply And.intro\n · -- Proof of nondec_prime_list []\n define\n show all_prime [] ∧ nondec [] from\n And.intro all_prime_nil nondec_nil\n done\n · -- Proof of prod [] = n\n rewrite [prod_nil, h2]\n rfl\n done\n done\n · -- Case 2. h2 : n ≠ 1\n have h3 : n ≥ 2 := lt_of_le_of_ne' h1 h2\n obtain (p : Nat) (h4 : prime_factor p n ∧ ∀ (q : Nat),\n prime_factor q n → p ≤ q) from exists_least_prime_factor h3\n have p_prime_factor : prime_factor p n := h4.left\n define at p_prime_factor\n have p_prime : prime p := p_prime_factor.left\n have p_dvd_n : p ∣ n := p_prime_factor.right\n have p_least : ∀ (q : Nat), prime_factor q n → p ≤ q := h4.right\n obtain (m : Nat) (n_eq_pm : n = p * m) from p_dvd_n\n have h5 : m ≠ 0 := by\n contradict h1 with h6\n have h7 : n = 0 :=\n calc n\n _ = p * m := n_eq_pm\n _ = p * 0 := by rw [h6]\n _ = 0 := by ring\n rewrite [h7]\n decide\n done\n have m_pos : 0 < m := Nat.pos_of_ne_zero h5\n have m_lt_n : m < n := by\n define at p_prime\n show m < n from\n calc m\n _ < m + m := by linarith\n _ = 2 * m := by ring\n _ ≤ p * m := by rel [p_prime.left]\n _ = n := n_eq_pm.symm\n done\n obtain (L : List Nat) (h6 : prime_factorization m L)\n from ih m m_lt_n m_pos\n define at h6\n have ndpl_L : nondec_prime_list L := h6.left\n define at ndpl_L\n apply Exists.intro (p :: L)\n define\n apply And.intro\n · -- Proof of nondec_prime_list (p :: L)\n define\n apply And.intro\n · -- Proof of all_prime (p :: L)\n rewrite [all_prime_cons]\n show prime p ∧ all_prime L from And.intro p_prime ndpl_L.left\n done\n · -- Proof of nondec (p :: L)\n rewrite [nondec_cons]\n apply And.intro _ ndpl_L.right\n fix q : Nat\n assume q_in_L : q ∈ L\n have h7 : q ∣ prod L := list_elt_dvd_prod q_in_L\n rewrite [h6.right] at h7 --h7 : q ∣ m\n have h8 : m ∣ n := by\n apply Exists.intro p\n rewrite [n_eq_pm]\n ring\n done\n have q_dvd_n : q ∣ n := dvd_trans h7 h8\n have ap_L : all_prime L := ndpl_L.left\n define at ap_L\n have q_prime_factor : prime_factor q n :=\n And.intro (ap_L q q_in_L) q_dvd_n\n show p ≤ q from p_least q q_prime_factor\n done\n done\n · -- Proof of prod (p :: L) = n\n rewrite [prod_cons, h6.right, n_eq_pm]\n rfl\n done\n done\n done\nWe now turn to the proof that the prime factorization of a positive integer is unique. In preparation for that proof, HTPI defines two numbers to be relatively prime if their greatest common divisor is 1, and then it uses that concept to prove two theorems, 7.2.2 and 7.2.3. Here are similar proofs of those theorems in Lean, with the proof of one lemma left as an exercise. In the proof of Theorem 7.2.2, we begin, as we did in the proof of Theorem 7.1.6, by converting the goal from natural numbers to integers so that we can use integer algebra.\ndef rel_prime (a b : Nat) : Prop := gcd a b = 1\n\ntheorem Theorem_7_2_2 {a b c : Nat}\n (h1 : c ∣ a * b) (h2 : rel_prime a c) : c ∣ b := by\n rewrite [←Int.natCast_dvd_natCast] --Goal : ↑c ∣ ↑b\n define at h1; define at h2; define\n obtain (j : Nat) (h3 : a * b = c * j) from h1\n set s : Int := gcd_c1 a c\n set t : Int := gcd_c2 a c\n have h4 : s * ↑a + t * ↑c = ↑(gcd a c) := gcd_lin_comb c a\n rewrite [h2, Nat.cast_one] at h4 --h4 : s * ↑a + t * ↑c = (1 : Int)\n apply Exists.intro (s * ↑j + t * ↑b)\n show ↑b = ↑c * (s * ↑j + t * ↑b) from\n calc ↑b\n _ = (1 : Int) * ↑b := (one_mul _).symm\n _ = (s * ↑a + t * ↑c) * ↑b := by rw [h4]\n _ = s * (↑a * ↑b) + t * ↑c * ↑b := by ring\n _ = s * (↑c * ↑j) + t * ↑c * ↑b := by\n rw [←Nat.cast_mul a b, h3, Nat.cast_mul c j]\n _ = ↑c * (s * ↑j + t * ↑b) := by ring\n done\n\nlemma dvd_prime {a p : Nat}\n (h1 : prime p) (h2 : a ∣ p) : a = 1 ∨ a = p := sorry\n\nlemma rel_prime_of_prime_not_dvd {a p : Nat}\n (h1 : prime p) (h2 : ¬p ∣ a) : rel_prime a p := by\n have h3 : gcd a p ∣ a := gcd_dvd_left a p\n have h4 : gcd a p ∣ p := gcd_dvd_right a p\n have h5 : gcd a p = 1 ∨ gcd a p = p := dvd_prime h1 h4\n have h6 : gcd a p ≠ p := by\n contradict h2 with h6\n rewrite [h6] at h3\n show p ∣ a from h3\n done\n disj_syll h5 h6\n show rel_prime a p from h5\n done\n\ntheorem Theorem_7_2_3 {a b p : Nat}\n (h1 : prime p) (h2 : p ∣ a * b) : p ∣ a ∨ p ∣ b := by\n or_right with h3\n have h4 : rel_prime a p := rel_prime_of_prime_not_dvd h1 h3\n show p ∣ b from Theorem_7_2_2 h2 h4\n done\nTheorem 7.2.4 in HTPI extends Theorem 7.2.3 to show that if a prime number divides the product of a list of natural numbers, then it divides one of the numbers in the list. (Theorem 7.2.3 is the case of a list of length two.) The proof in HTPI is by induction on the length of the list, and we could use that method to prove the theorem in Lean. But look back at our proof of the lemma list_elt_dvd_prod_by_length, which also used induction on the length of a list. In the base case, we ended up proving that the nil list has the property stated in the lemma, and in the induction step we proved that if a list L has the property, then so does any list of the form b :: L. We could think of this as a kind of “induction on lists.” As we observed earlier, every list can be constructed by starting with the nil list and applying cons finitely many times. It follows that if the nil list has some property, and applying the cons operation to a list with the property produces another list with the property, then all lists have the property. (In fact, a similar principle was at work in our recursive definitions of nondec l and prod l.)\nLean has a theorem called List.rec that can be used to justify induction on lists. This is a little more convenient than induction on the length of a list, so we’ll use it to prove Theorem 7.2.4. The proof uses two lemmas, whose proofs we leave as exercises for you.\nlemma eq_one_of_dvd_one {n : Nat} (h : n ∣ 1) : n = 1 := sorry\n\nlemma prime_not_one {p : Nat} (h : prime p) : p ≠ 1 := sorry\n\ntheorem Theorem_7_2_4 {p : Nat} (h1 : prime p) :\n ∀ (l : List Nat), p ∣ prod l → ∃ a ∈ l, p ∣ a := by\n apply List.rec\n · -- Base Case. Goal : p ∣ prod [] → ∃ a ∈ [], p ∣ a\n rewrite [prod_nil]\n assume h2 : p ∣ 1\n show ∃ a ∈ [], p ∣ a from\n absurd (eq_one_of_dvd_one h2) (prime_not_one h1)\n done\n · -- Induction Step\n fix b : Nat\n fix L : List Nat\n assume ih : p ∣ prod L → ∃ a ∈ L, p ∣ a\n --Goal : p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a\n assume h2 : p ∣ prod (b :: L)\n rewrite [prod_cons] at h2\n have h3 : p ∣ b ∨ p ∣ prod L := Theorem_7_2_3 h1 h2\n by_cases on h3\n · -- Case 1. h3 : p ∣ b\n apply Exists.intro b\n show b ∈ b :: L ∧ p ∣ b from\n And.intro (List.mem_cons_self b L) h3\n done\n · -- Case 2. h3 : p ∣ prod L\n obtain (a : Nat) (h4 : a ∈ L ∧ p ∣ a) from ih h3\n apply Exists.intro a\n show a ∈ b :: L ∧ p ∣ a from\n And.intro (List.mem_cons_of_mem b h4.left) h4.right\n done\n done\n done\nIn Theorem 7.2.4, if all members of the list l are prime, then we can conclude not merely that p divides some member of l, but that p is one of the members.\nlemma prime_in_list {p : Nat} {l : List Nat}\n (h1 : prime p) (h2 : all_prime l) (h3 : p ∣ prod l) : p ∈ l := by\n obtain (a : Nat) (h4 : a ∈ l ∧ p ∣ a) from Theorem_7_2_4 h1 l h3\n define at h2\n have h5 : prime a := h2 a h4.left\n have h6 : p = 1 ∨ p = a := dvd_prime h5 h4.right\n disj_syll h6 (prime_not_one h1)\n rewrite [h6]\n show a ∈ l from h4.left\n done\nThe uniqueness of prime factorizations follows from Theorem 7.2.5 of HTPI, which says that if two nondecreasing lists of prime numbers have the same product, then the two lists must be the same. In HTPI, a key step in the proof of Theorem 7.2.5 is to show that if two nondecreasing lists of prime numbers have the same product, then the last entry of one list is less than or equal to the last entry of the other. In Lean, because of the way the cons operation works, it is easier to work with the first entries of the lists.\nlemma first_le_first {p q : Nat} {l m : List Nat}\n (h1 : nondec_prime_list (p :: l)) (h2 : nondec_prime_list (q :: m))\n (h3 : prod (p :: l) = prod (q :: m)) : p ≤ q := by\n define at h1; define at h2\n have h4 : q ∣ prod (p :: l) := by\n define\n apply Exists.intro (prod m)\n rewrite [←prod_cons]\n show prod (p :: l) = prod (q :: m) from h3\n done\n have h5 : all_prime (q :: m) := h2.left\n rewrite [all_prime_cons] at h5\n have h6 : q ∈ p :: l := prime_in_list h5.left h1.left h4\n have h7 : nondec (p :: l) := h1.right\n rewrite [nondec_cons] at h7\n rewrite [List.mem_cons] at h6\n by_cases on h6\n · -- Case 1. h6 : q = p\n linarith\n done\n · -- Case 2. h6 : q ∈ l\n have h8 : ∀ m ∈ l, p ≤ m := h7.left\n show p ≤ q from h8 q h6\n done\n done\nThe proof of Theorem 7.2.5 is another proof by induction on lists. It uses a few more lemmas whose proofs we leave as exercises.\nlemma nondec_prime_list_tail {p : Nat} {l : List Nat}\n (h : nondec_prime_list (p :: l)) : nondec_prime_list l := sorry\n\nlemma cons_prod_not_one {p : Nat} {l : List Nat}\n (h : nondec_prime_list (p :: l)) : prod (p :: l) ≠ 1 := sorry\n\nlemma list_nil_iff_prod_one {l : List Nat} (h : nondec_prime_list l) :\n l = [] ↔ prod l = 1 := sorry\n\nlemma prime_pos {p : Nat} (h : prime p) : p > 0 := sorry\n\ntheorem Theorem_7_2_5 : ∀ (l1 l2 : List Nat),\n nondec_prime_list l1 → nondec_prime_list l2 →\n prod l1 = prod l2 → l1 = l2 := by\n apply List.rec\n · -- Base Case. Goal : ∀ (l2 : List Nat), nondec_prime_list [] →\n -- nondec_prime_list l2 → prod [] = prod l2 → [] = l2\n fix l2 : List Nat\n assume h1 : nondec_prime_list []\n assume h2 : nondec_prime_list l2\n assume h3 : prod [] = prod l2\n rewrite [prod_nil, eq_comm, ←list_nil_iff_prod_one h2] at h3\n show [] = l2 from h3.symm\n done\n · -- Induction Step\n fix p : Nat\n fix L1 : List Nat\n assume ih : ∀ (L2 : List Nat), nondec_prime_list L1 →\n nondec_prime_list L2 → prod L1 = prod L2 → L1 = L2\n -- Goal : ∀ (l2 : List Nat), nondec_prime_list (p :: L1) →\n -- nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2\n fix l2 : List Nat\n assume h1 : nondec_prime_list (p :: L1)\n assume h2 : nondec_prime_list l2\n assume h3 : prod (p :: L1) = prod l2\n have h4 : ¬prod (p :: L1) = 1 := cons_prod_not_one h1\n rewrite [h3, ←list_nil_iff_prod_one h2] at h4\n obtain (q : Nat) (h5 : ∃ (L : List Nat), l2 = q :: L) from\n List.exists_cons_of_ne_nil h4\n obtain (L2 : List Nat) (h6 : l2 = q :: L2) from h5\n rewrite [h6] at h2 --h2 : nondec_prime_list (q :: L2)\n rewrite [h6] at h3 --h3 : prod (p :: L1) = prod (q :: L2)\n have h7 : p ≤ q := first_le_first h1 h2 h3\n have h8 : q ≤ p := first_le_first h2 h1 h3.symm\n have h9 : p = q := by linarith\n rewrite [h9, prod_cons, prod_cons] at h3\n --h3 : q * prod L1 = q * prod L2\n have h10 : nondec_prime_list L1 := nondec_prime_list_tail h1\n have h11 : nondec_prime_list L2 := nondec_prime_list_tail h2\n define at h2\n have h12 : all_prime (q :: L2) := h2.left\n rewrite [all_prime_cons] at h12\n have h13 : q > 0 := prime_pos h12.left\n have h14 : prod L1 = prod L2 := Nat.eq_of_mul_eq_mul_left h13 h3\n have h15 : L1 = L2 := ih L2 h10 h11 h14\n rewrite [h6, h9, h15]\n rfl\n done\n done\nPutting it all together, we can finally prove the fundamental theorem of arithmetic, which is stated as Theorem 7.2.6 in HTPI:\ntheorem fund_thm_arith (n : Nat) (h : n ≥ 1) :\n ∃! (l : List Nat), prime_factorization n l := by\n exists_unique\n · -- Existence\n show ∃ (l : List Nat), prime_factorization n l from\n exists_prime_factorization n h\n done\n · -- Uniqueness\n fix l1 : List Nat; fix l2 : List Nat\n assume h1 : prime_factorization n l1\n assume h2 : prime_factorization n l2\n define at h1; define at h2\n have h3 : prod l1 = n := h1.right\n rewrite [←h2.right] at h3\n show l1 = l2 from Theorem_7_2_5 l1 l2 h1.left h2.left h3\n done\n done\n\nExercises\n\nlemma dvd_prime {a p : Nat}\n (h1 : prime p) (h2 : a ∣ p) : a = 1 ∨ a = p := sorry\n\n\n--Hints: Start with apply List.rec.\n--You may find the theorem mul_ne_zero useful.\ntheorem prod_nonzero_nonzero : ∀ (l : List Nat),\n (∀ a ∈ l, a ≠ 0) → prod l ≠ 0 := sorry\n\n\ntheorem rel_prime_iff_no_common_factor (a b : Nat) :\n rel_prime a b ↔ ¬∃ (p : Nat), prime p ∧ p ∣ a ∧ p ∣ b := sorry\n\n\ntheorem rel_prime_symm {a b : Nat} (h : rel_prime a b) :\n rel_prime b a := sorry\n\n\nlemma in_prime_factorization_iff_prime_factor {a : Nat} {l : List Nat}\n (h1 : prime_factorization a l) (p : Nat) :\n p ∈ l ↔ prime_factor p a := sorry\n\n\ntheorem Exercise_7_2_5 {a b : Nat} {l m : List Nat}\n (h1 : prime_factorization a l) (h2 : prime_factorization b m) :\n rel_prime a b ↔ (¬∃ (p : Nat), p ∈ l ∧ p ∈ m) := sorry\n\n\ntheorem Exercise_7_2_6 (a b : Nat) :\n rel_prime a b ↔ ∃ (s t : Int), s * a + t * b = 1 := sorry\n\n\ntheorem Exercise_7_2_7 {a b a' b' : Nat}\n (h1 : rel_prime a b) (h2 : a' ∣ a) (h3 : b' ∣ b) :\n rel_prime a' b' := sorry\n\n\ntheorem Exercise_7_2_9 {a b j k : Nat}\n (h1 : gcd a b ≠ 0) (h2 : a = j * gcd a b) (h3 : b = k * gcd a b) :\n rel_prime j k := sorry\n\n\ntheorem Exercise_7_2_17a (a b c : Nat) :\n gcd a (b * c) ∣ gcd a b * gcd a c := sorry"
},
{
"objectID": "Chap7.html#modular-arithmetic",
@@ -347,7 +347,7 @@
"href": "Chap8.html#countable-and-uncountable-sets",
"title": "8 Infinite Sets",
"section": "8.2. Countable and Uncountable Sets",
- "text": "8.2. Countable and Uncountable Sets\nSection 8.2 of HTPI shows that many set-theoretic operations, when applied to countable sets, produce results that are countable. For example, the first part of Theorem 8.2.1 shows that a Cartesian product of countable sets is countable. Our proof of this statement in Lean is based on Theorem_8_1_2_1 and the countability of Univ (Nat × Nat). We also use an exercise from Section 8.1.\ntheorem Exercise_8_1_17 {U : Type} {A B : Set U}\n (h1 : B ⊆ A) (h2 : ctble A) : ctble B := sorry\n\ntheorem Theorem_8_2_1_1 {U V : Type} {A : Set U} {B : Set V}\n (h1 : ctble A) (h2 : ctble B) : ctble (A ×ₛ B) := by\n rewrite [ctble_iff_equinum_set_nat] at h1\n rewrite [ctble_iff_equinum_set_nat] at h2\n obtain (I : Set Nat) (h3 : I ∼ A) from h1\n obtain (J : Set Nat) (h4 : J ∼ B) from h2\n have h5 : I ×ₛ J ∼ A ×ₛ B := Theorem_8_1_2_1 h3 h4\n have h6 : I ×ₛ J ⊆ Univ (Nat × Nat) := by\n fix p : Nat × Nat\n assume h6 : p ∈ I ×ₛ J\n show p ∈ Univ (Nat × Nat) from elt_Univ p\n done\n have h7 : ctble (Univ (Nat × Nat)) := by\n define --Goal : finite (Univ (Nat × Nat)) ∨ denum (Univ (Nat × Nat))\n apply Or.inr\n rewrite [denum_def]\n show Univ Nat ∼ Univ (Nat × Nat) from Theorem_8_1_3_2 NxN_equinum_N\n done\n have h8 : ctble (I ×ₛ J) := Exercise_8_1_17 h6 h7\n show ctble (A ×ₛ B) from ctble_of_equinum_ctble h5 h8\n done\nThe second part of Theorem 8.2.1 shows that a union of two countable sets is countable, but, as we ask you to show in the exercises, it is superseded by Theorem 8.2.2, which says that a union of a countable family of countable sets is countable. So we will skip ahead to Theorem 8.2.2. Here’s how we state the theorem in Lean:\ntheorem Theorem_8_2_2 {U : Type} {F : Set (Set U)}\n (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) : ctble (⋃₀ F)\nIn our proof, we will use the characterization of countability from Theorem_8_1_5_2. Thus, we will use the hypotheses h1 and h2 to conclude that there is a relation R : Rel Nat (Set U) such that fcnl_onto_from_nat R F, and also that for each A ∈ F there is a relation SA : Rel Nat U such that fcnl_onto_from_nat SA A. We begin by proving an easier version of the theorem, where we assume that we have a function f : Set U → Rel Nat U that supplies, for each A ∈ F, the required relation SA. Imitating the proof in HTPI, we can use R and f to construct the relation needed to prove that ⋃₀ F is countable.\ndef enum_union_fam {U : Type}\n (F : Set (Set U)) (f : Set U → Rel Nat U) (R : Rel Nat (Set U))\n (n : Nat) (a : U) : Prop := ∃ (p : Nat × Nat), fnnn p = n ∧\n ∃ A ∈ F, R p.1 A ∧ (f A) p.2 a\n\nlemma Lemma_8_2_2_1 {U : Type} {F : Set (Set U)} {f : Set U → Rel Nat U}\n (h1 : ctble F) (h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A) :\n ctble (⋃₀ F) := by\n rewrite [Theorem_8_1_5_2] at h1\n rewrite [Theorem_8_1_5_2]\n obtain (R : Rel Nat (Set U)) (h3 : fcnl_onto_from_nat R F) from h1\n define at h3\n have Runiqueval : unique_val_on_N R := h3.left\n have Ronto : nat_rel_onto R F := h3.right\n set S : Rel Nat U := enum_union_fam F f R\n apply Exists.intro S\n define\n apply And.intro\n · -- Proof of unique_val_on_N S\n define\n fix n : Nat; fix a1 : U; fix a2 : U\n assume Sna1 : S n a1\n assume Sna2 : S n a2 --Goal : a1 = a2\n define at Sna1; define at Sna2\n obtain ((i1, j1) : Nat × Nat) (h4 : fnnn (i1, j1) = n ∧\n ∃ A ∈ F, R i1 A ∧ f A j1 a1) from Sna1\n obtain (A1 : Set U) (Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1)\n from h4.right\n obtain ((i2, j2) : Nat × Nat) (h5 : fnnn (i2, j2) = n ∧\n ∃ A ∈ F, R i2 A ∧ f A j2 a2) from Sna2\n obtain (A2 : Set U) (Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2)\n from h5.right\n rewrite [←h5.left] at h4\n have h6 : (i1, j1) = (i2, j2) :=\n fnnn_one_one (i1, j1) (i2, j2) h4.left\n have h7 : i1 = i2 ∧ j1 = j2 := Prod.mk.inj h6\n rewrite [h7.left, h7.right] at Aija1\n --Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1\n define at Runiqueval\n have h8 : A1 = A2 := Runiqueval Aija1.right.left Aija2.right.left\n rewrite [h8] at Aija1 --Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1\n have fA2fcnlonto : fcnl_onto_from_nat (f A2) A2 := h2 A2 Aija2.left\n define at fA2fcnlonto\n have fA2uniqueval : unique_val_on_N (f A2) := fA2fcnlonto.left\n define at fA2uniqueval\n show a1 = a2 from fA2uniqueval Aija1.right.right Aija2.right.right\n done\n · -- Proof of nat_rel_onto S (⋃₀ F)\n define\n fix x : U\n assume h4 : x ∈ ⋃₀ F --Goal : ∃ (n : Nat), S n x\n define at h4\n obtain (A : Set U) (h5 : A ∈ F ∧ x ∈ A) from h4\n define at Ronto\n obtain (i : Nat) (h6 : R i A) from Ronto h5.left\n have fAfcnlonto : fcnl_onto_from_nat (f A) A := h2 A h5.left\n define at fAfcnlonto\n have fAonto : nat_rel_onto (f A) A := fAfcnlonto.right\n define at fAonto\n obtain (j : Nat) (h7 : f A j x) from fAonto h5.right\n apply Exists.intro (fnnn (i, j))\n define --Goal : ∃ (p : Nat × Nat), fnnn p = fnnn (i, j) ∧\n -- ∃ A ∈ F, R p.1 A ∧ f A p.2 x\n apply Exists.intro (i, j)\n apply And.intro\n · -- Proof that fnnn (i, j) = fnnn (i, j)\n rfl\n done\n · -- Proof that ∃ A ∈ F, R (i, j).1 A ∧ f A (i, j).2 x\n apply Exists.intro A\n show A ∈ F ∧ R (i, j).1 A ∧ f A (i, j).2 x from\n And.intro h5.left (And.intro h6 h7)\n done\n done\n done\nHow can we use Lemma_8_2_2_1 to prove Theorem_8_2_2? We must use the hypothesis h2 : ∀ A ∈ F, ctble A in Theorem_8_2_2 to produce the function f required in Lemma_8_2_2_1. As we have already observed, Theorem_8_1_5_2 guarantees that for each A ∈ F, an appropriate relation SA : Rel Nat U exists. We need a function f that will choose such a relation SA for each A. A function with this property is often called a choice function. And now we come to a delicate point that was skipped over in HTPI: to prove the existence of a choice function, we must use a statement called the axiom of choice.1\nThe distinction between the existence of an appropriate relation SA for each A and the existence of a function that chooses such a relation for each A is a subtle one. Perhaps for this reason, many people find the axiom of choice to be intuitively obvious. HTPI took advantage of this intuition to skip over this step in the proof without comment. But of course Lean won’t let us skip anything!\nTo implement the axiom of choice, Lean uses a function called Classical.choose. Given a proof h of a statement of the form ∃ (x : U), P x, the expression Classical.choose h produces (“chooses”) some u : U such that P u is true. There is also a theorem Classical.choose_spec that guarantees that the Classical.choose function meets its specification—that is, P (Classical.choose h) is true. Using these, we can prove a lemma that will bridge the gap between Lemma_8_2_2_1 and Theorem_8_2_2.\nlemma Lemma_8_2_2_2 {U : Type} {F : Set (Set U)} (h : ∀ A ∈ F, ctble A) :\n ∃ (f : Set U → Rel Nat U), ∀ A ∈ F, fcnl_onto_from_nat (f A) A := by\n have h1 : ∀ (A : Set U), ∃ (SA : Rel Nat U),\n A ∈ F → fcnl_onto_from_nat SA A := by\n fix A : Set U\n by_cases h2 : A ∈ F\n · -- Case 1. h2 : A ∈ F\n have h3 : ctble A := h A h2\n rewrite [Theorem_8_1_5_2] at h3\n obtain (SA : Rel Nat U) (h4 : fcnl_onto_from_nat SA A) from h3\n apply Exists.intro SA\n assume h5 : A ∈ F\n show fcnl_onto_from_nat SA A from h4\n done\n · -- Case 2. h2 : A ∉ F\n apply Exists.intro (emptyRel Nat U)\n assume h3 : A ∈ F\n show fcnl_onto_from_nat (emptyRel Nat U) A from absurd h3 h2\n done\n done\n set f : Set U → Rel Nat U := fun (A : Set U) => Classical.choose (h1 A)\n apply Exists.intro f\n fix A : Set U\n show A ∈ F → fcnl_onto_from_nat (f A) A from Classical.choose_spec (h1 A)\n done\nNotice that the domain of the function f in Lemma_8_2_2_2 is Set U, not F. Thus, we must produce a relation SA for every A : Set U, but it is only when A ∈ F that we care what SA is. Thus, the proof above just picks a default value (emptyRel Nat U) when A ∉ F.\nWe now have everything in place to prove Theorem_8_2_2:\ntheorem Theorem_8_2_2 {U : Type} {F : Set (Set U)}\n (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) : ctble (⋃₀ F) := by\n obtain (f : Set U → Rel Nat U) (h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A)\n from Lemma_8_2_2_2 h2\n show ctble (⋃₀ F) from Lemma_8_2_2_1 h1 h3\n done\nBy the way, we can now explain a mystery from Section 5.1. The reason we skipped the proof of the right-to-left direction of func_from_graph is that the proof uses Classical.choose and Classical.choose_spec. Now that you know about this function and theorem, we can show you the proof.\ntheorem func_from_graph_rtl {A B : Type} (F : Set (A × B)) :\n is_func_graph F → (∃ (f : A → B), graph f = F) := by\n assume h1 : is_func_graph F\n define at h1 --h1 : ∀ (x : A), ∃! (y : B), (x, y) ∈ F\n have h2 : ∀ (x : A), ∃ (y : B), (x, y) ∈ F := by\n fix x : A\n obtain (y : B) (h3 : (x, y) ∈ F)\n (h4 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x\n show ∃ (y : B), (x, y) ∈ F from Exists.intro y h3\n done\n set f : A → B := fun (x : A) => Classical.choose (h2 x)\n apply Exists.intro f\n apply Set.ext\n fix (x, y) : A × B\n have h3 : (x, f x) ∈ F := Classical.choose_spec (h2 x)\n apply Iff.intro\n · -- (→)\n assume h4 : (x, y) ∈ graph f\n define at h4 --h4 : f x = y\n rewrite [h4] at h3\n show (x, y) ∈ F from h3\n done\n · -- (←)\n assume h4 : (x, y) ∈ F\n define --Goal : f x = y\n obtain (z : B) (h5 : (x, z) ∈ F)\n (h6 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x\n show f x = y from h6 (f x) y h3 h4\n done\n done\nThere is one more theorem in Section 8.2 of HTPI showing that a set-theoretic operation, when applied to a countable set, gives a countable result. Theorem 8.2.4 says that if a set \\(A\\) is countable, then the set of all finite sequences of elements of \\(A\\) is also countable. In HTPI, finite sequences are represented by functions, but in Lean it is easier to use lists. Thus, if A has type Set U, then we define a finite sequence of elements of A to be a list l : List U with the property that every entry of l is an element of A. Letting seq A denote the set of all finite sequences of elements of A, our version of Theorem 8.2.4 will say that if A is countable, then so is seq A.\ndef seq {U : Type} (A : Set U) : Set (List U) :=\n {l : List U | ∀ x ∈ l, x ∈ A}\n\nlemma seq_def {U : Type} (A : Set U) (l : List U) :\n l ∈ seq A ↔ ∀ x ∈ l, x ∈ A := by rfl\n\ntheorem Theorem_8_2_4 {U : Type} {A : Set U}\n (h1 : ctble A) : ctble (seq A)\nOur proof of Theorem_8_2_4 will use exactly the same strategy as the proof in HTPI. We begin by showing that, for every natural number n, the set of sequences of elements of A of length n is countable. The proof is by mathematical induction. The base case is easy, because the only sequence of length 0 is the nil list.\ndef seq_by_length {U : Type} (A : Set U) (n : Nat) : Set (List U) :=\n {l : List U | l ∈ seq A ∧ l.length = n}\n\nlemma sbl_base {U : Type} (A : Set U) : seq_by_length A 0 = {[]} := by\n apply Set.ext\n fix l : List U\n apply Iff.intro\n · -- (→)\n assume h1 : l ∈ seq_by_length A 0\n define at h1 --h1 : l ∈ seq A ∧ List.length l = 0\n rewrite [List.length_eq_zero] at h1\n define\n show l = [] from h1.right\n done\n · -- (←)\n assume h1 : l ∈ {[]}\n define at h1 --h1 : l = []\n define --Goal : l ∈ seq A ∧ List.length l = 0\n apply And.intro _ (List.length_eq_zero.rtl h1)\n define --Goal : ∀ x ∈ l, x ∈ A\n fix x : U\n assume h2 : x ∈ l\n contradict h2 with h3\n rewrite [h1]\n show x ∉ [] from List.not_mem_nil x\n done\n done\nFor the induction step, the key idea is that A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1). To prove this, we define a function seq_cons U that matches up A ×ₛ (seq_by_length A n) with seq_by_length A (n + 1).\ndef seq_cons (U : Type) (p : U × (List U)) : List U := p.1 :: p.2\n\nlemma seq_cons_def {U : Type} (x : U) (l : List U) :\n seq_cons U (x, l) = x :: l := by rfl\n\nlemma seq_cons_one_one (U : Type) : one_to_one (seq_cons U) := by\n fix (a1, l1) : U × List U; fix (a2, l2) : U × List U\n assume h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)\n rewrite [seq_cons_def, seq_cons_def] at h1 --h1 : a1 :: l1 = a2 :: l2\n rewrite [List.cons_eq_cons] at h1 --h1 : a1 = a2 ∧ l1 = l2\n rewrite [h1.left, h1.right]\n rfl\n done\n\nlemma seq_cons_image {U : Type} (A : Set U) (n : Nat) :\n image (seq_cons U) (A ×ₛ (seq_by_length A n)) =\n seq_by_length A (n + 1) := sorry\n\nlemma Lemma_8_2_4_1 {U : Type} (A : Set U) (n : Nat) :\n A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1) :=\n equinum_image (one_one_on_of_one_one (seq_cons_one_one U)\n (A ×ₛ (seq_by_length A n))) (seq_cons_image A n)\nWith this preparation, we can now use singleton_one_elt to justify the base case of our induction proof and Theorem_8_2_1_1 for the induction step.\nlemma Lemma_8_2_4_2 {U : Type} {A : Set U} (h1 : ctble A) :\n ∀ (n : Nat), ctble (seq_by_length A n) := by\n by_induc\n · -- Base Case\n rewrite [sbl_base] --Goal : ctble {[]}\n define\n apply Or.inl --Goal : finite {[]}\n rewrite [finite_def]\n apply Exists.intro 1 --Goal : numElts {[]} 1\n show numElts {[]} 1 from singleton_one_elt []\n done\n · -- Induction Step\n fix n : Nat\n assume ih : ctble (seq_by_length A n)\n have h2 : A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1) :=\n Lemma_8_2_4_1 A n\n have h3 : ctble (A ×ₛ (seq_by_length A n)) := Theorem_8_2_1_1 h1 ih\n show ctble (seq_by_length A (n + 1)) from ctble_of_equinum_ctble h2 h3\n done\n done\nOur next step is to show that the union of all of the sets seq_by_length A n, for n : Nat, is seq A.\ndef sbl_set {U : Type} (A : Set U) : Set (Set (List U)) :=\n {S : Set (List U) | ∃ (n : Nat), seq_by_length A n = S}\n\nlemma Lemma_8_2_4_3 {U : Type} (A : Set U) : ⋃₀ (sbl_set A) = seq A := by\n apply Set.ext\n fix l : List U\n apply Iff.intro\n · -- (→)\n assume h1 : l ∈ ⋃₀ (sbl_set A)\n define at h1\n obtain (S : Set (List U)) (h2 : S ∈ sbl_set A ∧ l ∈ S) from h1\n have h3 : S ∈ sbl_set A := h2.left\n define at h3\n obtain (n : Nat) (h4 : seq_by_length A n = S) from h3\n have h5 : l ∈ S := h2.right\n rewrite [←h4] at h5\n define at h5\n show l ∈ seq A from h5.left\n done\n · -- (←)\n assume h1 : l ∈ seq A\n define\n set n : Nat := l.length\n apply Exists.intro (seq_by_length A n)\n apply And.intro\n · -- Proof of seq_by_length A n ∈ sbl_set A\n define\n apply Exists.intro n\n rfl\n done\n · -- Proof of l ∈ seq_by_length A n\n define\n apply And.intro h1\n rfl\n done\n done\n done\nOf course, sbl_set A is countable. The easiest way to prove this is to apply an exercise from Section 8.1.\ntheorem ctble_of_onto_func_from_N {U : Type} {A : Set U} {f : Nat → U}\n (h1 : ∀ x ∈ A, ∃ (n : Nat), f n = x) : ctble A := sorry\n\nlemma Lemma_8_2_4_4 {U : Type} (A : Set U) : ctble (sbl_set A) := by\n have h1 : ∀ S ∈ sbl_set A, ∃ (n : Nat), seq_by_length A n = S := by\n fix S : Set (List U)\n assume h1 : S ∈ sbl_set A\n define at h1\n show ∃ (n : Nat), seq_by_length A n = S from h1\n done\n show ctble (sbl_set A) from ctble_of_onto_func_from_N h1\n done\nWe now have everything we need to prove Theorem_8_2_4 as an application of Theorem_8_2_2.\ntheorem Theorem_8_2_4 {U : Type} {A : Set U}\n (h1 : ctble A) : ctble (seq A) := by\n set F : Set (Set (List U)) := sbl_set A\n have h2 : ctble F := Lemma_8_2_4_4 A\n have h3 : ∀ S ∈ F, ctble S := by\n fix S : Set (List U)\n assume h3 : S ∈ F\n define at h3\n obtain (n : Nat) (h4 : seq_by_length A n = S) from h3\n rewrite [←h4]\n show ctble (seq_by_length A n) from Lemma_8_2_4_2 h1 n\n done\n rewrite [←Lemma_8_2_4_3 A]\n show ctble (⋃₀ sbl_set A) from Theorem_8_2_2 h2 h3\n done\nThere is a set-theoretic operation that can produce an uncountable set from a countable set: the power set operation. HTPI demonstrates this by proving Cantor’s theorem (Theorem 8.2.5), which says that \\(\\mathscr{P}(\\mathbb{Z}^+)\\) is uncountable. The strategy for this proof is tricky; it involves defining a set \\(D\\) using a method called diagonalization. For an explanation of the motivation behind this strategy, see HTPI. Here we will use this strategy to prove that 𝒫 (Univ Nat) is uncountable.\nlemma set_elt_powerset_univ {U : Type} (A : Set U) :\n A ∈ 𝒫 (Univ U) := by\n fix x : U\n assume h : x ∈ A\n show x ∈ Univ U from elt_Univ x\n done\n\ntheorem Cantor's_theorem : ¬ctble (𝒫 (Univ Nat)) := by\n by_contra h1\n rewrite [Theorem_8_1_5_2] at h1\n obtain (R : Rel Nat (Set Nat))\n (h2 : fcnl_onto_from_nat R (𝒫 (Univ Nat))) from h1\n define at h2\n have h3 : unique_val_on_N R := h2.left\n have h4 : nat_rel_onto R (𝒫 (Univ Nat)) := h2.right\n set D : Set Nat := {n : Nat | ∃ (X : Set Nat), R n X ∧ n ∉ X}\n have h5 : D ∈ 𝒫 (Univ Nat) := set_elt_powerset_univ D\n define at h4\n obtain (n : Nat) (h6 : R n D) from h4 h5\n by_cases h7 : n ∈ D\n · -- Case 1. h7 : n ∈ D\n contradict h7\n define at h7\n obtain (X : Set Nat) (h8 : R n X ∧ n ∉ X) from h7\n define at h3\n have h9 : D = X := h3 h6 h8.left\n rewrite [h9]\n show n ∉ X from h8.right\n done\n · -- Case 2. h7 : n ∉ D\n contradict h7\n define\n show ∃ (X : Set Nat), R n X ∧ n ∉ X from\n Exists.intro D (And.intro h6 h7)\n done\n done\nAs a consequence of Theorem 8.2.5, HTPI shows that \\(\\mathbb{R}\\) is uncountable. The proof is not hard, but it requires facts about the decimal expansions of real numbers. Developing those facts in Lean would take us too far afield, so we will skip the proof.\n\nExercises\n\nlemma pair_ctble {U : Type} (a b : U) : ctble {a, b} := sorry\n\n\n--Hint: Use the previous exercise and Theorem_8_2_2\ntheorem Theorem_8_2_1_2 {U : Type} {A B : Set U}\n (h1 : ctble A) (h2 : ctble B) : ctble (A ∪ B) := sorry\n\n\nlemma seq_cons_image {U : Type} (A : Set U) (n : Nat) :\n image (seq_cons U) (A ×ₛ (seq_by_length A n)) =\n seq_by_length A (n + 1) := sorry\n\n\n--Hint: Use induction on the size of A\nlemma set_to_list {U : Type} {A : Set U} (h : finite A) :\n ∃ (l : List U), ∀ (x : U), x ∈ l ↔ x ∈ A := sorry\n\n\n--Hint: Use the previous exercise and Theorem_8_2_4\ntheorem Like_Exercise_8_2_4 {U : Type} {A : Set U} (h : ctble A) :\n ctble {X : Set U | X ⊆ A ∧ finite X} := sorry\n\n\ntheorem Exercise_8_2_6b (A B C : Type) :\n Univ ((A × B) → C) ∼ Univ (A → (B → C)) := sorry\n\n\ntheorem Like_Exercise_8_2_7 : ∃ (P : Set (Set Nat)),\n partition P ∧ denum P ∧ ∀ X ∈ P, denum X := sorry\n\n\ntheorem unctbly_many_inf_set_nat :\n ¬ctble {X : Set Nat | ¬finite X} := sorry\n\n\ntheorem Exercise_8_2_8 {U : Type} {A B : Set U}\n (h : empty (A ∩ B)) : 𝒫 (A ∪ B) ∼ 𝒫 A ×ₛ 𝒫 B := sorry"
+ "text": "8.2. Countable and Uncountable Sets\nSection 8.2 of HTPI shows that many set-theoretic operations, when applied to countable sets, produce results that are countable. For example, the first part of Theorem 8.2.1 shows that a Cartesian product of countable sets is countable. Our proof of this statement in Lean is based on Theorem_8_1_2_1 and the countability of Univ (Nat × Nat). We also use an exercise from Section 8.1.\ntheorem Exercise_8_1_17 {U : Type} {A B : Set U}\n (h1 : B ⊆ A) (h2 : ctble A) : ctble B := sorry\n\ntheorem Theorem_8_2_1_1 {U V : Type} {A : Set U} {B : Set V}\n (h1 : ctble A) (h2 : ctble B) : ctble (A ×ₛ B) := by\n rewrite [ctble_iff_equinum_set_nat] at h1\n rewrite [ctble_iff_equinum_set_nat] at h2\n obtain (I : Set Nat) (h3 : I ∼ A) from h1\n obtain (J : Set Nat) (h4 : J ∼ B) from h2\n have h5 : I ×ₛ J ∼ A ×ₛ B := Theorem_8_1_2_1 h3 h4\n have h6 : I ×ₛ J ⊆ Univ (Nat × Nat) := by\n fix p : Nat × Nat\n assume h6 : p ∈ I ×ₛ J\n show p ∈ Univ (Nat × Nat) from elt_Univ p\n done\n have h7 : ctble (Univ (Nat × Nat)) := by\n define --Goal : finite (Univ (Nat × Nat)) ∨ denum (Univ (Nat × Nat))\n apply Or.inr\n rewrite [denum_def]\n show Univ Nat ∼ Univ (Nat × Nat) from Theorem_8_1_3_2 NxN_equinum_N\n done\n have h8 : ctble (I ×ₛ J) := Exercise_8_1_17 h6 h7\n show ctble (A ×ₛ B) from ctble_of_equinum_ctble h5 h8\n done\nThe second part of Theorem 8.2.1 shows that a union of two countable sets is countable, but, as we ask you to show in the exercises, it is superseded by Theorem 8.2.2, which says that a union of a countable family of countable sets is countable. So we will skip ahead to Theorem 8.2.2. Here’s how we state the theorem in Lean:\ntheorem Theorem_8_2_2 {U : Type} {F : Set (Set U)}\n (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) : ctble (⋃₀ F)\nIn our proof, we will use the characterization of countability from Theorem_8_1_5_2. Thus, we will use the hypotheses h1 and h2 to conclude that there is a relation R : Rel Nat (Set U) such that fcnl_onto_from_nat R F, and also that for each A ∈ F there is a relation SA : Rel Nat U such that fcnl_onto_from_nat SA A. We begin by proving an easier version of the theorem, where we assume that we have a function f : Set U → Rel Nat U that supplies, for each A ∈ F, the required relation SA. Imitating the proof in HTPI, we can use R and f to construct the relation needed to prove that ⋃₀ F is countable.\ndef enum_union_fam {U : Type}\n (F : Set (Set U)) (f : Set U → Rel Nat U) (R : Rel Nat (Set U))\n (n : Nat) (a : U) : Prop := ∃ (p : Nat × Nat), fnnn p = n ∧\n ∃ A ∈ F, R p.1 A ∧ (f A) p.2 a\n\nlemma Lemma_8_2_2_1 {U : Type} {F : Set (Set U)} {f : Set U → Rel Nat U}\n (h1 : ctble F) (h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A) :\n ctble (⋃₀ F) := by\n rewrite [Theorem_8_1_5_2] at h1\n rewrite [Theorem_8_1_5_2]\n obtain (R : Rel Nat (Set U)) (h3 : fcnl_onto_from_nat R F) from h1\n define at h3\n have Runiqueval : unique_val_on_N R := h3.left\n have Ronto : nat_rel_onto R F := h3.right\n set S : Rel Nat U := enum_union_fam F f R\n apply Exists.intro S\n define\n apply And.intro\n · -- Proof of unique_val_on_N S\n define\n fix n : Nat; fix a1 : U; fix a2 : U\n assume Sna1 : S n a1\n assume Sna2 : S n a2 --Goal : a1 = a2\n define at Sna1; define at Sna2\n obtain ((i1, j1) : Nat × Nat) (h4 : fnnn (i1, j1) = n ∧\n ∃ A ∈ F, R i1 A ∧ f A j1 a1) from Sna1\n obtain (A1 : Set U) (Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1)\n from h4.right\n obtain ((i2, j2) : Nat × Nat) (h5 : fnnn (i2, j2) = n ∧\n ∃ A ∈ F, R i2 A ∧ f A j2 a2) from Sna2\n obtain (A2 : Set U) (Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2)\n from h5.right\n rewrite [←h5.left] at h4\n have h6 : (i1, j1) = (i2, j2) :=\n fnnn_one_one (i1, j1) (i2, j2) h4.left\n have h7 : i1 = i2 ∧ j1 = j2 := Prod.mk.inj h6\n rewrite [h7.left, h7.right] at Aija1\n --Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1\n define at Runiqueval\n have h8 : A1 = A2 := Runiqueval Aija1.right.left Aija2.right.left\n rewrite [h8] at Aija1 --Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1\n have fA2fcnlonto : fcnl_onto_from_nat (f A2) A2 := h2 A2 Aija2.left\n define at fA2fcnlonto\n have fA2uniqueval : unique_val_on_N (f A2) := fA2fcnlonto.left\n define at fA2uniqueval\n show a1 = a2 from fA2uniqueval Aija1.right.right Aija2.right.right\n done\n · -- Proof of nat_rel_onto S (⋃₀ F)\n define\n fix x : U\n assume h4 : x ∈ ⋃₀ F --Goal : ∃ (n : Nat), S n x\n define at h4\n obtain (A : Set U) (h5 : A ∈ F ∧ x ∈ A) from h4\n define at Ronto\n obtain (i : Nat) (h6 : R i A) from Ronto h5.left\n have fAfcnlonto : fcnl_onto_from_nat (f A) A := h2 A h5.left\n define at fAfcnlonto\n have fAonto : nat_rel_onto (f A) A := fAfcnlonto.right\n define at fAonto\n obtain (j : Nat) (h7 : f A j x) from fAonto h5.right\n apply Exists.intro (fnnn (i, j))\n define --Goal : ∃ (p : Nat × Nat), fnnn p = fnnn (i, j) ∧\n -- ∃ A ∈ F, R p.1 A ∧ f A p.2 x\n apply Exists.intro (i, j)\n apply And.intro\n · -- Proof that fnnn (i, j) = fnnn (i, j)\n rfl\n done\n · -- Proof that ∃ A ∈ F, R (i, j).1 A ∧ f A (i, j).2 x\n apply Exists.intro A\n show A ∈ F ∧ R (i, j).1 A ∧ f A (i, j).2 x from\n And.intro h5.left (And.intro h6 h7)\n done\n done\n done\nHow can we use Lemma_8_2_2_1 to prove Theorem_8_2_2? We must use the hypothesis h2 : ∀ A ∈ F, ctble A in Theorem_8_2_2 to produce the function f required in Lemma_8_2_2_1. As we have already observed, Theorem_8_1_5_2 guarantees that for each A ∈ F, an appropriate relation SA : Rel Nat U exists. We need a function f that will choose such a relation SA for each A. A function with this property is often called a choice function. And now we come to a delicate point that was skipped over in HTPI: to prove the existence of a choice function, we must use a statement called the axiom of choice.1\nThe distinction between the existence of an appropriate relation SA for each A and the existence of a function that chooses such a relation for each A is a subtle one. Perhaps for this reason, many people find the axiom of choice to be intuitively obvious. HTPI took advantage of this intuition to skip over this step in the proof without comment. But of course Lean won’t let us skip anything!\nTo implement the axiom of choice, Lean uses a function called Classical.choose. Given a proof h of a statement of the form ∃ (x : U), P x, the expression Classical.choose h produces (“chooses”) some u : U such that P u is true. There is also a theorem Classical.choose_spec that guarantees that the Classical.choose function meets its specification—that is, P (Classical.choose h) is true. Using these, we can prove a lemma that will bridge the gap between Lemma_8_2_2_1 and Theorem_8_2_2.\nlemma Lemma_8_2_2_2 {U : Type} {F : Set (Set U)} (h : ∀ A ∈ F, ctble A) :\n ∃ (f : Set U → Rel Nat U), ∀ A ∈ F, fcnl_onto_from_nat (f A) A := by\n have h1 : ∀ (A : Set U), ∃ (SA : Rel Nat U),\n A ∈ F → fcnl_onto_from_nat SA A := by\n fix A : Set U\n by_cases h2 : A ∈ F\n · -- Case 1. h2 : A ∈ F\n have h3 : ctble A := h A h2\n rewrite [Theorem_8_1_5_2] at h3\n obtain (SA : Rel Nat U) (h4 : fcnl_onto_from_nat SA A) from h3\n apply Exists.intro SA\n assume h5 : A ∈ F\n show fcnl_onto_from_nat SA A from h4\n done\n · -- Case 2. h2 : A ∉ F\n apply Exists.intro (emptyRel Nat U)\n assume h3 : A ∈ F\n show fcnl_onto_from_nat (emptyRel Nat U) A from absurd h3 h2\n done\n done\n set f : Set U → Rel Nat U := fun (A : Set U) => Classical.choose (h1 A)\n apply Exists.intro f\n fix A : Set U\n show A ∈ F → fcnl_onto_from_nat (f A) A from Classical.choose_spec (h1 A)\n done\nNotice that the domain of the function f in Lemma_8_2_2_2 is Set U, not F. Thus, we must produce a relation SA for every A : Set U, but it is only when A ∈ F that we care what SA is. Thus, the proof above just picks a default value (emptyRel Nat U) when A ∉ F.\nWe now have everything in place to prove Theorem_8_2_2:\ntheorem Theorem_8_2_2 {U : Type} {F : Set (Set U)}\n (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) : ctble (⋃₀ F) := by\n obtain (f : Set U → Rel Nat U) (h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A)\n from Lemma_8_2_2_2 h2\n show ctble (⋃₀ F) from Lemma_8_2_2_1 h1 h3\n done\nBy the way, we can now explain a mystery from Section 5.1. The reason we skipped the proof of the right-to-left direction of func_from_graph is that the proof uses Classical.choose and Classical.choose_spec. Now that you know about this function and theorem, we can show you the proof.\ntheorem func_from_graph_rtl {A B : Type} (F : Set (A × B)) :\n is_func_graph F → (∃ (f : A → B), graph f = F) := by\n assume h1 : is_func_graph F\n define at h1 --h1 : ∀ (x : A), ∃! (y : B), (x, y) ∈ F\n have h2 : ∀ (x : A), ∃ (y : B), (x, y) ∈ F := by\n fix x : A\n obtain (y : B) (h3 : (x, y) ∈ F)\n (h4 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x\n show ∃ (y : B), (x, y) ∈ F from Exists.intro y h3\n done\n set f : A → B := fun (x : A) => Classical.choose (h2 x)\n apply Exists.intro f\n apply Set.ext\n fix (x, y) : A × B\n have h3 : (x, f x) ∈ F := Classical.choose_spec (h2 x)\n apply Iff.intro\n · -- (→)\n assume h4 : (x, y) ∈ graph f\n define at h4 --h4 : f x = y\n rewrite [h4] at h3\n show (x, y) ∈ F from h3\n done\n · -- (←)\n assume h4 : (x, y) ∈ F\n define --Goal : f x = y\n obtain (z : B) (h5 : (x, z) ∈ F)\n (h6 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x\n show f x = y from h6 (f x) y h3 h4\n done\n done\nThere is one more theorem in Section 8.2 of HTPI showing that a set-theoretic operation, when applied to a countable set, gives a countable result. Theorem 8.2.4 says that if a set \\(A\\) is countable, then the set of all finite sequences of elements of \\(A\\) is also countable. In HTPI, finite sequences are represented by functions, but in Lean it is easier to use lists. Thus, if A has type Set U, then we define a finite sequence of elements of A to be a list l : List U with the property that every entry of l is an element of A. Letting seq A denote the set of all finite sequences of elements of A, our version of Theorem 8.2.4 will say that if A is countable, then so is seq A.\ndef seq {U : Type} (A : Set U) : Set (List U) :=\n {l : List U | ∀ x ∈ l, x ∈ A}\n\nlemma seq_def {U : Type} (A : Set U) (l : List U) :\n l ∈ seq A ↔ ∀ x ∈ l, x ∈ A := by rfl\n\ntheorem Theorem_8_2_4 {U : Type} {A : Set U}\n (h1 : ctble A) : ctble (seq A)\nOur proof of Theorem_8_2_4 will use exactly the same strategy as the proof in HTPI. We begin by showing that, for every natural number n, the set of sequences of elements of A of length n is countable. The proof is by mathematical induction. The base case is easy, because the only sequence of length 0 is the nil list.\ndef seq_by_length {U : Type} (A : Set U) (n : Nat) : Set (List U) :=\n {l : List U | l ∈ seq A ∧ l.length = n}\n\nlemma sbl_base {U : Type} (A : Set U) : seq_by_length A 0 = {[]} := by\n apply Set.ext\n fix l : List U\n apply Iff.intro\n · -- (→)\n assume h1 : l ∈ seq_by_length A 0\n define at h1 --h1 : l ∈ seq A ∧ l.length = 0\n rewrite [List.length_eq_zero] at h1\n define\n show l = [] from h1.right\n done\n · -- (←)\n assume h1 : l ∈ {[]}\n define at h1 --h1 : l = []\n define --Goal : l ∈ seq A ∧ l.length = 0\n apply And.intro _ (List.length_eq_zero.rtl h1)\n define --Goal : ∀ x ∈ l, x ∈ A\n fix x : U\n assume h2 : x ∈ l\n contradict h2 with h3\n rewrite [h1]\n show x ∉ [] from List.not_mem_nil x\n done\n done\nFor the induction step, the key idea is that A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1). To prove this, we define a function seq_cons U that matches up A ×ₛ (seq_by_length A n) with seq_by_length A (n + 1).\ndef seq_cons (U : Type) (p : U × (List U)) : List U := p.1 :: p.2\n\nlemma seq_cons_def {U : Type} (x : U) (l : List U) :\n seq_cons U (x, l) = x :: l := by rfl\n\nlemma seq_cons_one_one (U : Type) : one_to_one (seq_cons U) := by\n fix (a1, l1) : U × List U; fix (a2, l2) : U × List U\n assume h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)\n rewrite [seq_cons_def, seq_cons_def] at h1 --h1 : a1 :: l1 = a2 :: l2\n rewrite [List.cons_eq_cons] at h1 --h1 : a1 = a2 ∧ l1 = l2\n rewrite [h1.left, h1.right]\n rfl\n done\n\nlemma seq_cons_image {U : Type} (A : Set U) (n : Nat) :\n image (seq_cons U) (A ×ₛ (seq_by_length A n)) =\n seq_by_length A (n + 1) := sorry\n\nlemma Lemma_8_2_4_1 {U : Type} (A : Set U) (n : Nat) :\n A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1) :=\n equinum_image (one_one_on_of_one_one (seq_cons_one_one U)\n (A ×ₛ (seq_by_length A n))) (seq_cons_image A n)\nWith this preparation, we can now use singleton_one_elt to justify the base case of our induction proof and Theorem_8_2_1_1 for the induction step.\nlemma Lemma_8_2_4_2 {U : Type} {A : Set U} (h1 : ctble A) :\n ∀ (n : Nat), ctble (seq_by_length A n) := by\n by_induc\n · -- Base Case\n rewrite [sbl_base] --Goal : ctble {[]}\n define\n apply Or.inl --Goal : finite {[]}\n rewrite [finite_def]\n apply Exists.intro 1 --Goal : numElts {[]} 1\n show numElts {[]} 1 from singleton_one_elt []\n done\n · -- Induction Step\n fix n : Nat\n assume ih : ctble (seq_by_length A n)\n have h2 : A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1) :=\n Lemma_8_2_4_1 A n\n have h3 : ctble (A ×ₛ (seq_by_length A n)) := Theorem_8_2_1_1 h1 ih\n show ctble (seq_by_length A (n + 1)) from ctble_of_equinum_ctble h2 h3\n done\n done\nOur next step is to show that the union of all of the sets seq_by_length A n, for n : Nat, is seq A.\ndef sbl_set {U : Type} (A : Set U) : Set (Set (List U)) :=\n {S : Set (List U) | ∃ (n : Nat), seq_by_length A n = S}\n\nlemma Lemma_8_2_4_3 {U : Type} (A : Set U) : ⋃₀ (sbl_set A) = seq A := by\n apply Set.ext\n fix l : List U\n apply Iff.intro\n · -- (→)\n assume h1 : l ∈ ⋃₀ (sbl_set A)\n define at h1\n obtain (S : Set (List U)) (h2 : S ∈ sbl_set A ∧ l ∈ S) from h1\n have h3 : S ∈ sbl_set A := h2.left\n define at h3\n obtain (n : Nat) (h4 : seq_by_length A n = S) from h3\n have h5 : l ∈ S := h2.right\n rewrite [←h4] at h5\n define at h5\n show l ∈ seq A from h5.left\n done\n · -- (←)\n assume h1 : l ∈ seq A\n define\n set n : Nat := l.length\n apply Exists.intro (seq_by_length A n)\n apply And.intro\n · -- Proof of seq_by_length A n ∈ sbl_set A\n define\n apply Exists.intro n\n rfl\n done\n · -- Proof of l ∈ seq_by_length A n\n define\n apply And.intro h1\n rfl\n done\n done\n done\nOf course, sbl_set A is countable. The easiest way to prove this is to apply an exercise from Section 8.1.\ntheorem ctble_of_onto_func_from_N {U : Type} {A : Set U} {f : Nat → U}\n (h1 : ∀ x ∈ A, ∃ (n : Nat), f n = x) : ctble A := sorry\n\nlemma Lemma_8_2_4_4 {U : Type} (A : Set U) : ctble (sbl_set A) := by\n have h1 : ∀ S ∈ sbl_set A, ∃ (n : Nat), seq_by_length A n = S := by\n fix S : Set (List U)\n assume h1 : S ∈ sbl_set A\n define at h1\n show ∃ (n : Nat), seq_by_length A n = S from h1\n done\n show ctble (sbl_set A) from ctble_of_onto_func_from_N h1\n done\nWe now have everything we need to prove Theorem_8_2_4 as an application of Theorem_8_2_2.\ntheorem Theorem_8_2_4 {U : Type} {A : Set U}\n (h1 : ctble A) : ctble (seq A) := by\n set F : Set (Set (List U)) := sbl_set A\n have h2 : ctble F := Lemma_8_2_4_4 A\n have h3 : ∀ S ∈ F, ctble S := by\n fix S : Set (List U)\n assume h3 : S ∈ F\n define at h3\n obtain (n : Nat) (h4 : seq_by_length A n = S) from h3\n rewrite [←h4]\n show ctble (seq_by_length A n) from Lemma_8_2_4_2 h1 n\n done\n rewrite [←Lemma_8_2_4_3 A]\n show ctble (⋃₀ sbl_set A) from Theorem_8_2_2 h2 h3\n done\nThere is a set-theoretic operation that can produce an uncountable set from a countable set: the power set operation. HTPI demonstrates this by proving Cantor’s theorem (Theorem 8.2.5), which says that \\(\\mathscr{P}(\\mathbb{Z}^+)\\) is uncountable. The strategy for this proof is tricky; it involves defining a set \\(D\\) using a method called diagonalization. For an explanation of the motivation behind this strategy, see HTPI. Here we will use this strategy to prove that 𝒫 (Univ Nat) is uncountable.\nlemma set_elt_powerset_univ {U : Type} (A : Set U) :\n A ∈ 𝒫 (Univ U) := by\n fix x : U\n assume h : x ∈ A\n show x ∈ Univ U from elt_Univ x\n done\n\ntheorem Cantor's_theorem : ¬ctble (𝒫 (Univ Nat)) := by\n by_contra h1\n rewrite [Theorem_8_1_5_2] at h1\n obtain (R : Rel Nat (Set Nat))\n (h2 : fcnl_onto_from_nat R (𝒫 (Univ Nat))) from h1\n define at h2\n have h3 : unique_val_on_N R := h2.left\n have h4 : nat_rel_onto R (𝒫 (Univ Nat)) := h2.right\n set D : Set Nat := {n : Nat | ∃ (X : Set Nat), R n X ∧ n ∉ X}\n have h5 : D ∈ 𝒫 (Univ Nat) := set_elt_powerset_univ D\n define at h4\n obtain (n : Nat) (h6 : R n D) from h4 h5\n by_cases h7 : n ∈ D\n · -- Case 1. h7 : n ∈ D\n contradict h7\n define at h7\n obtain (X : Set Nat) (h8 : R n X ∧ n ∉ X) from h7\n define at h3\n have h9 : D = X := h3 h6 h8.left\n rewrite [h9]\n show n ∉ X from h8.right\n done\n · -- Case 2. h7 : n ∉ D\n contradict h7\n define\n show ∃ (X : Set Nat), R n X ∧ n ∉ X from\n Exists.intro D (And.intro h6 h7)\n done\n done\nAs a consequence of Theorem 8.2.5, HTPI shows that \\(\\mathbb{R}\\) is uncountable. The proof is not hard, but it requires facts about the decimal expansions of real numbers. Developing those facts in Lean would take us too far afield, so we will skip the proof.\n\nExercises\n\nlemma pair_ctble {U : Type} (a b : U) : ctble {a, b} := sorry\n\n\n--Hint: Use the previous exercise and Theorem_8_2_2\ntheorem Theorem_8_2_1_2 {U : Type} {A B : Set U}\n (h1 : ctble A) (h2 : ctble B) : ctble (A ∪ B) := sorry\n\n\nlemma seq_cons_image {U : Type} (A : Set U) (n : Nat) :\n image (seq_cons U) (A ×ₛ (seq_by_length A n)) =\n seq_by_length A (n + 1) := sorry\n\n\n--Hint: Use induction on the size of A\nlemma set_to_list {U : Type} {A : Set U} (h : finite A) :\n ∃ (l : List U), ∀ (x : U), x ∈ l ↔ x ∈ A := sorry\n\n\n--Hint: Use the previous exercise and Theorem_8_2_4\ntheorem Like_Exercise_8_2_4 {U : Type} {A : Set U} (h : ctble A) :\n ctble {X : Set U | X ⊆ A ∧ finite X} := sorry\n\n\ntheorem Exercise_8_2_6b (A B C : Type) :\n Univ ((A × B) → C) ∼ Univ (A → (B → C)) := sorry\n\n\ntheorem Like_Exercise_8_2_7 : ∃ (P : Set (Set Nat)),\n partition P ∧ denum P ∧ ∀ X ∈ P, denum X := sorry\n\n\ntheorem unctbly_many_inf_set_nat :\n ¬ctble {X : Set Nat | ¬finite X} := sorry\n\n\ntheorem Exercise_8_2_8 {U : Type} {A B : Set U}\n (h : empty (A ∩ B)) : 𝒫 (A ∪ B) ∼ 𝒫 A ×ₛ 𝒫 B := sorry"
},
{
"objectID": "Chap8.html#the-cantorschröderbernstein-theorem",
diff --git a/lean.xml b/lean.xml
index 9b3be24..51b78e4 100644
--- a/lean.xml
+++ b/lean.xml
@@ -70,6 +70,7 @@
- push_neg
- #eval
- #check
+- @[semireducible]
- sorry
@@ -126,6 +127,6 @@