## Stream: new members

### Topic: simple equations in pnat

#### Moritz Firsching (Jan 11 2021 at 15:33):

Hi! I'm playing around with some simple equations and inequalities in pnat and it seems to be much more cumbersome than doing the same in nat. Especially since many tactics like simp and linarithm don't work.
Here's an example of a really simple lemma:

lemma simple_ineq (a b: ℕ+): a < a + b :=
begin
let c := a + b,
have coerce: a < c ↔ ↑a < ↑c := by refl,
let nb := ↑b,
have bneq: nb ≠ 0 := by apply pnat.ne_zero,
have bpoa: nb > 0 := by simp,
have aplusb: ↑a  <  ↑a + nb  := by simp,
exact aplusb,
end


What are better ways of doing that?

#### Moritz Firsching (Jan 11 2021 at 15:50):

Here's an example with a slightly more involved inequality:

lemma larger_ineq (x y z: ℕ+) (h: x + z < y):
¬ x + 2 * z + (y - x - z) < z := by sorry,


#### Kevin Buzzard (Jan 11 2021 at 15:57):

Taking the pnats apart seems to be more effective:

import data.pnat.basic
import tactic

lemma simple_ineq : ∀ a b : ℕ+, a < a + b :=
begin
rintro ⟨a, ha⟩ ⟨b, hb⟩,
show a < a + b,
linarith,
end


#### Eric Wieser (Jan 11 2021 at 15:58):

I was surprised that norm_cast couldn't handle that show line for me

#### Moritz Firsching (Jan 11 2021 at 15:58):

thanks, that's perfect!

#### Eric Wieser (Jan 11 2021 at 16:01):

This looks like it makes progress on the second case:

lemma larger_ineq (x y z: ℕ+) (h: x + z < y) :
¬ x + 2 * z + (y - x - z) < z :=
begin
obtain ⟨x, hx⟩ := x,
obtain ⟨y, hy⟩ := y,
obtain ⟨z, hz⟩ := z,
simp [←pnat.coe_lt_coe] at ⊢ h,
sorry
end


#### Eric Wieser (Jan 11 2021 at 16:02):

Indeed, linarith closes the goal

#### Kevin Buzzard (Jan 11 2021 at 16:02):

import data.pnat.basic
import tactic

lemma larger_ineq (x y z: ℕ+) (h: x + z < y):
¬ x + 2 * z + (y - x - z) < z :=
begin
cases x with x hx,
cases y with y hy,
cases z with z hz,
simp [←pnat.coe_lt_coe] at ⊢ h,
linarith,
end


#### Eric Wieser (Jan 11 2021 at 16:02):

docs#pnat.coe_lt_coe

nice

#### Moritz Firsching (Jan 11 2021 at 20:46):

Here's another one I'm struggling with, this time an equation for a change:

lemma eq_with_2 (x z: ℕ+) (h_2: ¬x + 2 * z < 2 * z):
x + 2 * z - 2 * z = x :=
begin
obtain ⟨x, hx⟩ := x,
obtain ⟨z, hz⟩ := z,
simp [←pnat.coe_inj],
rw [pnat.sub_coe],
sorry,
end


Can this start be finished? Is there a better way to do that?

#### Kevin Buzzard (Jan 11 2021 at 20:59):

Oh lol pnat subtraction is even crazier than nat subtraction! 1-1=1 :D

#### Eric Wieser (Jan 11 2021 at 21:01):

generalize : y = 2*z at the start of the proof would help clean up the goal slightly

#### Kevin Buzzard (Jan 11 2021 at 21:02):

I am getting lazy and I don't want to do this one. Instead I am going to challenge the very idea that you ever want to be using - at all when working with pnats. Are you absolutely sure that you can't do what you want to do with addition instead? There seems to be a missing lemma pnat.add_sub_cancel : a + b - b = aand using this it's easy. Feel free to prove it yourself and PR it if you really feel you need it! But why all this pnat subtraction? If I ever do a subtraction in nat I know I'm doing it wrong.

#### Moritz Firsching (Jan 11 2021 at 21:11):

As a fun exercise I'm trying to proof sum_two_squares in a different way, using Zagier's "one sentence proof". To this end I defined an involution

def zagier_involution (x : ℕ+)  (y : ℕ+) (z : ℕ+) : ℕ+ × ℕ+ × ℕ+ :=
if (x + z) < y then (x + 2*z, z, y - x - z) else
(if x < 2*y  then (2*y - x, y, x - y + z) else
(x - 2*y, x - y + z, y) )


and when trying to proof that it really is an involution, I started

lemma zinvolu {x y z : ℕ+}: zagier_involution
(zagier_involution x y z).1
(zagier_involution x y z).2.1
(zagier_involution x y z).2.2 = (x, y, z):=
begin
rw [zagier_involution],
rw [zagier_involution],
split_ifs,
sorry,
end


