# Zulip Chat Archive

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

#### Eric Wieser (Jul 20 2020 at 10:25):

Not that that really addresses your concerns

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

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

?

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

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 add_zero at h_ab,
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