How to import everything under `(mathlib)/data/nat/` ?

Stream: new members

[Michael Stoll]

Since I never know beforehand which precise files I need to import (who would have guessed that nat.odd_of_mod_four_eq_three lives in data.nat.modeq?), I would like to imprt everything related to nats (say) in one go. But import data.nat gives the error file 'data/nat' not found in the search path (whereas import tactic does work, even though tactic is a folder and not a file). So how can I get around this?

[Johan Commelin]

@Michael Stoll If there is a file some/directory/default.lean, then that will get imported if you write import some.directory.

[Johan Commelin]

But not all directories have such a file. And default.lean doesn't always import all other files in the directory either.

[Michael Stoll]

OK; this tells me why my attempt did not work. But is there a reasonable way to do it other than importing all the individual files? I guess I could write some sort of all_nat.lean file for this and import that. Is this the way to go?

[Yaël Dillies]

YOu would end up importing most of the library I suspect. $\N$ has a lot of properties.

[Eric Rodriguez]

I feel like out of all the folders, data/nat could definbitely have a default; I thought the same as Yael but I had a hunt and there's no really egregiously large file there

[Damiano Testa]

In a separate thread, Kevin said this:

You can always run ./scripts/mk_all.sh on the command line and then import all if you want to search all of mathlib.

[Michael Stoll]

BTW, generating all.lean and doing import all tends to produce excessive memory errors on things like suggestor hint...

[Michael Stoll]

(I was just typing this before Damiano replied...)

[Eric Rodriguez]

I feel like the most efficient way to search theorems in mathlib is using the regex search

[Michael Stoll]

The concrete motivation for my question is the following. I want to prove

example (p : ℕ) (hp : p % 4 = 3) : ∃ n : ℕ, p = 4*n + 3 := ?

believing that this should certainly be (in a suitably more general form) in mathlib, but I was unable to find it...

[Eric Rodriguez]

indeed, just typing % 4 finds this theorem pretty instantly

[Michael Stoll]

Where do I type % 4?

[Eric Rodriguez]

if you're using vscode, you can press the search thing on the left or press (ctrl/command)+shift+f

[Michael Stoll]

If I do that, I find lots of places where % 4 occurs in my project files, but it doesn't appear to search the library.

[Eric Rodriguez]

oh! you'll need to turn off the cog of doom

[Eric Rodriguez]

image.png

unpress that weird cog at the bottom right

[Eric Rodriguez]

