Stream: new members

Topic: mul_left_cancel for integral domains

Damiano Testa (Sep 21 2020 at 11:46):

Dear All,

I would like to use the fact that in an integral domain, every non-zero element is left-cancellable (see the #mwe below). Is this lemma already in mathlib and I have simply been unable to find it?

Thank you!

import tactic

lemma xxv {R : Type*} [comm_ring R] [is_integral_domain R] {x y z : R} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
sorry,
end


Johan Commelin (Sep 21 2020 at 11:47):

mul_left_cancel hopefully?

Johan Commelin (Sep 21 2020 at 11:48):

Maybe with a ', if the other version is for groups

Damiano Testa (Sep 21 2020 at 11:50):

I tried, but I was unable to make it work...

Kevin Buzzard (Sep 21 2020 at 11:51):

I'll give it a go

Shing Tak Lam (Sep 21 2020 at 11:52):

If you change is_integral_domain to integral_domain, then mul_left_cancel' works btw

Kevin Buzzard (Sep 21 2020 at 11:52):

Aah, that's the issue: is_integral_domain isn't the way to say an integral domain.

Damiano Testa (Sep 21 2020 at 11:52):

Shing Tak Lam said:

If you change is_integral_domain to integral_domain, then mul_left_cancel' works btw

Ah, this might fix it for me, then!

Kevin Buzzard (Sep 21 2020 at 11:52):

You should delete comm_ring R and use integral_domain R

Let me try!

Damiano Testa (Sep 21 2020 at 11:56):

I am trying

lemma xxv [integral_domain R] {x y z : R} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
apply mul_left_cancel',
exact h,
end


but I get this error:

invalid type ascription, term has type
x ≠ 0
but is expected to have type
x ≠ 0
state:
R : Type u_1,
_inst_1 : semiring R,
_inst_2 : integral_domain R,
x y z : R,
h : x ≠ 0
⊢ x ≠ 0


Kevin Buzzard (Sep 21 2020 at 11:58):

import tactic

lemma xxv (R : Type) [integral_domain R] {x y z : R} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
apply mul_left_cancel',
exact h,
end


works for me.

Shing Tak Lam (Sep 21 2020 at 11:59):

I'm not sure why, but I think the semiring R instance is affecting things

Shing Tak Lam (Sep 21 2020 at 11:59):

you probably have variable [semiring R] somewhere? I can reproduce the error if I add a semiring R typeclass

import tactic

lemma xxv {R : Type*} [semiring R] [integral_domain R] {x y z : R} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
apply mul_left_cancel',
exact h, -- Same error
end


Damiano Testa (Sep 21 2020 at 12:00):

Yes, my standing assumption is that R is a semiring

Interesting

Reid Barton (Sep 21 2020 at 12:01):

I wonder if it's worth trying to improve these error messages, or we should just wait for :four_leaf_clover:

Kevin Buzzard (Sep 21 2020 at 12:01):

But an integral domain is a semiring so you should maybe just start afresh with some new variable which is an integral domain

Damiano Testa (Sep 21 2020 at 12:01):

I will remove this assumption now. In case someone is further interested, here is what happens if I try to convert h. Lean wants me to prove:

⊢ cancel_monoid_with_zero.to_monoid_with_zero R = semiring.to_monoid_with_zero R


Johan Commelin (Sep 21 2020 at 12:01):

Yup, but those are two completely different 0s (-;

Kevin Buzzard (Sep 21 2020 at 12:02):

You can't prove this, because one has come from [semiring R] and one has come from [integral_domain R]. That's exactly the difference between integral_domain and is_integral_domain

Johan Commelin (Sep 21 2020 at 12:02):

You assumed two semiring instances (one coming from the integral domain) but Lean doesn't know any compatibility between them.

Damiano Testa (Sep 21 2020 at 12:02):

Ok, I will remove the semiring assumption

Kevin Buzzard (Sep 21 2020 at 12:02):

You should remove the [semiring R] assumption because type class inference knows that an integral domain is a semiring

Kevin Buzzard (Sep 21 2020 at 12:03):

so all the stuff you just proved about semirings will all work fine when you're rewriting it in some lemmas about integral domains

Damiano Testa (Sep 21 2020 at 12:04):

Thank you all for the help! For the record, this now is a working lemma:

lemma xxv {RR : Type*} [integral_domain RR] {x y z : RR} {h : x ≠ 0} : x*y=x*z → y=z :=
begin
apply mul_left_cancel' h,
end


Kevin Buzzard (Sep 21 2020 at 12:04):

now see if you can do it in term mode :-)

Damiano Testa (Sep 21 2020 at 12:06):

I would love to, but I would need to learn how to communicate to Lean in term mode... Ahahaha

Reid Barton (Sep 21 2020 at 12:07):

hint: the term-mode proof is a substring of the tactic proof

Damiano Testa (Sep 21 2020 at 12:10):

Ok, I am making the guess that I should remove characters from apply , since I imagine that the name of the lemmas in mathlib appear identically in term mode!

Johan Commelin (Sep 21 2020 at 12:10):

begin means entering tactic mode

Johan Commelin (Sep 21 2020 at 12:10):

and end stops it.

Johan Commelin (Sep 21 2020 at 12:11):

Indeed, apply takes a little bit of term mode as argument, and does something useful with it.

Damiano Testa (Sep 21 2020 at 12:11):

ah, so i should remove from begin apply [] end

I will keep by! Ahahaha

Johan Commelin (Sep 21 2020 at 12:11):

No by also enters tactic mode

Reid Barton (Sep 21 2020 at 12:12):

To be more specific, a consecutive substring :upside_down:

Kevin Buzzard (Sep 21 2020 at 12:12):

by {...} and begin ... end are the two ways to enter tactic mode from term mode. exact ... is the way to enter term mode from tactic mode.

Johan Commelin (Sep 21 2020 at 12:13):

@Damiano Testa Did you know that mul_left_cancel' is a function?

Johan Commelin (Sep 21 2020 at 12:13):

Your lemma xxv is also a function

Reid Barton (Sep 21 2020 at 12:21):

Regarding the error, if you set_option pp.numerals false, then you get an error which shows the issue:

error: invalid type ascription, term has type
x ≠
@has_zero.zero R
(@mul_zero_class.to_has_zero R (@monoid_with_zero.to_mul_zero_class R (@semiring.to_monoid_with_zero R _inst_1)))
but is expected to have type
x ≠
@has_zero.zero R
(@mul_zero_class.to_has_zero R
(@monoid_with_zero.to_mul_zero_class R
(@cancel_monoid_with_zero.to_monoid_with_zero R
(@domain.to_cancel_monoid_with_zero R (@integral_domain.to_domain R _inst_2)))))


Reid Barton (Sep 21 2020 at 12:22):

showing that Lean already has some logic to help identify the issue,
but to make it work you have to (1) guess it's an issue with 0, (2) know (or guess) that pp.numerals exists, (3) turn it on and understand the resulting message

Damiano Testa (Sep 21 2020 at 12:23):

I managed the term mode proof!

mul_left_cancel' h


I got stuck this whole time with the comma at the end...

Damiano Testa (Sep 21 2020 at 12:25):

Reid Barton said:

Regarding the error, if you set_option pp.numerals false, then you get an error which shows the issue:

error: invalid type ascription, term has type
x ≠
@has_zero.zero R
(@mul_zero_class.to_has_zero R
(@monoid_with_zero.to_mul_zero_class R
(@semiring.to_monoid_with_zero R _inst_1)))
but is expected to have type
x ≠
@has_zero.zero R
(@mul_zero_class.to_has_zero R
(@monoid_with_zero.to_mul_zero_class R
(@cancel_monoid_with_zero.to_monoid_with_zero R
(@domain.to_cancel_monoid_with_zero R (@integral_domain.to_domain R _inst_2)))))


I see: one appears to go by semiring, the other by cancel_monoid.

Thanks for the explanation!

Johan Commelin (Sep 21 2020 at 12:26):

Nasty commas are nasty

Reid Barton (Sep 21 2020 at 12:26):

The main point is buried though: one is ultimately built from _inst_1 and the other from _inst_2`. So the error message could still use some work.

Kevin Buzzard (Sep 21 2020 at 12:35):

"Don't forget the comma!"

Last updated: May 08 2021 at 19:11 UTC