Zulip Chat Archive

Stream: new members

Topic: Shortening proof on product of units in Z


view this post on Zulip Alex Peattie (Jul 20 2020 at 08:44):

Hi all, I've been trying to write a tactic proof of the fact that m * n = 1 ↔ m = 1 ∧ n = 1 ∨ m = -1 ∧ n = -1 over the integers. I've managed to muddle this together:

theorem mul_eq_one_left {a b : } :
  a * b = 1  a = 1  a = -1 := begin
  assume h,
  cases (is_unit_of_mul_eq_one a b h) with a_unit h_a,

  have h_a_one_or_neg_one : a_unit = 1  a_unit = -1 := int.units_eq_one_or a_unit,
  simpa [h_a, units.ext_iff] using h_a_one_or_neg_one
end

theorem mul_eq_one {m n : } :
  m * n = 1  m = 1  n = 1  m = -1  n = -1 :=
  begin
    split,
    assume h,

    -- use result that a * b = 1 → a = 1 ∨ a = -1
    -- on m and n
    have hm := mul_eq_one_left h,
    rw mul_comm at h,
    have hn := mul_eq_one_left h,

    -- enumerate combos of m, n = {1, -1}
    cases hm, cases hn,
    -- m = 1, n = 1
    left, exact hm, hn,
    -- m = 1, n = -1 → false
    rw [hm, hn] at h, linarith,
    cases hn,
    -- m = -1, n = 1 → false
    rw [hm, hn] at h, linarith,
    -- m = -1, n = -1
    right, exact hm, hn,

    -- prove other direction of iff
    -- i.e. 1 * 1 = 1 and -1 * -1 = 1
    assume h,
    repeat { rcases h with hm, hn, simp [hm, hn] }
end

which works OK, but feels very length for a result that I feel like should follow quite easily from int.units_eq_one_or and is_unit_of_mul_eq_one? Is my approach here silly? Am I missing any approaches to shorten/clean up this proof?

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 08:52):

Your code doesn't run as it stands. Can you add the relevant imports/opens etc?

view this post on Zulip Markus Himmel (Jul 20 2020 at 08:53):

import tactic is enough

view this post on Zulip Alex Peattie (Jul 20 2020 at 08:58):

Ah yes, sorry, it's missing an import tactic at the start

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 08:59):

The easy direction looks like this:

import tactic

theorem mul_eq_one' {m n : } :
  m = 1  n = 1  m = -1  n = -1  m * n = 1 :=
begin
  rintros (rfl, rfl | rfl, rfl);
  norm_num
end

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 10:03):

The trick is that rintros will let you use rfl to mean "don't just make a new hypothesis h : m = 1, but define m to be 1 and then eliminate it, replacing all m's with 1's"

view this post on Zulip Eric Wieser (Jul 20 2020 at 10:13):

You can eliminate the second cases hn by using a semicolon to separate the first two cases

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 10:15):

For the harder way, I think some units.coe lemmas are maybe missing?

view this post on Zulip Eric Wieser (Jul 20 2020 at 10:24):

You can golf the harder way to:

        assume h,

        -- use result that a * b = 1 → a = 1 ∨ a = -1
        -- on m and n
        obtain hm | hm := mul_eq_one_left h;
        obtain hn | hn := mul_eq_one_left (by rwa mul_comm at h : n * m = 1);
        rw [hm, hn] at h;
        tauto,

view this post on Zulip Eric Wieser (Jul 20 2020 at 10:25):

Not that that really addresses your concerns

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 10:25):

I think that these are missing from the units API:

namespace units

universe u

variables {M : Type u} [monoid M]

@[simp, to_additive] lemma coe_eq_coe {u v : units M} : (u : M) = v  u = v :=
by ext, λ h, by rw h

@[simp, to_additive] lemma coe_eq_one {u : units M} : (u : M) = 1  u = 1 :=
begin
  rw units.coe_one,
  apply coe_eq_coe
end

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 10:26):

norm_cast should help here but I don't really know how to steer it.

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 10:40):

Oh, coe_eq_coe is ext_iff.symm

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 10:46):

and ext.eq_iff. It should probably be tagged norm_cast I guess?

view this post on Zulip Scott Morrison (Jul 20 2020 at 11:30):

@Alex Peattie, if you feel like making a PR with Kevin's suggestions here, that would be great! :-) (See #contrib.)

view this post on Zulip Alex Peattie (Jul 20 2020 at 11:42):

Yes I'd be happy to take a crack at it @Scott Morrison :slight_smile:

view this post on Zulip Johan Commelin (Jul 20 2020 at 11:44):

@Alex Peattie What's your github username? Then we can give you push access

view this post on Zulip Alex Peattie (Jul 20 2020 at 11:44):

It's alexpeattie

view this post on Zulip Johan Commelin (Jul 20 2020 at 11:45):

https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Alex Peattie (Jul 20 2020 at 16:01):

