Shortening proof on product of units in Z

Stream: new members

[Alex Peattie]

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?

[Kevin Buzzard]

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

[Markus Himmel]

import tactic is enough

[Alex Peattie]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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"

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

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,

[Eric Wieser]

Not that that really addresses your concerns

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh, coe_eq_coe is ext_iff.symm

[Kevin Buzzard]

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

[Scott Morrison]

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

[Alex Peattie]

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

[Johan Commelin]

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

[Alex Peattie]

It's alexpeattie

[Johan Commelin]

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

[Alex Peattie]

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?

[Kevin Buzzard]

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.

[Alex Peattie]

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...

[Kevin Buzzard]

Try removing the simp tag from coe_eq_one?

[Johan Commelin]

I'll take a look

[Johan Commelin]

@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.

[Johan Commelin]

I pushed a commit that does (2).

[Alex Peattie]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Alex Peattie]

@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...

[Alex Peattie]

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

[Johan Commelin]

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

[Johan Commelin]

@Alex Peattie Does push_cast instead of norm_cast help you?

[Johan Commelin]

It "goes the other way"

[Johan Commelin]

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).

[Johan Commelin]

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

[Alex Peattie]

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.

[Kevin Buzzard]

This was what I couldn't fathom out, because

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

[Johan Commelin]

@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.

[Kevin Buzzard]

So we maybe need a coe_neg_one?

[Kevin Buzzard]

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)

[Kevin Buzzard]

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

[Rob Lewis]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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 :-)

[Kevin Buzzard]

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.

[Alex Peattie]

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:

[Kevin Buzzard]

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

[Alex Peattie]

OK coe_neg_one is in the latest mathlib now :ok:

[Alex Peattie]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

That's more challenging.

[Alex Peattie]

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

[Alex Peattie]

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

[Kevin Buzzard]

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 :-)

[Alex Peattie]

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: !