Zulip Chat Archive

Stream: maths

Topic: one_ne_zero in commutative rings: funny types


view this post on Zulip Julian Gilbey (Feb 19 2020 at 17:31):

I'm playing with lean, and trying to prove an "easy" result, namely that nilpotent elements are zero divisors. I've got very stuck, though, trying to prove that 1 is not 0. Here's where I've got to...

variables {α : Type u} [comm_ring α]

def zero_divisor (x : α) :=  z, z  0  z * x = 0

def nilpotent (x : α) :=  n : nat, n > 0  x^n = 0

-- set_option pp.all true
lemma zero_divisor_of_nilpotent { x : α } [ decidable_eq α ] [ zero_ne_one_class α ]
  (h : nilpotent (x : α)) : zero_divisor x :=
begin
  simp [nilpotent, zero_divisor] at *,
  obtain m, mprop := nat.find_x h,
  cases m with d,
    exfalso,
    exact (nat.not_lt_zero _ mprop.left.left),
  use (x ^ d),
  split,
    have := ((mprop.right d) (nat.lt_succ_self d)),
    intros h1,
    cases d with e,
      simp at h1,
      have h0 : (1 : α)  0, exact one_ne_zero,
      sorry,
    sorry,
  sorry,
end

At this point (the first sorry), I just want to say exact h0 h1. But though they appear to be the right things, they are completely different, as shown by pp.all, and this application of exact completely fails. How on earth do I use one_ne_zero, then?!

Thanks!

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:33):

@Julian Gilbey I think an apology is in place... the library is very bad here.

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:33):

I completely understand your confusion.

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:33):

Short answer: use nonzero_comm_ring and remove zero_ne_one_class

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:33):

Then everything should work fine.

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:35):

Long answer: zero_ne_one_class is not a "property", but it includes the data of an element 0, an element 1 + the assertion that they are not equal. But these elements 0 and 1 are completely unrelated from the 0 and 1 provided by comm_ring.

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:35):

In other words, zero_ne_one_class is completely useless

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:35):

(Except that there are some technical reasons why one might want it for library development.)

view this post on Zulip Julian Gilbey (Feb 19 2020 at 17:35):

Aww, thanks!!

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:35):

But for end users... it's just useless

view this post on Zulip Julian Gilbey (Feb 19 2020 at 17:42):

It doesn't seem to have helped, though. I've changed zero_ne_one_class to nonzero_comm_ring, and then changed this part of the argument to

      simp at h1,
      have h0 : 0  (1 : α), exact zero_ne_one,
      exact h0 h1.symm,

but it's equally unhappy. How to I get the "correct" version of zero_ne_one, or do I need to so something different?

Thanks!

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:43):

Which instances do you now have?

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:43):

Can you copy-paste your tactic state? (I.e., the goal window)

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:44):

My guess is that it is still finding the wrong 0 and 1 because you have too many such elements.

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:45):

@Julian Gilbey There should be no comm_ring \alpha left in your code. Only nonzero_comm_ring \alpha.

view this post on Zulip Julian Gilbey (Feb 19 2020 at 17:45):

It's long...

3 goals
case nat.zero
α : Type u,
_inst_1 : comm_ring.{u} α,
x : α,
_inst_2 : decidable_eq.{u+1} α,
_inst_3 : nonzero_comm_ring.{u} α,
h :
  @Exists.{1} nat
    (λ (n : nat),
       and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
         (@eq.{u+1} α
            (@has_pow.pow.{u 0} α nat
               (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
               x
               n)
            (@has_zero.zero.{u} α
               (@mul_zero_class.to_has_zero.{u} α
                  (@semiring.to_mul_zero_class.{u} α
                     (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1))))))),