PR is here - https://github.com/leanprover-community/mathlib/pull/3472

Incidentally, I don't think I've quite wrapped my head around how to use the extra coe lemmas on units to simplify things :thinking: ? I'm guessing it allows getting rid of the simpa [←h_a, units.ext_iff] part, and maybe using norm_cast instead?

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 16:41):

Yeah I couldn't get them to do anything useful. I don't really know how norm_cast works any more. The docstring for norm_cast used to have a bunch of information on what kind of lemmas to tag with what attribute, but then it all got simplified and the helpful docstring disappeared because it was all supposed to be easier -- "tag everything with norm_cast". The upshot is that I now don't really know what to tag with norm_cast because I can't see the examples any more.

view this post on Zulip Alex Peattie (Jul 20 2020 at 17:07):

Ah OK, thanks. I've just seen from the build on my PR that for some reason coe_eq_one seems to be causing int.units_eq_one_or to timeout during build, but I'm afraid it's well beyond my limited Lean skills to see why...

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 17:26):

Try removing the simp tag from coe_eq_one?

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:26):

I'll take a look

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:33):

@Alex Peattie Here's what you could do to "fix" int.units_eq_one_or:

(1) add , - units.coe_eq_one to the arguments of simpa
(2) turn the simpa into a simpa only.

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:33):

I pushed a commit that does (2).

view this post on Zulip Alex Peattie (Jul 20 2020 at 17:36):

Thank you @Johan Commelin and @Kevin Buzzard . So just so I understand, the simp tag on coe_eq_one is the "culprit" but based on Johan's suggestions I guess that it's still useful to have it there, so a better solution is being more specific in the simpa call in units_eq_one_or?

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 17:36):

I'm sure norm_cast should be helpful here. If RR is a ring then there's a has_neg instance on units R, as well as a has_one instance.

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 17:41):

theorem mul_eq_one_left {a b : } (h : a * b = 1) : a = 1  a = -1 := begin
  rcases (is_unit_of_mul_eq_one a b h) with a_unit, rfl,
  cases int.units_eq_one_or a_unit with h h,
  -- now what?
  /-
  case or.inl
b: ℤ
a_unit: units ℤ
h: ↑a_unit * b = 1
h: a_unit = 1
⊢ ↑a_unit = 1 ∨ ↑a_unit = -1
case or.inr
b: ℤ
a_unit: units ℤ
h: ↑a_unit * b = 1
h: a_unit = -1
⊢ ↑a_unit = 1 ∨ ↑a_unit = -1
-/
  sorry, sorry
end

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 17:42):

I want to run norm_cast on the goal and turn it to a_unit = 1 \or a_unit = -1

view this post on Zulip Alex Peattie (Jul 20 2020 at 17:48):

@Kevin Buzzard it seems like rw h, left, norm_cast closes the first goal, but rw h, right, norm_cast doesn't close the second goal...

view this post on Zulip Alex Peattie (Jul 20 2020 at 17:49):

so it seems like norm_cast gets stuck with ↑-1 = -1?

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:50):

It might need to be taught about that lemma...

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:51):

@Alex Peattie Does push_cast instead of norm_cast help you?

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:51):

It "goes the other way"

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:51):

norm_cast tries to pull coercions as far out as possible (and tries to strip them away if they get all the way to the outside).

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:52):

push_cast tries to push coercions to the inside of expressions... and there they might cancel because of lemmas like ↑1 = 1

view this post on Zulip Alex Peattie (Jul 20 2020 at 17:54):

Ah OK, interesting. push_cast in place of norm_cast the way I'm using it (i.e. rw h, right, norm_cast) doesn't seem to make progress, no.

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 18:03):

This was what I couldn't fathom out, because

@[simp, norm_cast] protected theorem coe_neg (u : units α) : (-u : α) = -u := rfl

view this post on Zulip Johan Commelin (Jul 20 2020 at 18:05):

@Kevin Buzzard But if you apply that to 1, it doesn't work, because you would need a \u before the 1 on the RHS.

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 18:05):

So we maybe need a coe_neg_one?

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 18:08):

units.ext_iff :  {α : Type u} [_inst_1 : monoid α] {a b : units α}, a = b  a = b

Should either that, or its symm, be @[norm_cast]? This is exactly the sort of question which used to be answered in the docstring (or somewhere describing norm_cast) and no longer is (or at least I can't find it)

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 18:09):

When all the attributes were normalised, the examples were removed (or at least moved) (or at least I can't find them any more)

view this post on Zulip Rob Lewis (Jul 20 2020 at 18:09):

https://leanprover-community.github.io/mathlib_docs/attributes.html#norm_cast%20attributes

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 18:09):

Thanks Rob! I was looking under "tactics", and not under "attributes"

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 18:11):

My main problem now is that I'm on a machine with a screen that isn't wide enough to read the link without scrolling to the bottom and dragging from left to right and then scrolling back up again :-)

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 18:25):

