## Stream: new members

### Topic: Shortening proof on product of units in Z

#### 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?

#### Kevin Buzzard (Jul 20 2020 at 08:52):

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

#### Markus Himmel (Jul 20 2020 at 08:53):

import tactic is enough

#### Alex Peattie (Jul 20 2020 at 08:58):

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

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


#### 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"

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

#### Kevin Buzzard (Jul 20 2020 at 10:15):

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

#### 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,


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


#### Kevin Buzzard (Jul 20 2020 at 10:26):

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

#### Kevin Buzzard (Jul 20 2020 at 10:40):

Oh, coe_eq_coe is ext_iff.symm

#### Kevin Buzzard (Jul 20 2020 at 10:46):

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

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

#### Alex Peattie (Jul 20 2020 at 11:42):

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

#### Johan Commelin (Jul 20 2020 at 11:44):

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

#### Alex Peattie (Jul 20 2020 at 11:44):

It's alexpeattie

#### Johan Commelin (Jul 20 2020 at 11:45):

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

#### Alex Peattie (Jul 20 2020 at 16:01):

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

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

#### Kevin Buzzard (Jul 20 2020 at 17:26):

Try removing the simp tag from coe_eq_one?

I'll take a look

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

#### Johan Commelin (Jul 20 2020 at 17:33):

I pushed a commit that does (2).

#### 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?

#### Kevin Buzzard (Jul 20 2020 at 17:36):

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


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

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

#### Alex Peattie (Jul 20 2020 at 17:49):

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

#### Johan Commelin (Jul 20 2020 at 17:50):

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

#### Johan Commelin (Jul 20 2020 at 17:51):

@Alex Peattie Does push_cast instead of norm_cast help you?

#### Johan Commelin (Jul 20 2020 at 17:51):

It "goes the other way"

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

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

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

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


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

#### Kevin Buzzard (Jul 20 2020 at 18:05):

So we maybe need a coe_neg_one?

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

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

#### Rob Lewis (Jul 20 2020 at 18:09):

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

#### Kevin Buzzard (Jul 20 2020 at 18:09):

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

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

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

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

#### Kevin Buzzard (Jul 20 2020 at 20:25):

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

#### Alex Peattie (Jul 22 2020 at 11:10):

OK coe_neg_one is in the latest mathlib now :ok:

#### 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 h_ab, ring, use ⟨rfl, rfl⟩
}
end


#### 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?

#### Kevin Buzzard (Jul 22 2020 at 21:05):

That's more challenging.

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

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

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

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