one_ne_zero in commutative rings: funny types

Stream: maths

[Julian Gilbey]

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!

[Johan Commelin]

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

[Johan Commelin]

I completely understand your confusion.

[Johan Commelin]

Short answer: use nonzero_comm_ring and remove zero_ne_one_class

[Johan Commelin]

Then everything should work fine.

[Johan Commelin]

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.

[Johan Commelin]

In other words, zero_ne_one_class is completely useless

[Johan Commelin]

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

[Julian Gilbey]

Aww, thanks!!

[Johan Commelin]

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

[Julian Gilbey]

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!

[Johan Commelin]

Which instances do you now have?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Julian Gilbey]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Julian Gilbey]

Woo-hoo, thanks!!

[Julian Gilbey]

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 ;-)

[Kevin Buzzard]

Yes but there would still be visibly too many instances

[Mario Carneiro]

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

[Johan Commelin]

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