Zulip Chat Archive

Stream: new members

Topic: mul_left_cancel for integral domains


view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 21 2020 at 11:47):

mul_left_cancel hopefully?

view this post on Zulip Johan Commelin (Sep 21 2020 at 11:48):

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

view this post on Zulip Damiano Testa (Sep 21 2020 at 11:50):

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

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 11:51):

I'll give it a go

view this post on Zulip Shing Tak Lam (Sep 21 2020 at 11:52):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 11:52):

You should delete comm_ring R and use integral_domain R

view this post on Zulip Damiano Testa (Sep 21 2020 at 11:52):

Let me try!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Shing Tak Lam (Sep 21 2020 at 11:59):

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

view this post on Zulip 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

view this post on Zulip Damiano Testa (Sep 21 2020 at 12:00):

Yes, my standing assumption is that R is a semiring

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 12:00):

Interesting

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 21 2020 at 12:01):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Sep 21 2020 at 12:02):

Ok, I will remove the semiring assumption

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 12:04):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 21 2020 at 12:07):

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

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Sep 21 2020 at 12:10):

begin means entering tactic mode

view this post on Zulip Johan Commelin (Sep 21 2020 at 12:10):

and end stops it.

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Sep 21 2020 at 12:11):

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

I will keep by! Ahahaha

view this post on Zulip Johan Commelin (Sep 21 2020 at 12:11):

No by also enters tactic mode

view this post on Zulip Reid Barton (Sep 21 2020 at 12:12):

To be more specific, a consecutive substring :upside_down:

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 21 2020 at 12:13):

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

view this post on Zulip Johan Commelin (Sep 21 2020 at 12:13):

Your lemma xxv is also a function

view this post on Zulip 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)))))

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Sep 21 2020 at 12:26):

Nasty commas are nasty

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 12:35):

"Don't forget the comma!"


Last updated: May 08 2021 at 19:11 UTC