Zulip Chat Archive

Stream: general

Topic: some lemmas


view this post on Zulip Scott Morrison (Oct 12 2019 at 10:17):

Any opinions on adding these?

lemma int.succ_ne_self (n : ℤ) : n + 1 ≠ n :=
λ h, one_ne_zero ((add_left_inj n).mp (by { convert h, simp }))
lemma int.pred_ne_self (n : ℤ) : n - 1 ≠ n :=
λ h, one_ne_zero (neg_inj ((add_left_inj n).mp (by { convert h, simp })))

I couldn't find them in mathlib.

view this post on Zulip Chris Hughes (Oct 12 2019 at 10:24):

They're true in ring with 0 \ne 1. Maybe even semiring.

view this post on Zulip Johan Commelin (Oct 12 2019 at 10:26):

The second doesn't make sense in a semiring... for the former you need something cancellative

view this post on Zulip Scott Morrison (Oct 12 2019 at 10:28):

Does int have some typeclass already that asserts 0 \ne 1?

view this post on Zulip Scott Morrison (Oct 12 2019 at 10:29):

example : zero_ne_one_class ℤ := infer_instance

view this post on Zulip Johan Commelin (Oct 12 2019 at 10:31):

There is nonzero_comm_ring. I don't think there is nonzero_ring though.

view this post on Zulip Scott Morrison (Oct 12 2019 at 10:33):

I'll just write the lemma with [zero_ne_one_class R] and [ring R]?

view this post on Zulip Johan Commelin (Oct 12 2019 at 10:33):

I think you than have two incompatible zeros?

view this post on Zulip Johan Commelin (Oct 12 2019 at 10:33):

And two ones...

view this post on Zulip Scott Morrison (Oct 12 2019 at 10:34):

... yes.

view this post on Zulip Scott Morrison (Oct 12 2019 at 10:46):

Okay, sorted it out. Shall I put this in a separate PR? (I'm tempted to just roll it into the PR that needs these lemmas...)

view this post on Zulip Reid Barton (Oct 12 2019 at 11:57):

How about

lemma int.succ_ne_self (n : ) : n + 1  n :=
ne_of_gt n.lt_succ_self
lemma int.pred_ne_self (n : ) : n - 1  n :=
ne_of_lt n.pred_self_lt

view this post on Zulip Floris van Doorn (Oct 12 2019 at 17:53):

The first one should be done for a nonzero_comm_semiring.

view this post on Zulip Floris van Doorn (Oct 12 2019 at 17:57):

Or is it false in that case?

view this post on Zulip Reid Barton (Oct 12 2019 at 17:59):

I think {0, 1}, 1 + 1 = 1 is a semiring

view this post on Zulip Scott Morrison (Oct 13 2019 at 06:41):

I've stuck with the proof via nonzero_comm_ring, https://github.com/leanprover-community/mathlib/pull/1540/files#diff-997c56fe87e1352880681d783e610a7f, just because it's more general (but not as general as possible, which would require adjusting the algebraic hierarchy for very little gain).


Last updated: May 14 2021 at 06:16 UTC