Zulip Chat Archive

Stream: new members

Topic: Proving that 0 = 0 in zmod


view this post on Zulip Marc Masdeu (Aug 26 2020 at 13:55):

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!

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 13:57):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 13:58):

< 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 <.

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:00):

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.

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:00):

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

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:01):

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.

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:01):

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

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:03):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:03):

h: x = 0
 x = 0

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:04):

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:04):

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:04):

or to nat

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:04):

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)

view this post on Zulip Patrick Massot (Aug 26 2020 at 14:05):

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.

view this post on Zulip Patrick Massot (Aug 26 2020 at 14:05):

Just click on the arrow.

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:05):

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.

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:05):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:06):

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:06):

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:06):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:06):

uparrow2.png

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:06):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:06):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:07):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:07):

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

view this post on Zulip Patrick Massot (Aug 26 2020 at 14:07):

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.

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:08):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:08):

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 :=

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:08):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:10):

oh -- I keep going with the widgets!

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:10):

tada.png

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:11):

what is that cursed instance

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:12):

/-- 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 }

view this post on Zulip Rob Lewis (Aug 26 2020 at 14:12):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:14):

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

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:14):

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...

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:16):

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?

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:17):

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:17):

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:17):

now that cursed instance seems like a good candidate

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:18):

because zmod p does have characteristic dividing p^r

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:18):

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:18):

so maybe zmod.cast_hom would help

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:20):

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:20):

I feel like this is still #xy

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:21):

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 14:21):

what demanded this coercion to start with?

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:21):

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

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:22):

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, ...

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:25):

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.

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:26):

right, that looks like the standard proof.

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:30):

I might start from scratch...

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:39):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:40):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:49):

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

view this post on Zulip Johan Commelin (Aug 26 2020 at 14:53):

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

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:53):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:53):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:54):

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.

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:54):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:55):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:55):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:56):

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

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:56):

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.

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:57):

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.

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:57):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:58):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:58):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:58):

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

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:59):

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...

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:59):

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

view this post on Zulip Marc Masdeu (Aug 26 2020 at 14:59):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 15:00):

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.

view this post on Zulip Marc Masdeu (Aug 26 2020 at 15:00):

I'll try...

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 15:01):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 15:02):

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 15:10):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 26 2020 at 15:13):

There's docs#mul_self_eq_one_iff

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 15:16):

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

view this post on Zulip Johan Commelin (Aug 26 2020 at 15:52):

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

view this post on Zulip Johan Commelin (Aug 26 2020 at 15:52):

I guess that might be helpful...

view this post on Zulip Johan Commelin (Aug 26 2020 at 15:52):

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

view this post on Zulip Mario Carneiro (Aug 26 2020 at 17:30):

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)

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 17:31):

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

view this post on Zulip Mario Carneiro (Aug 26 2020 at 17:32):

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

view this post on Zulip Mario Carneiro (Aug 26 2020 at 17:32):

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

view this post on Zulip Mario Carneiro (Aug 26 2020 at 17:34):

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

view this post on Zulip Mario Carneiro (Aug 26 2020 at 17:34):

so a different ring would actually be substantively different

view this post on Zulip Marc Masdeu (Aug 26 2020 at 18:25):

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


Last updated: May 15 2021 at 22:14 UTC