(in this case though, you may enjoy docs#nat.div_add_mod, too)

[Kevin Buzzard]

Yeah, the proof is use p/4 then rw <- hp followed by library_search

[Michael Stoll]

I knew that I had seen this at some point, but wasn't able to find it again...

[Michael Stoll]

Which is an experience I'm having more and more frequently.

[Yaël Dillies]

Eric Rodriguez said:

I thought the same as Yael but I had a hunt and there's no really egregiously large file there

My point is that not all the properties of $\N$ are under data.nat..

[Michael Stoll]

And how do I do

example (p : ℕ) (hp : p % 4 = 3) : odd ((p-1)/2) := ?

Somehow I think that all these trivial elementary number theory lemmas should be much easier to obtain...

[Michael Stoll]

... than in the way I'm trying to do it.

[Yaël Dillies]

Maybe giving (p - 3)/4 as a witness of oddness is somewhat easy?

[Michael Stoll]

example (p : ℕ) (hp : p % 4 = 3) : odd ((p-1)/2) :=
begin
  have h : ∃ n : ℕ, p = 4*n + 3 := by { use p/4, rw ← hp, exact (nat.div_add_mod p 4).symm, },
  use (p-3)/4, rw [h],
  nth_rewrite 0 (by norm_num : 4 = 2*2),
  rw mul_assoc,
  simp,
end

I'm sure this can be simplified...

[Kevin Buzzard]

You are using subtraction and division of naturals so you can expect pain. Neither of these operations are mathematically well-behaved in Lean

[Michael Stoll]

I'm going to use things as exponents, so I do want naturals... Also, prime numbers are naturals in mathlib.

[Michael Stoll]

Here is finally what I wanted to achieve. I had expected this to be part of the API in number_theory.sum_two_squares, but there is really no API there. (One has to add the necessary imports.)

/-- A lemma from elementary number theory that should be in the library -/
lemma prime_eq_three_mod_four_not_dvd_sum_of_two_squares
  (p : ℕ) [fact p.prime] (hp : p % 4 = 3) (a b : ℤ) (hab : is_coprime a b) : ¬ ↑p ∣ a^2 + b^2 :=
begin
  intro h,
  -- rewrite divisibility assumption as an equality in ℤ/pℤ
  have h₁ : ((a^2 + b^2 : ℤ) : zmod p) = 0 := (zmod.int_coe_zmod_eq_zero_iff_dvd _ _).mpr h,
  push_cast at h₁,
  have h₂ : (a : zmod p)^2 = -↑b^2 := eq_neg_of_add_eq_zero h₁,
  -- The idea is now to deduce from a² = -b² in ℤ/pℤ that 1 = -1
  -- using Fermat's little theorem
  have h₃ := nat.mul_div_cancel' (div_sub_one_of_mod_two_eq_one p (nat.odd_of_mod_four_eq_three hp)),
  -- h₃ : 2*((p-1)/2) = p-1
  have h₄ : ∃ n : ℕ, p = 4*n + 3 := by { use p/4, rw ← hp, exact (nat.div_add_mod p 4).symm, },
  cases h₄ with n h₄,
  -- we need to know that `(p-1)/2` is odd
  have hodd : odd ((p-1)/2) :=
  by { use (p-3)/4, rw [h₄],
       nth_rewrite 0 (by norm_num : 4 = 2*2),
       rw mul_assoc,
       simp, },
  -- raise our equality to the `(p-1)/2`th power
  have h₅ : (a : zmod p)^(p-1) = -↑b^(p-1),
  { have h₂' : ((a : zmod p)^2)^((p-1)/2) = (-↑b^2)^((p-1)/2) :=
    congr_fun (congr_arg pow h₂) ((p - 1) / 2),
    rw [← pow_mul (↑a), neg_pow, ← pow_mul (↑b), h₃, nat.neg_one_pow_of_odd hodd, neg_one_mul] at h₂',
    exact h₂', },
  -- another bit of trivial knowledge that is needed
  have h₆ : 0 < p - 1 := by { simp [h₄], },
  -- we can apply Fermat's little theorem when `a` and `b` are nonzero in ℤ/pℤ,
  -- so we have to distinguish cases here
  by_cases ha : (a : zmod p) = 0,
  { simp [ha, zero_pow h₆] at h₅,
    -- if `a = 0` mod `p`, then `b = 0` mod `p`, so `p` divides `a` and `b`,
    -- which contradicts the coprimality assumption
    have hpa := (zmod.int_coe_zmod_eq_zero_iff_dvd a p).mp ha,
    have hpb := (zmod.int_coe_zmod_eq_zero_iff_dvd b p).mp (pow_eq_zero h₅),
    rcases hab with ⟨u, v, hab⟩,
    have hf : (p : ℤ) ∣ 1 :=
    by { rw [← hab],
         apply dvd_add,
         apply dvd_mul_of_dvd_right hpa,
         apply dvd_mul_of_dvd_right hpb, },
    norm_cast at hf,
    exact nat.prime.not_dvd_one _inst_1.1 hf, },
  { -- now the case that `a ≠ 0` mod `p`
    rw zmod.pow_card_sub_one_eq_one ha at h₅,
    -- we have to get rid of the possibility that `b = 0` mod `p`
    by_cases hb : (b : zmod p) = 0,
    { simp [hb, zero_pow h₆] at h₅,
      exact h₅, },
    { -- now both are nonzero mod `p` and we get that `1 = -1` mod `p`
      rw zmod.pow_card_sub_one_eq_one hb at h₅,
      -- it is surprisingly hard to get from this to a contradiction...
      have h₇ : ↑p ∣ (2 : ℤ) :=
      by { rw [(by norm_cast : (-1 : zmod p) = ↑(-1 : ℤ)), (by norm_cast : (1 : zmod p) = ↑(1 : ℤ))] at h₅,
           rw [zmod.int_coe_eq_int_coe_iff, int.modeq_iff_dvd] at h₅,
           norm_num at h₅,
           exact h₅, },
      norm_cast at h₇,
      have hp2 : 2 < p :=
      by { simp [h₄], apply nat.succ_lt_succ, apply nat.succ_lt_succ, exact nat.zero_lt_succ _, },
      have h₈ : p ≤ 2 := nat.le_of_dvd (nat.zero_lt_succ 1) h₇,
      revert hp2,
      exact not_lt_of_le h₈, }, },
end

This has cost me a full day! :frown: It shouldn't be that hard...

[Kevin Buzzard]

I know but wasn't it satisfying!

[Kevin Buzzard]

It might have been cheaper to deduce that -1 is a square and then use the fact (in the library) that this is false if p=3 mod 4

[Michael Stoll]

Not sure that it would be much cheaper to get to -1 being a square mod p. But feel free to suggest a more efficient proof :smile:

[Johan Commelin]

@Michael Stoll

import number_theory.sum_two_squares

/-- A lemma from elementary number theory that should be in the library -/
lemma prime_eq_three_mod_four_not_dvd_sum_of_two_squares
  (p : ℕ) [fact p.prime] (hp : p % 4 = 3) (a b : ℤ) (hab : is_coprime a b) : ¬ ↑p ∣ a^2 + b^2 :=
begin
  contrapose! hp,
  rw ← zmod.exists_sq_eq_neg_one_iff_mod_four_ne_three,
  simp only [← zmod.int_coe_zmod_eq_zero_iff_dvd, int.cast_add, int.cast_pow] at hp,
  obtain hb|hb := eq_or_ne (b : zmod p) 0,
  { simp only [hb, zero_pow', ne.def, bit0_eq_zero, nat.one_ne_zero, not_false_iff, add_zero,
      pow_eq_zero_iff, nat.succ_pos'] at hp,
    rw [zmod.int_coe_zmod_eq_zero_iff_dvd, ← int.dvd_nat_abs, int.coe_nat_dvd] at hb hp,
    rw int.coprime_iff_nat_coprime at hab,
    have h1p : 1 < p := fact.out _,
    exact (nat.not_coprime_of_dvd_of_dvd h1p hp hb hab).elim, },
  refine ⟨(a / b : zmod p), _⟩,
  field_simp [hb, eq_neg_iff_add_eq_zero, hp],
end

[Michael Stoll]

@Johan Commelin Thanks! I did not realize that nat.not_coprime_of_dvd_of_dvd was there; this saves a few extra lines...

[Johan Commelin]

Also, it suffices to case on whether (b : zmod p) is 0.

[Michael Stoll]

Yes, I saw that in your code.

[Michael Stoll]

Is there an integers version of nat.not_coprime_of_dvd_of_dvd?

[Johan Commelin]

Nope, but there should be. My proof is a bit hacky at that point.

[Johan Commelin]

Otoh, that would probably use p : ℤ. So we'd still need some glue at some point.

[Michael Stoll]

Presumably a more general version for any commutative ring would make sense.

[Johan Commelin]

Agreed. I guess it makes sense in any UFD? Or gcd_domain? I don't know precisely what's needed.

[Michael Stoll]

When dealing with primes, one has to convert between ℕ and ℤ anyway.

[Michael Stoll]

Commutative ring should be OK. The proof is the same: a | b and a | c implies a | u*b + v*c = 1 if b and c are coprime, as witnessed by u and v. The condition for a is then that a is not a unit (which is clearly a bit less nice to work with than a ≠ 1).

[Eric Rodriguez]

import field_theory.abel_ruffini

lemma coprime_of_dvd_of_dvd {R} [comm_semiring R] {d x y : R} (h : ¬ is_unit d)
  (hx : d ∣ x) (hy : d ∣ y) : ¬is_coprime x y :=
begin
  rintro ⟨a, b, hab⟩,
  apply h,
  exact is_unit_of_dvd_unit (show d ∣ 1, from hab ▸ hx.linear_comb hy a b) is_unit_one,
end

[Eric Rodriguez]

I'll leave it to you to figure out the right imports :b

[Michael Stoll]

It should better be called not_coprime_... :smile: