doc(number_theory/*): provide docstrings for basic and dioph (#6063)

The main purpose of this PR is to provide docstrings for the two remaining files without docstring in number_theory, basic and dioph. Furthermore, lines are split in other files, so that there should be no number_theory entries in the style_exceptions file.



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>

Author: Julian-Kuelshammer

src/number_theory/basic.lean

@@ -7,6 +7,19 @@ Authors: Johan Commelin, Kenny Lau
 import algebra.geom_sum
 import ring_theory.ideal.basic
 
+/-!
+# Basic results in number theory
+
+This file should contain basic results in number theory. So far, it only contains the essential
+lemma in the construction of the ring of Witt vectors.
+
+## Main statement
+
+`dvd_sub_pow_of_dvd_sub` proves that for elements `a` and `b` in a commutative ring `R` and for
+all natural numbers `p` and `k` if `p` divides `a-b` in `R`, then `p ^ (k + 1)` divides
+`a ^ (p ^ k) - b ^ (p ^ k)`.
+-/
+
 section
 
 open ideal ideal.quotient

src/number_theory/dioph.lean

@@ -3,10 +3,50 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+
 import number_theory.pell
 import data.pfun
 import data.fin2
 
+/-!
+# Diophantine functions and Matiyasevic's theorem
+
+Hilbert's tenth problem asked whether there exists an algorithm which for a given integer polynomial
+determines whether this polynomial has integer solutions. It was answered in the negative in 1970,
+the final step being completed by Matiyasevic who showed that the power function is Diophantine.
+
+Here a function is called Diophantine if its graph is Diophantine as a set. A subset `S ⊆ ℕ ^ α` in
+turn is called Diophantine if there exists an integer polynomial on `α ⊕ β` such that `v ∈ S` iff
+there exists `t : ℕ^β` with `p (v, t) = 0`.
+
+## Main definitions
+
+* `is_poly`: a predicate stating that a function is a multivariate integer polynomial.
+* `poly`: the type of multivariate integer polynomial functions.
+* `dioph`: a predicate stating that a set `S ⊆ ℕ^α` is Diophantine, i.e. that
+* `dioph_fn`: a predicate on a function stating that it is Diophantine in the sense that its graph
+  is Diophantine as a set.
+
+## Main statements
+
+* `pell_dioph` states that solutions to Pell's equation form a Diophantine set.
+* `pow_dioph` states that the power function is Diophantine, a version of Matiyasevic's theorem.
+
+## References
+
+* [M. Carneiro, _A Lean formalization of Matiyasevic's theorem_][carneiro2018matiyasevic]
+* [M. Davis, _Hilbert's tenth problem is unsolvable_][MR317916]
+
+## Tags
+
+Matiyasevic's theorem, Hilbert's tenth problem
+
+## TODO
+
+* Finish the solution of Hilbert's tenth problem.
+* Connect `poly` to `mv_polynomial`
+-/
+
 universe u
 
 open nat function
@@ -389,7 +429,7 @@ end option
 
 /- dioph -/
 
-/-- A set `S ⊆ ℕ^α` is diophantine if there exists a polynomial on
+/-- A set `S ⊆ ℕ^α` is Diophantine if there exists a polynomial on
   `α ⊕ β` such that `v ∈ S` iff there exists `t : ℕ^β` with `p (v, t) = 0`. -/
 def dioph {α : Type u} (S : set (α → ℕ)) : Prop :=
 ∃ {β : Type u} (p : poly (α ⊕ β)), ∀ (v : α → ℕ), S v ↔ ∃t, p (v ⊗ t) = 0

src/number_theory/lucas_lehmer.lean

@@ -398,7 +398,8 @@ begin
   { norm_num, },
   { intro o,
     have ω_pow := order_of_dvd_iff_pow_eq_one.1 o,
-    replace ω_pow := congr_arg (units.coe_hom (X (q (p'+2))) : units (X (q (p'+2))) → X (q (p'+2))) ω_pow,
+    replace ω_pow := congr_arg (units.coe_hom (X (q (p'+2))) :
+      units (X (q (p'+2))) → X (q (p'+2))) ω_pow,
     simp at ω_pow,
     have h : (1 : zmod (q (p'+2))) = -1 :=
       congr_arg (prod.fst) ((ω_pow.symm).trans (ω_pow_eq_neg_one p' h)),

src/number_theory/pell.lean

@@ -14,7 +14,7 @@ import tactic.omega
 This file solves Pell's equation, i.e. integer solutions to `x ^ 2 - d * y ^ 2 = 1` in the special
 case that `d = a ^ 2 - 1`. This is then applied to prove Matiyasevic's theorem that the power
 function is Diophantine, which is the last key ingredient in the solution to Hilbert's tenth
-problem.
+problem. For the definition of Diophantine function, see `dioph.lean`.
 
 ## Main definition
 
@@ -113,8 +113,10 @@ section
   def is_pell : ℤ√d → Prop | ⟨x, y⟩ := x*x - d*y*y = 1
 
   theorem is_pell_nat {x y : ℕ} : is_pell ⟨x, y⟩ ↔ x*x - d*y*y = 1 :=
-  ⟨λh, int.coe_nat_inj (by rw int.coe_nat_sub (int.le_of_coe_nat_le_coe_nat $ int.le.intro_sub h); exact h),
-  λh, show ((x*x : ℕ) - (d*y*y:ℕ) : ℤ) = 1, by rw [← int.coe_nat_sub $ le_of_lt $ nat.lt_of_sub_eq_succ h, h]; refl⟩
+  ⟨λh, int.coe_nat_inj
+    (by rw int.coe_nat_sub (int.le_of_coe_nat_le_coe_nat $ int.le.intro_sub h); exact h),
+  λh, show ((x*x : ℕ) - (d*y*y:ℕ) : ℤ) = 1,
+    by rw [← int.coe_nat_sub $ le_of_lt $ nat.lt_of_sub_eq_succ h, h]; refl⟩
 
   theorem is_pell_norm : Π {b : ℤ√d}, is_pell b ↔ b * b.conj = 1
   | ⟨x, y⟩ := by simp [zsqrtd.ext, is_pell, mul_comm]; ring
@@ -151,7 +153,7 @@ section
     have na : n < a, from nat.mul_self_lt_mul_self_iff.2 (by rw ← this; exact nat.lt_succ_self _),
     have (n+1)*(n+1) ≤ n*n + 1, by rw this; exact nat.mul_self_le_mul_self na,
     have n+n ≤ 0, from @nat.le_of_add_le_add_right (n*n + 1) _ _ (by ring at this ⊢; assumption),
-    ne_of_gt d_pos $ by rw nat.eq_zero_of_le_zero (le_trans (nat.le_add_left _ _) this) at h; exact h⟩
+    ne_of_gt d_pos $ by rwa nat.eq_zero_of_le_zero ((nat.le_add_left _ _).trans this) at h⟩
 
   theorem xn_ge_a_pow : ∀ (n : ℕ), a^n ≤ xn n
   | 0     := le_refl 1
@@ -450,7 +452,8 @@ section
      (lt_or_eq_of_le (nat.le_of_succ_le_succ ij)).elim
         (λh, lt_trans (eq_of_xn_modeq_lem1 h (le_of_lt jn)) this)
         (λh, by rw h; exact this),
-    by rw [nat.mod_eq_of_lt (x_increasing _ (nat.lt_of_succ_lt jn)), nat.mod_eq_of_lt (x_increasing _ jn)];
+    by rw [nat.mod_eq_of_lt (x_increasing _ (nat.lt_of_succ_lt jn)),
+           nat.mod_eq_of_lt (x_increasing _ jn)];
        exact x_increasing _ (nat.lt_succ_self _)
 
   theorem eq_of_xn_modeq_lem2 {n} (h : 2 * xn n = xn (n + 1)) : a = 2 ∧ n = 0 :=
@@ -487,23 +490,25 @@ section
       cases (lt_or_eq_of_le $ nat.le_of_succ_le_succ ij) with lin ein,
       { rw nat.mod_eq_of_lt (x_increasing _ lin),
         have ll : xn a1 (n-1) + xn a1 (n-1) ≤ xn a1 n,
-        { rw [← two_mul, mul_comm, show xn a1 n = xn a1 (n-1+1), by rw [nat.sub_add_cancel npos], xn_succ],
+        { rw [← two_mul, mul_comm, show xn a1 n = xn a1 (n-1+1),
+                                   by rw [nat.sub_add_cancel npos], xn_succ],
           exact le_trans (nat.mul_le_mul_left _ a1) (nat.le_add_right _ _) },
         have npm : (n-1).succ = n := nat.succ_pred_eq_of_pos npos,
-        have il : i ≤ n - 1 := by apply nat.le_of_succ_le_succ; rw npm; exact lin,
+        have il : i ≤ n - 1, { apply nat.le_of_succ_le_succ, rw npm, exact lin },
         cases lt_or_eq_of_le il with ill ile,
         { exact lt_of_lt_of_le (nat.add_lt_add_left (x_increasing a1 ill) _) ll },
         { rw ile,
           apply lt_of_le_of_ne ll,
           rw ← two_mul,
           exact λe, ntriv $
-            let ⟨a2, s1⟩ := @eq_of_xn_modeq_lem2 _ a1 (n-1) (by rw[nat.sub_add_cancel npos]; exact e) in
+            let ⟨a2, s1⟩ := @eq_of_xn_modeq_lem2 _ a1 (n-1) (by rwa [nat.sub_add_cancel npos]) in
             have n1 : n = 1, from le_antisymm (nat.le_of_sub_eq_zero s1) npos,
             by rw [ile, a2, n1]; exact ⟨rfl, rfl, rfl, rfl⟩ } },
       { rw [ein, nat.mod_self, add_zero],
         exact x_increasing _ (nat.pred_lt $ ne_of_gt npos) } })
     (λ (jn : j > n),
-      have lem1 : j ≠ n → xn j % xn n < xn (j + 1) % xn n → xn i % xn n < xn (j + 1) % xn n, from λjn s,
+      have lem1 : j ≠ n → xn j % xn n < xn (j + 1) % xn n → xn i % xn n < xn (j + 1) % xn n,
+        from λjn s,
       (lt_or_eq_of_le (nat.le_of_succ_le_succ ij)).elim
         (λh, lt_trans (eq_of_xn_modeq_lem3 h (le_of_lt j2n) jn $ λ⟨a1, n1, i0, j2⟩,
           by rw [n1, j2] at j2n; exact absurd j2n dec_trivial) s)
@@ -533,10 +538,11 @@ section
     i = j :=
   (le_total i j).elim
     (λij, eq_of_xn_modeq_le npos ij j2n h $ λ⟨a2, n1, i0, j2⟩, (ntriv a2 n1).left i0 j2)
-    (λij, (eq_of_xn_modeq_le npos ij i2n h.symm $ λ⟨a2, n1, j0, i2⟩, (ntriv a2 n1).right i2 j0).symm)
+    (λij, (eq_of_xn_modeq_le npos ij i2n h.symm $ λ⟨a2, n1, j0, i2⟩,
+      (ntriv a2 n1).right i2 j0).symm)
 
-  theorem eq_of_xn_modeq' {i j n} (ipos : 0 < i) (hin : i ≤ n) (j4n : j ≤ 4 * n) (h : xn j ≡ xn i [MOD xn n]) :
-    j = i ∨ j + i = 4 * n :=
+  theorem eq_of_xn_modeq' {i j n} (ipos : 0 < i) (hin : i ≤ n) (j4n : j ≤ 4 * n)
+    (h : xn j ≡ xn i [MOD xn n]) : j = i ∨ j + i = 4 * n :=
   have i2n : i ≤ 2*n, by apply le_trans hin; rw two_mul; apply nat.le_add_left,
   have npos : 0 < n, from lt_of_lt_of_le ipos hin,
   (le_or_gt j (2 * n)).imp
@@ -549,7 +555,8 @@ section
         exact nat.add_le_add_left (le_of_lt j2n) _,
      eq_of_xn_modeq npos i2n j42n
        (h.symm.trans $ let t := xn_modeq_x4n_sub j42n in by rwa [nat.sub_sub_self j4n] at t)
-       (λa2 n1, ⟨λi0, absurd i0 (ne_of_gt ipos), λi2, by rw[n1, i2] at hin; exact absurd hin dec_trivial⟩))
+       (λa2 n1, ⟨λi0, absurd i0 (ne_of_gt ipos), λi2, by { rw [n1, i2] at hin,
+         exact absurd hin dec_trivial }⟩))
 
   theorem modeq_of_xn_modeq {i j n} (ipos : 0 < i) (hin : i ≤ n) (h : xn j ≡ xn i [MOD xn n]) :
     j ≡ i [MOD 4 * n] ∨ j + i ≡ 0 [MOD 4 * n] :=

src/number_theory/primorial.lean

@@ -36,7 +36,7 @@ begin
     { linarith, },
     { exfalso,
       rw ←not_even_iff at n_even r,
-      have e : even (n + 1 - n), exact (even_sub (le_of_lt (lt_add_one n))).2 (iff_of_false n_even r),
+      have e : even (n + 1 - n) := (even_sub (lt_add_one n).le).2 (iff_of_false n_even r),
       simp only [nat.add_sub_cancel_left, not_even_one] at e,
       exact e, }, },
   apply finset.prod_congr,
@@ -120,31 +120,36 @@ lemma primorial_le_4_pow : ∀ (n : ℕ), n# ≤ 4 ^ n
                 simp only [add_le_add_iff_right],
                 linarith,
               end
-        ... = ∏ i in (filter prime (finset.Ico (m + 2) (2 * m + 2)) ∪ (filter prime (range (m + 2)))), i :
+        ... = ∏ i in (filter prime (finset.Ico (m + 2) (2 * m + 2))
+              ∪ (filter prime (range (m + 2)))), i :
               by rw filter_union
         ... = (∏ i in filter prime (finset.Ico (m + 2) (2 * m + 2)), i)
               * (∏ i in filter prime (range (m + 2)), i) :
               begin
                 apply finset.prod_union,
                 have disj : disjoint (finset.Ico (m + 2) (2 * m + 2)) (range (m + 2)),
-                { simp only [finset.disjoint_left, and_imp, finset.Ico.mem, not_lt, finset.mem_range],
+                { simp only [finset.disjoint_left, and_imp, finset.Ico.mem, not_lt,
+                    finset.mem_range],
                   intros _ pr _, exact pr, },
                 exact finset.disjoint_filter_filter disj,
               end
         ... ≤ (∏ i in filter prime (finset.Ico (m + 2) (2 * m + 2)), i) * 4 ^ (m + 1) :
               by exact nat.mul_le_mul_left _ (primorial_le_4_pow (m + 1))
         ... ≤ (choose (2 * m + 1) (m + 1)) * 4 ^ (m + 1) :
               begin
-                have s : ∏ i in filter prime (finset.Ico (m + 2) (2 * m + 2)), i ∣ choose (2 * m + 1) (m + 1),
+                have s : ∏ i in filter prime (finset.Ico (m + 2) (2 * m + 2)),
+                  i ∣ choose (2 * m + 1) (m + 1),
                 { refine prod_primes_dvd  (choose (2 * m + 1) (m + 1)) _ _,
                   { intros a, rw finset.mem_filter, cc, },
                   { intros a, rw finset.mem_filter,
                     intros pr,
                     rcases pr with ⟨ size, is_prime ⟩,
                     simp only [finset.Ico.mem] at size,
                     rcases size with ⟨ a_big , a_small ⟩,
-                    exact dvd_choose_of_middling_prime a is_prime m a_big (nat.lt_succ_iff.mp a_small), }, },
-                have r : ∏ i in filter prime (finset.Ico (m + 2) (2 * m + 2)), i ≤ choose (2 * m + 1) (m + 1),
+                    exact dvd_choose_of_middling_prime a is_prime m a_big
+                      (nat.lt_succ_iff.mp a_small), }, },
+                have r : ∏ i in filter prime (finset.Ico (m + 2) (2 * m + 2)),
+                  i ≤ choose (2 * m + 1) (m + 1),
                 { refine @nat.le_of_dvd _ _ _ s,
                   exact @choose_pos (2 * m + 1) (m + 1) (by linarith), },
                 exact nat.mul_le_mul_right _ r,

src/number_theory/pythagorean_triples.lean

@@ -12,8 +12,9 @@ import tactic.field_simp
 
 /-!
 # Pythagorean Triples
-The main result is the classification of pythagorean triples. The final result is for general
-pythagorean triples. It follows from the more interesting relatively prime case. We use the
+
+The main result is the classification of Pythagorean triples. The final result is for general
+Pythagorean triples. It follows from the more interesting relatively prime case. We use the
 "rational parametrization of the circle" method for the proof. The parametrization maps the point
 `(x / z, y / z)` to the slope of the line through `(-1 , 0)` and `(x / z, y / z)`. This quickly
 shows that `(x / z, y / z) = (2 * m * n / (m ^ 2 + n ^ 2), (m ^ 2 - n ^ 2) / (m ^ 2 + n ^ 2))` where
@@ -80,7 +81,8 @@ end
 
 include h
 
-/-- A pythogorean triple `x, y, z` is “classified” if there exist integers `k, m, n` such that either
+/-- A Pythagorean triple `x, y, z` is “classified” if there exist integers `k, m, n` such that
+either
  * `x = k * (m ^ 2 - n ^ 2)` and `y = k * (2 * m * n)`, or
  * `x = k * (2 * m * n)` and `y = k * (m ^ 2 - n ^ 2)`. -/
 @[nolint unused_arguments] def is_classified := ∃ (k m n : ℤ),
@@ -177,8 +179,8 @@ begin
   { apply and.intro _ co, rw one_mul, rw one_mul, tauto }
 end
 
-lemma is_classified_of_normalize_is_primitive_classified (hc : h.normalize.is_primitive_classified) :
-  h.is_classified :=
+lemma is_classified_of_normalize_is_primitive_classified
+  (hc : h.normalize.is_primitive_classified) : h.is_classified :=
 begin
   convert h.normalize.mul_is_classified (int.gcd x y)
     (is_classified_of_is_primitive_classified h.normalize hc);
@@ -281,8 +283,10 @@ begin
   rw ← int.coe_nat_dvd_left at hp1 hp2,
   have h2m : (p : ℤ) ∣ 2 * m ^ 2, { convert dvd_add hp2 hp1, ring },
   have h2n : (p : ℤ) ∣ 2 * n ^ 2, { convert dvd_sub hp2 hp1, ring },
-  have hmc : p = 2 ∨ p ∣ int.nat_abs m, { exact prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2m },
-  have hnc : p = 2 ∨ p ∣ int.nat_abs n, { exact prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2n },
+  have hmc : p = 2 ∨ p ∣ int.nat_abs m :=
+    prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2m,
+  have hnc : p = 2 ∨ p ∣ int.nat_abs n :=
+    prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2n,
   by_cases h2 : p = 2,
   { have h3 : (m ^ 2 + n ^ 2) % 2 = 1, { norm_num [pow_two, int.add_mod, int.mul_mod, hm, hn] },
     have h4 : (m ^ 2 + n ^ 2) % 2 = 0, { apply int.mod_eq_zero_of_dvd, rwa h2 at hp2 },
@@ -313,7 +317,7 @@ begin
   cases int.prime.dvd_mul hp hp2 with hp2m hpn,
   { rw int.nat_abs_mul at hp2m,
     cases (nat.prime.dvd_mul hp).mp hp2m with hp2 hpm,
-    { have hp2' : p = 2, { exact le_antisymm (nat.le_of_dvd zero_lt_two hp2) (nat.prime.two_le hp) },
+    { have hp2' : p = 2 := (nat.le_of_dvd zero_lt_two hp2).antisymm hp.two_le,
       revert hp1, rw hp2',
       apply mt int.mod_eq_zero_of_dvd,
       norm_num [pow_two, int.sub_mod, int.mul_mod, hm, hn],
@@ -417,7 +421,9 @@ begin
   { field_simp [hz, pow_two], norm_cast, exact h },
   have hvz : v ≠ 0, { field_simp [hz], exact h0 },
   have hw1 : w ≠ -1,
-  { contrapose! hvz with hw1, rw [hw1, neg_square, one_pow, add_left_eq_self] at hq, exact pow_eq_zero hq, },
+  { contrapose! hvz with hw1,
+    rw [hw1, neg_square, one_pow, add_left_eq_self] at hq,
+    exact pow_eq_zero hq, },
   have hQ : ∀ x : ℚ, 1 + x^2 ≠ 0,
   { intro q, apply ne_of_gt, exact lt_add_of_pos_of_le zero_lt_one (pow_two_nonneg q) },
   have hp : (⟨v, w⟩ : ℚ × ℚ) ∈ {p : ℚ × ℚ | p.1^2 + p.2^2 = 1 ∧ p.2 ≠ -1} := ⟨hq, hw1⟩,

src/number_theory/quadratic_reciprocity.lean

@@ -440,7 +440,8 @@ have hx2 : ∀ x ∈ Ico 1 (p / 2).succ, (2 * x : zmod p).val = 2 * x,
   from λ x hx, have h2xp : 2 * x < p,
       from calc 2 * x ≤ 2 * (p / 2) : mul_le_mul_of_nonneg_left
         (le_of_lt_succ $ by finish) dec_trivial
-      ... < _ : by conv_rhs {rw [← div_add_mod p 2, show p % 2 = 1, from hp1]}; exact lt_succ_self _,
+      ... < _ :
+        by conv_rhs {rw [← div_add_mod p 2, show p % 2 = 1, from hp1]}; exact lt_succ_self _,
     by rw [← nat.cast_two, ← nat.cast_mul, val_cast_of_lt h2xp],
 have hdisj : disjoint
     ((Ico 1 (p / 2).succ).filter (λ x, p / 2 < ((2 : ℕ) * x : zmod p).val))