mul_left_cancel for integral domains

Stream: new members

[Damiano Testa]

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]

mul_left_cancel hopefully?

[Johan Commelin]

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

[Damiano Testa]

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

[Kevin Buzzard]

I'll give it a go

[Shing Tak Lam]

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

[Kevin Buzzard]

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

[Damiano Testa]

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]

You should delete comm_ring R and use integral_domain R

[Damiano Testa]

Let me try!

[Damiano Testa]

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]

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]

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

[Shing Tak Lam]

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]

Yes, my standing assumption is that R is a semiring

[Kevin Buzzard]

Interesting

[Reid Barton]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Damiano Testa]

Ok, I will remove the semiring assumption

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Damiano Testa]

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

[Reid Barton]

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

[Damiano Testa]

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]

begin means entering tactic mode

[Johan Commelin]

and end stops it.

[Johan Commelin]

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

[Damiano Testa]

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

I will keep by! Ahahaha

[Johan Commelin]

No by also enters tactic mode

[Reid Barton]

To be more specific, a consecutive substring :upside_down:

[Kevin Buzzard]

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]

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

[Johan Commelin]

Your lemma xxv is also a function

[Reid Barton]

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]

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]

I managed the term mode proof!

mul_left_cancel' h

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

[Damiano Testa]

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]

Nasty commas are nasty

[Reid Barton]

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]

"Don't forget the comma!"