Then there is 9 subcases, each of which can either be done by showing the case can never happen by showing some contradiction between inequalities or showing that the case is true by showing some equalities.
I didn't know that pnat is more cumbersome than nat...

#### Kevin Buzzard (Jan 11 2021 at 21:14):

import tactic
import data.pnat.basic

-- this could be in mathlib
lemma pnat.add_sub_cancel (a b : ℕ+) : a + b - b = a := pnat.eq
begin
rw [pnat.sub_coe, if_pos],
{ exact lt_add_of_pos_left b.1 a.pos },
end

lemma eq_with_2 (x z: ℕ+) (h_2: ¬x + 2 * z < 2 * z):
x + 2 * z - 2 * z = x := pnat.add_sub_cancel _ _


#### Kevin Buzzard (Jan 11 2021 at 21:16):

pnat is just less used. An alternative is to develop a robust library for pnat! I think your reponse is perfectly adequate, and a good justification for pnat subtraction.

#### Alex J. Best (Jan 11 2021 at 21:18):

I also did this as a "fun exercise" when I first started, it might not be as fun as you think :grinning: (mine ended up at 650 lines, but mathlib has moved on a lot since then so I imagine its possible to do it in way less). I highly recommend using Z when dealing with subtraction, it will save you a lot of pain if you only have to show in one point of the proof that some statement about integers implies some statement about naturals, rather than worrying about an inequality every time you use a - sign.

#### Bryan Gin-ge Chen (Jan 11 2021 at 21:20):

A cleaned up and nicely documented version of this would be a good proof to include in mathlib's /archive.

#### Kevin Buzzard (Jan 11 2021 at 21:22):

Yes, it might be easier to define this involution on the finite set Zagier isolates, and let x, y, z be positive integers rather than pnats. You'll have to insert proofs that various things are positive in your definition of the involution, but linarith should be able to deal with them relatively easily. This would probably be a less painful way of doing what you're doing. You're in some sense skipping the work that various things are positive, and then all of a sudden it all hits you at once when you're trying to use your definition.

#### Moritz Firsching (Jan 11 2021 at 21:23):

Cool, thanks @Kevin Buzzard. After reading @Alex J. Best 's comment, it seems like I will go with \N instead of \N+ for now.

#### Kevin Buzzard (Jan 11 2021 at 21:23):

Alex is suggesting Z not N! N is almost as horrible as pnat!

#### Moritz Firsching (Jan 11 2021 at 21:24):

ok, I see, makes sense

#### Kevin Buzzard (Jan 11 2021 at 21:25):

Ask yourself what function Zagier is using when he's talking about subtraction. Is he using some weird function which thinks 2-3=0 (nat) or 1 (pnat)? No, he's using a function which has much nicer properties -- integer subtraction, a.k.a. "subtraction" (to mathematicians -- these pathological functions on nat and pnat do not deserve the name subtraction). So you should use subtraction too and use int, for minimal pain.

#### Kevin Buzzard (Jan 11 2021 at 21:36):

I'd be tempted to start like this:

import tactic
import data.nat.prime

def S (p : ℤ) :=
{c : ℤ × ℤ × ℤ | let (x, y, z) := c in
0 < x ∧ 0 < y ∧ 0 < z ∧ x * x + 4 * y * z = p}

lemma mem_S_iff (p x y z : ℤ) : (x, y, z) ∈ S p ↔ 0 < x ∧ 0 < y ∧ 0 < z ∧ x * x + 4 * y * z = p := iff.rfl

def aux_lemma_1 (p : ℕ) (hp : p.prime) (x y z : ℤ) : (x, y, z) ∈ S p → x ≠ y - z := sorry
def aux_lemma_2 (p : ℕ) (hp : p.prime) (x y z : ℤ) : (x, y, z) ∈ S p → x ≠ 2 * y := sorry

def zagier_involution (p : ℕ) (hp : p.prime) : S p → S p :=
λ c, let ⟨(x, y, z), h1, h2, h3, h4⟩ := c in
if x < y - z then ⟨(x + 2 * z, z, y - x - z), sorry⟩ else
if 2 * y < x then ⟨(x - 2 * y, x - y + z, y), sorry⟩ else
⟨(2 * y - x, y, x - y + z), sorry⟩


Those sorries should be far less painful to fill in.

#### Kevin Buzzard (Jan 11 2021 at 21:38):

Don is prone to exaggeration -- the implicit assumptions here show that really it is not a one-line proof, although the details he omits are not difficult. All these sorries are now statements about integers, so you have access to linarith and ring etc.

#### Moritz Firsching (Jan 11 2021 at 21:48):

Thanks that looks like a good start.

Last updated: May 08 2021 at 18:17 UTC