Proving that 0 = 0 in zmod

Stream: new members

[Marc Masdeu]

I am having trouble with this simple lemma.

lemma zero_eq_zero {n : ℕ} [0 < n] {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=
begin
    sorry
end

In fact, I have been able to prove this, which I thought would already be in mathlib:

variables {n : ℕ}  [fact (0 < n)]

lemma zero_iff_n_divides (x : zmod n) : x = 0 ↔ n  ∣ x.val :=
begin
    split,
    {
        intro h,
        finish,
    },
    {
        intro h,
        cases h with w hw,
        suffices : w = 0, by finish,
        have H : x.val < n := @@zmod.val_lt _inst_1 x,
        rw hw at H,
        suffices : w < 1, by linarith,
        exact (mul_lt_iff_lt_one_right _inst_1).mp H,
    }
end

and I can't seem to prove the analogous one for integers:

variables {n : ℕ}  [fact (0 < n)]

lemma zero_iff_n_divides' (x : zmod n) : x = 0 ↔ (n : ℤ) ∣ (x : ℤ):=
begin
    split,
    {
        intro h,
        finish,
    },
    {
        intro h,
        cases h with w hw,
        suffices : w = 0,
        {
            have hw0 : (x : ℤ) = 0, by nlinarith,
            exact zero_eq_zero hw0,
        },
        sorry
    }
end

Incidentally, I don't see with the typeclass inference system doesn't work in this case (hence the two occurrences of _inst_1 in the proof). Is there something that I am overlooking?

Thank you!

[Kevin Buzzard]

Can you post a #mwe? You're missing one or more of imports, variables, opens, universes

[Kevin Buzzard]

< is not a class, so [0 < n] won't work. Inputs to functions in [square brackets] are supposed to be filled in by the type class inference system, and the type class inference system only deals with classes, so it won't deal with <.

[Kevin Buzzard]

I feel like some people might think I'm just nagging when I ask for MWE's, but I genuinely don't know what to import to get zmod and I'm too lazy to find out.

[Marc Masdeu]

That compiles in my system.

import data.zmod.basic
import tactic

open_locale classical
noncomputable theory


variables {n : ℕ}  [fact (0 < n)]

lemma zero_eq_zero  {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=
begin
    sorry
end

[Marc Masdeu]

Kevin Buzzard said:

I feel like some people might think I'm just nagging when I ask for MWE's, but I genuinely don't know what to import to get zmod and I'm too lazy to find out.

I am not one of those people.

[Kevin Buzzard]

You're using a coercion from zmod n to Z? Eew. I am surprised there is even a coercion :-)

[Marc Masdeu]

Well somewhere in Zulip I saw that it's best to work with int than with nat whenever possible.

[Kevin Buzzard]

h: ↑x = 0
⊢ x = 0

I don't know what the definition of that arrow is yet

[Kenny Lau]

Marc Masdeu said:

Well somewhere in Zulip I saw that it's best to work with int than with nat whenever possible.

that surely highly depends on context

[Kenny Lau]

I say that if you're in zmod you shouldn't coerce to int

[Kenny Lau]

or to nat

[Kevin Buzzard]

If you plan to do subtractions you shouldn't be using nat because it doesn't have a subtraction (it's a semiring, not a ring)

[Patrick Massot]

Kevin Buzzard said:

h: ↑x = 0
⊢ x = 0

I don't know what the definition of that arrow is yet

Kevin, we longer have this issue since Ed offered us magic widgets.

[Patrick Massot]

Just click on the arrow.

[Marc Masdeu]

What I want is an easy way to go from x=y (in zmod n) to n dividing x'-y', where x' and y' are lifts to integers. So here is where subtraction appears.

[Kenny Lau]

when we say "lift", we choose x' first

[Kevin Buzzard]

what are x' and y'? Are they arbitrary? Is this a theorem about x and y, or about x' and y'?

[Kenny Lau]

i.e. rather than using the standard lift that isn't canonical, instead let the integer be the variable

[Kenny Lau]

so the "correct" theorem should say that for x y : Z, (x : zmod n) = y <-> n | (x - y)

[Kevin Buzzard]

uparrow2.png

[Kenny Lau]

coercing from int to zmod is good; from zmod to int is bad

[Kevin Buzzard]

@Patrick Massot I said I didn't know the definition precisely because this trick told me nothing

[Kevin Buzzard]

#check (by apply_instance : has_lift (zmod n) ℤ)
/-
tactic.mk_instance failed to generate instance for
  has_lift (zmod n) ℤ
-/

[Kevin Buzzard]

I've never understood the zoo of lifts and coercions properly

[Patrick Massot]

The trick tells you this is coercion from zmod n to int, that's infinitely more information than what you would have had before widgets.

[Kevin Buzzard]

#check (by apply_instance : has_coe (zmod n) ℤ)
/-
tactic.mk_instance failed to generate instance for
  has_coe (zmod n) ℤ
-/

[Kevin Buzzard]

Patrick Massot said:

The trick tells you this is coercion from zmod n to int, that's infinitely more information than what you would have had before widgets.

I already knew that from the lemma statement lemma zero_eq_zero {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=

[Kevin Buzzard]

I genuinely don't know how to work out what the map is

[Kevin Buzzard]

oh -- I keep going with the widgets!

[Kevin Buzzard]

tada.png

[Kenny Lau]

what is that cursed instance

[Kevin Buzzard]

/-- Cast an integer modulo `n` to another semiring.
This function is a morphism if the characteristic of `R` divides `n`.
See `zmod.cast_hom` for a bundled version. -/
def cast : Π {n : ℕ}, zmod n → R
| 0     := int.cast
| (n+1) := λ i, i.val

-- see Note [coercion into rings]
@[priority 900] instance (n : ℕ) : has_coe_t (zmod n) R := ⟨cast⟩

@[simp] lemma cast_zero : ((0 : zmod n) : R) = 0 :=
by { cases n; refl }

[Rob Lewis]

@Kevin Buzzard https://github.com/leanprover-community/mathlib/pull/3882#discussion_r475005206

[Kevin Buzzard]

This coercion has no good ring-theoretic properties. @Rob Lewis the Teichmuller lift is at least a homomorphism of monoids with zero :-)

[Marc Masdeu]

OK I'll try to explain myself a bit better. I was trying to prove

variables {p r n m: ℕ} [fact p.prime] [fact (0 < n)] [fact (0 < m)] [1 ≤ r]

lemma basic_lemma (x : zmod (p^r)) (h : x * x = 1) : (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
   sorry
end

This is a statement about elements all in zmod (either p or p^r). It seems that it should be very easy, but I got this so far:

lemma basic_lemma (x : zmod (p^r)) (h : x * x = 1) : (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
    have hp : nat.prime p, by assumption,
    have  h1 : (p : ℤ)^r ∣ ((x.val : ℤ) * (x.val : ℤ) - 1),
    {
        have h' :  x * x -1 = 0 := sub_eq_zero.mpr h,
        --rw_mod_cast zmod.int_coe_zmod_eq_zero_iff_dvd at h',
        sorry
    },
    have h2 : (p : ℤ) ∣ ((x.val : ℤ) * (x.val : ℤ) - 1),
    {
        cases h1 with w h1w,
        rw h1w,
        ring,
        fconstructor,
        use (p^(r-1)) * w,
        rw ← int.mul_assoc,
        have hp : (p : ℤ)^r = p * p^(r-1),
        {
            induction r with d hd,
            {
                linarith,
            },
            {
                ring,
                ring,
            }
        },
        rw ←hp,
        rw int.mul_comm,
    },
    have h3 : (p : ℤ) ∣ ((x.val : ℤ) - 1) ∨ (p : ℤ) ∣ (x.val : ℤ) + 1,
    {
        have hfac : (x.val : ℤ) * (x.val : ℤ) - 1
                    = ((x.val:ℤ) - 1) * ((x.val:ℤ) + 1) := by ring,
        rw hfac at h2,
        apply int.prime.dvd_mul' hp h2,
    },
    cases h3 with h3l h3r,
    {
        left,
        suffices : (x : zmod p) - 1 = 0, by exact sub_eq_zero.mp this,
        rw← zmod.int_coe_zmod_eq_zero_iff_dvd (((x.val):ℤ)-1) p at h3l,
        push_cast at *,
        rw @@x_val_trans _inst_1 _inst_4 at h3l,
        exact h3l,
    },
    {
        right,
        suffices : (x : zmod p) + 1 = 0, by exact eq_neg_of_add_eq_zero this,
        rw← zmod.int_coe_zmod_eq_zero_iff_dvd (((x.val):ℤ) + 1) p at h3r,
        push_cast at *,
        rw @@x_val_trans _inst_1 _inst_4 at h3r,
        exact h3r,
    }
end

So I find myself trying to prove

↑p ^ r ∣ ↑(x.val) * ↑(x.val) - 1

in the realm of int...

[Kevin Buzzard]

To prove the basic lemma, let xbar be x mod p and deduce that xbar^2=1 and then you're done because zmod p is a field, right?

[Marc Masdeu]

This was my math proof, but I had a bit more trouble writing it in Lean!

[Kenny Lau]

@Kevin Buzzard right, so the problem is how to coerce from zmod (p^r) to zmod p

[Kenny Lau]

now that cursed instance seems like a good candidate

[Kenny Lau]

because zmod p does have characteristic dividing p^r

[Marc Masdeu]

But @Kenny Lau this coercion should be simple, right?

[Kenny Lau]

so maybe zmod.cast_hom would help

[Kevin Buzzard]

In the situation where the coercion is ring-theoretically reasonable one should use the ring-theoretic coercion I guess

[Kenny Lau]

I feel like this is still #xy

[Kenny Lau]

the "basic lemma" has a coercion from zmod (p^r) to zmod p

[Kenny Lau]

what demanded this coercion to start with?

[Kevin Buzzard]

There is no API for it and it's a horrible function, so it's horrible to use.

[Marc Masdeu]

OK the feeling I had throughout is that zmod's API is not quite working yet. It is very hard to work with it, since it has references to %, to MOD, ...

[Marc Masdeu]

Kenny Lau said:

I feel like this is still #xy

You got me. I want to prove that in Z/p^r (p odd) the only solutions to x^2-1=0 are 1 and -1. The way I can prove this is to lift x to x'=+-1 + e, with e being a multiple of p (hence the basic lemma). Then I prove that p^r divides e, here is where I use that p is odd.

[Kevin Buzzard]

right, that looks like the standard proof.

[Marc Masdeu]

I might start from scratch...

[Kevin Buzzard]

rofl cast uses nat.cast_coe because it's coercing to a general ring, as opposed to the standard coercion from nat to int.

[Kevin Buzzard]

so the issue is to prove that nat.cast_coe is injective when going from nat to int.

[Kevin Buzzard]

import data.zmod.basic
import tactic

open_locale classical
noncomputable theory


variables {n : ℕ} [fact (0 < n)]

lemma zero_eq_zero  {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=
begin
  -- this workaround is because you're using `fact`
  tactic.unfreeze_local_instances,
  -- deal with n = 0 case
  cases n with d, cases _inst_1,
  -- now n = d + 1
  -- now take x apart
  cases x with a ha,
  -- now a is a natural
  ext, dsimp,
  -- and it suffices to prove a = 0,
  unfold_coes at h,
  -- zmod.cast has no API because nobody uses it
  rw zmod.cast.equations._eqn_2 at h,
  -- We know the usual map ℕ → ℤ is injective
  rw ←int.coe_nat_eq_zero,
  -- so we would be done by h
  convert h,
  -- except we now have to prove that the two coercions ℕ → ℤ are equal.
  apply congr_arg has_coe_t.mk,
  ext n,
  -- we prove it by induction
  induction n with d hd,
  { refl },
  { unfold nat.cast,
    rw ←hd,
    refl }
end

You're really fighting the system here because the casts don't have too much API

[Johan Commelin]

My apologies for the awful coercion. I don't know how to improve it.

[Marc Masdeu]

Wow! That is incredibly hard!! Thanks @Kevin Buzzard, this is the kind of thing that throw some people off...

[Kevin Buzzard]

Because it's so general it's hard to find lemmas about it.

[Kevin Buzzard]

What's going on here Marc is that there is a map from Z/nZ to any ring given by literally sending 0,1,2,...,n-1 to 0,1,2,...,n-1. There aren't really any lemmas you can prove about it.

[Kevin Buzzard]

However, for a given ring like the integers, there are lemmas you can prove (for example injectivity)

[Kevin Buzzard]

but these lemmas are not proved, as far as I can see.

[Kevin Buzzard]

because probably there are a million such lemmas. We know that "if x is in Z/nZ then lift x to Z" is a reasonable thing to do

[Kevin Buzzard]

but "if x is in Z/nZ then randomly map it to Z/mZ" is perhaps not so common

[Marc Masdeu]

I see. Yes, the general map is a bit dumb, but it's very common as you know in arithmetic to lift elements in Z/n to Z and then prove things about those lifts, so it'd be useful to have some lemmas about this.

[Kevin Buzzard]

It might be interesting @Johan Commelin to see how many times in the library this map is used when the target ring is not nat or int. If people are only using it to lift from Z/n to Z (this is Marc's use case and also yours in the PR) then perhaps it's worth restricting to that case and then writing the API which Marc needed here.

[Marc Masdeu]

Maybe it'd be best to do as in mathlib, start with integers and prove things about their images in various zmods

[Kevin Buzzard]

right, that's another way of thinking about it.

[Kevin Buzzard]

There is congruence mod n in mathlib, and it's an equivalence relation on integers

[Kevin Buzzard]

and that has a whole file of API, a very solid one.

[Marc Masdeu]

Yes, I will want to work with the ring (and its units) zmod n, so I'd rather not think in terms of equivalence relations...

[Kevin Buzzard]

I feel like lifting from Z/p^n to Z/p^(n+1) is still a useful thing though

[Marc Masdeu]

Ideally, it would be easy to go back and forth between all these objects.

[Kevin Buzzard]

but I would be strongly tempted here not to use the cast. It is easy to go back and forth between these objects, because you can do it directly without using the coercion.

[Marc Masdeu]

I'll try...

[Kevin Buzzard]

If n>0 then a term of type zmod n is just a pair (a,h) with a a natural and h a proof that it's less than n. So you can just use (a,h') to move from Z/n to Z/(pn) where h' is a proof that a<pn manufactured from the proof that it's less than n

[Kevin Buzzard]

It would be very easy to prove things about that map because it's defined concretely on the level of integers without using nat.cast or zmod.cast

[Kevin Buzzard]

I can't find x^2=1 -> x=+-1 in a field

[Bryan Gin-ge Chen]

There's docs#mul_self_eq_one_iff

[Kevin Buzzard]

import data.zmod.basic
import tactic

open_locale classical
noncomputable theory

#check zmod.cast_hom


variables {p r n m: ℕ} (hp : p.prime) (hn : 0 < n) (hm : 0 < m) (hr : 0 < r)

lemma div_pow (p : ℕ) {r : ℕ} (hr : 0 < r) : p ∣ p^r :=
begin
  -- do a case split on r=0 or r=s+1
  cases r with s,
  { -- r=0 can't happen
    cases hr },
  { -- r = s + 1 so we can use nat.pow_succ
    rw nat.pow_succ,
    -- library_search found the next line
    apply dvd_mul_left,
  }
end

include hp hn hm hr

lemma basic_lemma (x : zmod (p^r)) (h : x * x = 1) :
  (x : zmod p) = 1 ∨ (x : zmod p) = -1 :=
begin
  let f := zmod.cast_hom (div_pow p hr) (zmod p), -- the ring hom
  set xp := f x with hxp,
  have hxpsquared : xp * xp = 1,
  { rw hxp,
    rw ←f.map_mul,
    rw h,
    exact f.map_one,
  },
  haveI : fact p.prime := hp,
  convert mul_self_eq_one_iff.1 hxpsquared,
end

[Johan Commelin]

Note that mathlib knows that coe : int → zmod n is surjective. In fact it knows that arbitrary ring homs to zmod n are surjective.

[Johan Commelin]

I guess that might be helpful...

[Johan Commelin]

But I haven't thought about the details of what's going on here.

[Mario Carneiro]

import data.zmod.basic

theorem cast_inj : ∀ {i}, function.injective (coe : zmod i → int)
| 0 := λ a b, by simp
| (n+1) := λ a b h, fin.val_injective (nat.cast_inj.1 h)

lemma zero_eq_zero {n} {x : zmod n} (h : (x : ℤ) = 0) : x = 0 :=
cast_inj (h.trans $ by simp)

[Kevin Buzzard]

Right! And now if we want to prove it for rationals, you have to prove a whole new cast_inj :-(

[Mario Carneiro]

I tried to generalize it but char_p wasn't built to handle this

[Mario Carneiro]

I don't know how to say "R is a ring with the first n elements distinct"

[Mario Carneiro]

Anyway this proof doesn't really generalize because the zero case uses int.cast_id

[Mario Carneiro]

so a different ring would actually be substantively different

[Marc Masdeu]

Thanks for the discussion. I am slowly understanding how this is working...