import tactic

-- should be in mathlib
namespace units

universe u

variables {M : Type u} [monoid M]

@[simp, to_additive, norm_cast] lemma coe_eq_coe {u v : units M} : (u : M) = v  u = v :=
ext.eq_iff

@[simp, to_additive] lemma coe_eq_one {u : units M} : (u : M) = 1  u = 1 :=
by norm_cast

@[simp, norm_cast] lemma coe_neg_one {R : Type u} [ring R] : ((-1 : units R) : R) = -1 := rfl

end units
-- end of mathlib stuff

theorem mul_eq_one_left {a b : } (h : a * b = 1) : a = 1  a = -1 := begin
  rcases (is_unit_of_mul_eq_one a b h) with a_unit, rfl,
  cases int.units_eq_one_or a_unit with h2 h2;
  rw h2,
  left, norm_cast,
  right, norm_cast,
end

theorem mul_eq_one {m n : } : m * n = 1  m = 1  n = 1  m = -1  n = -1 :=
begin
  split,
  { assume h,
    obtain hm | hm := mul_eq_one_left h;
    obtain hn | hn := mul_eq_one_left (by rwa mul_comm at h : n * m = 1);
    rw [hm, hn] at h;
    tauto },
  { rintros (rfl, rfl | rfl, rfl);
    norm_num }
end

OK so this is looking in better shape. I am a bit confused about which of the proposed mathlib lemmas should be simp lemmas (I'm not very good at simp) but perhaps I've managed to get the norm_cast lemmas into good shape.

view this post on Zulip Alex Peattie (Jul 20 2020 at 20:14):

OK the PR's merged so coe_eq_coe and coe_eq_one should be in mathlib now, I'll do a new PR tomorrow to add coe_neg_one :slight_smile:

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 20:25):

Oh, nice! You're a fast mover :-)

view this post on Zulip Alex Peattie (Jul 22 2020 at 11:10):

OK coe_neg_one is in the latest mathlib now :ok:

view this post on Zulip Alex Peattie (Jul 22 2020 at 11:11):

In case it's of interest to anyone, I originally wanted to prove the theorem above on my way to proving that 0 and 1 are the only consecutive perfect squares:

import tactic

theorem mul_eq_one_left {a b : } (h : a * b = 1) : a = 1  a = -1 := begin
  rcases (is_unit_of_mul_eq_one a b h) with a_unit, rfl,
  cases int.units_eq_one_or a_unit with h2 h2;
  rw h2,
  left, norm_cast,
  right, norm_cast,
end

theorem mul_eq_one {m n : } : m * n = 1  m = 1  n = 1  m = -1  n = -1 :=
begin
  split,
  { assume h,
    obtain hm | hm := mul_eq_one_left h;
    obtain hn | hn := mul_eq_one_left (by rwa mul_comm at h : n * m = 1);
    rw [hm, hn] at h;
    tauto },
  { rintros (rfl, rfl | rfl, rfl);
    norm_num }
end

theorem zero_one_only_consec_perfect_squares
  (a: ) (b: )
  : a^2 - b^2 = 1  b^2 = 0  a^2 = 1 :=
begin
  intro h,
  obtain h_ab, _⟩ | h_ab, _⟩ := mul_eq_one.1 (by {
    ring, assumption
  } : ((a + b) * (a - b) = 1));
  {
    have h_b0 : b = 0, linarith,
    rw h_b0 at *,
    rw add_zero at h_ab,
    rw h_ab, ring, use rfl, rfl
  }
end

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 21:05):

Nice :-) Now can you prove that there are no integer solutions to 4a^2=b^3+1 in integers is a=0 and b=-1?

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 21:05):

That's more challenging.

view this post on Zulip Alex Peattie (Aug 10 2020 at 18:39):

Kevin Buzzard said:

Nice :-) Now can you prove that there are no integer solutions to 4a^2=b^3+1 in integers is a=0 and b=-1?

I managed to prove this in the end. As you say much more challenging - it took me 500 or so lines, although I'm sure lots of parts are very "golfable" :smiling_face:. I'll clean up and the comment the proof, then stick it on Github

view this post on Zulip Alex Peattie (Aug 10 2020 at 18:40):

I'm not sure the main result is very applicable elsewhere, but hopefully (once cleaned up) a couple of the lemmas I proved along the way might be useful mathlib additions

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 19:17):

I'm sure the main result is not of much use in some sense, but if you managed to get Lean to do it then that's great -- you probably learnt a lot about Lean along the way! And indeed you might have found some holes in mathlib. You should make a level at codewars :-)

view this post on Zulip Alex Peattie (Aug 10 2020 at 19:27):

Yes is seems the best way to learn Lean is to just throw yourself into trying to prove things! I hadn't realised there was a Lean section on Codewars, I'll take a look :smile: !


Last updated: May 08 2021 at 10:12 UTC