mprop :
  and
    ((λ (n : nat),
        and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
          (@eq.{u+1} α
             (@has_pow.pow.{u 0} α nat
                (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
                x
                n)
             (@has_zero.zero.{u} α
                (@mul_zero_class.to_has_zero.{u} α
                   (@semiring.to_mul_zero_class.{u} α
                      (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))))
       (nat.succ nat.zero))
    ( (m : nat),
       @has_lt.lt.{0} nat nat.has_lt m (nat.succ nat.zero) 
       not
         ((λ (n : nat),
             and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
               (@eq.{u+1} α
                  (@has_pow.pow.{u 0} α nat
                     (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
                     x
                     n)
                  (@has_zero.zero.{u} α
                     (@mul_zero_class.to_has_zero.{u} α
                        (@semiring.to_mul_zero_class.{u} α
                           (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))))
            m)),
this :
  not
    ((λ (n : nat),
        and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
          (@eq.{u+1} α
             (@has_pow.pow.{u 0} α nat
                (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
                x
                n)
             (@has_zero.zero.{u} α
                (@mul_zero_class.to_has_zero.{u} α
                   (@semiring.to_mul_zero_class.{u} α
                      (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))))
       nat.zero),
h1 :
  @eq.{u+1} α
    (@has_one.one.{u} α (@monoid.to_has_one.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1))))
    (@has_zero.zero.{u} α
       (@mul_zero_class.to_has_zero.{u} α
          (@semiring.to_mul_zero_class.{u} α (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))
 false

case nat.succ
α : Type u,
_inst_1 : comm_ring.{u} α,
x : α,
_inst_2 : decidable_eq.{u+1} α,
_inst_3 : nonzero_comm_ring.{u} α,
h :
  @Exists.{1} nat
    (λ (n : nat),
       and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
         (@eq.{u+1} α
            (@has_pow.pow.{u 0} α nat
               (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
               x
               n)
            (@has_zero.zero.{u} α
               (@mul_zero_class.to_has_zero.{u} α
                  (@semiring.to_mul_zero_class.{u} α
                     (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1))))))),
e : nat,
mprop :
  and
    ((λ (n : nat),
        and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
          (@eq.{u+1} α
             (@has_pow.pow.{u 0} α nat
                (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
                x
                n)
             (@has_zero.zero.{u} α
                (@mul_zero_class.to_has_zero.{u} α
                   (@semiring.to_mul_zero_class.{u} α
                      (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))))
       (nat.succ (nat.succ e)))
    ( (m : nat),
       @has_lt.lt.{0} nat nat.has_lt m (nat.succ (nat.succ e)) 
       not
         ((λ (n : nat),
             and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
               (@eq.{u+1} α
                  (@has_pow.pow.{u 0} α nat
                     (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
                     x
                     n)
                  (@has_zero.zero.{u} α
                     (@mul_zero_class.to_has_zero.{u} α
                        (@semiring.to_mul_zero_class.{u} α
                           (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))))
            m)),
this :
  not
    ((λ (n : nat),
        and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
          (@eq.{u+1} α
             (@has_pow.pow.{u 0} α nat
                (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
                x
                n)
             (@has_zero.zero.{u} α
                (@mul_zero_class.to_has_zero.{u} α
                   (@semiring.to_mul_zero_class.{u} α
                      (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))))
       (nat.succ e)),
h1 :
  @eq.{u+1} α
    (@has_pow.pow.{u 0} α nat (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1))) x
       (nat.succ e))
    (@has_zero.zero.{u} α
       (@mul_zero_class.to_has_zero.{u} α
          (@semiring.to_mul_zero_class.{u} α (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))
 false

α : Type u,
_inst_1 : comm_ring.{u} α,
x : α,
_inst_2 : decidable_eq.{u+1} α,
_inst_3 : nonzero_comm_ring.{u} α,
h :
  @Exists.{1} nat
    (λ (n : nat),
       and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
         (@eq.{u+1} α
            (@has_pow.pow.{u 0} α nat
               (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
               x
               n)
            (@has_zero.zero.{u} α
               (@mul_zero_class.to_has_zero.{u} α
                  (@semiring.to_mul_zero_class.{u} α
                     (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1))))))),
d : nat,
mprop :
  and
    ((λ (n : nat),
        and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
          (@eq.{u+1} α
             (@has_pow.pow.{u 0} α nat
                (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
                x
                n)
             (@has_zero.zero.{u} α
                (@mul_zero_class.to_has_zero.{u} α
                   (@semiring.to_mul_zero_class.{u} α
                      (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))))
       (nat.succ d))
    ( (m : nat),
       @has_lt.lt.{0} nat nat.has_lt m (nat.succ d) 
       not
         ((λ (n : nat),
             and (@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) n)
               (@eq.{u+1} α
                  (@has_pow.pow.{u 0} α nat
                     (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
                     x
                     n)
                  (@has_zero.zero.{u} α
                     (@mul_zero_class.to_has_zero.{u} α
                        (@semiring.to_mul_zero_class.{u} α
                           (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))))
            m))
 @eq.{u+1} α
    (@has_mul.mul.{u} α
       (@mul_zero_class.to_has_mul.{u} α
          (@semiring.to_mul_zero_class.{u} α (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1))))
       (@has_pow.pow.{u 0} α nat (@monoid.has_pow.{u} α (@ring.to_monoid.{u} α (@comm_ring.to_ring.{u} α _inst_1)))
          x
          d)
       x)
    (@has_zero.zero.{u} α
       (@mul_zero_class.to_has_zero.{u} α
          (@semiring.to_mul_zero_class.{u} α (@ring.to_semiring.{u} α (@comm_ring.to_ring.{u} α _inst_1)))))

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:45):

_inst_1 : comm_ring.{u} α, is the culprit.

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:45):

Oooh, you could paste it without pp.all set to true.

view this post on Zulip Johan Commelin (Feb 19 2020 at 17:46):

Remove [comm_ring \alpha] from your variables, and you should be good to go.

view this post on Zulip Julian Gilbey (Feb 19 2020 at 17:49):

Woo-hoo, thanks!!

view this post on Zulip Julian Gilbey (Feb 19 2020 at 17:50):

Johan Commelin said:

Oooh, you could paste it without pp.all set to true.

Without pp.all set to true, it just said that both h0 and h1 said 0 (not) equal to 1, so didn't give any hint as to what was wrong ;-)

view this post on Zulip Kevin Buzzard (Feb 19 2020 at 18:08):

Yes but there would still be visibly too many instances

view this post on Zulip Mario Carneiro (Feb 19 2020 at 20:06):

Johan Commelin said:

Long answer: zero_ne_one_class is not a "property", but it includes the data of an element 0, an element 1 + the assertion that they are not equal. But these elements 0 and 1 are completely unrelated from the 0 and 1 provided by comm_ring.

In other words, zero_ne_one_class is completely useless

Interestingly, a comm ring with two random elements unequal is a nonzero ring, since a zero ring is a singleton. So it does work! (although you may have to get the order of the two instances right so that you get 0 and 1 coming from the comm_ring instead of the random values in the zero_ne_one_class.)

view this post on Zulip Johan Commelin (Feb 19 2020 at 20:07):

Ok, sure... but this is a very convoluted way of getting there...


Last updated: May 09 2021 at 10:11 UTC