## Stream: maths

### Topic: one_ne_zero in commutative rings: funny types

#### 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!

#### Johan Commelin (Feb 19 2020 at 17:33):

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

#### Johan Commelin (Feb 19 2020 at 17:33):

Short answer: use nonzero_comm_ring and remove zero_ne_one_class

#### Johan Commelin (Feb 19 2020 at 17:33):

Then everything should work fine.

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

#### Johan Commelin (Feb 19 2020 at 17:35):

In other words, zero_ne_one_class is completely useless

#### Johan Commelin (Feb 19 2020 at 17:35):

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

Aww, thanks!!

#### Johan Commelin (Feb 19 2020 at 17:35):

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

#### 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!

#### Johan Commelin (Feb 19 2020 at 17:43):

Which instances do you now have?

#### Johan Commelin (Feb 19 2020 at 17:43):

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

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

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

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


#### Johan Commelin (Feb 19 2020 at 17:45):

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

#### Johan Commelin (Feb 19 2020 at 17:45):

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

#### Johan Commelin (Feb 19 2020 at 17:46):

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

#### Julian Gilbey (Feb 19 2020 at 17:49):

Woo-hoo, thanks!!

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

#### Kevin Buzzard (Feb 19 2020 at 18:08):

Yes but there would still be visibly too many instances

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

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