simple equations in pnat

Stream: new members

[Moritz Firsching]

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]

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]

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]

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

[Moritz Firsching]

thanks, that's perfect!

[Eric Wieser]

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]

Indeed, linarith closes the goal

[Kevin Buzzard]

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]

docs#pnat.coe_lt_coe

[Moritz Firsching]

nice

[Moritz Firsching]

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],
  simp [pnat.mul_coe, pnat.add_coe],
  sorry,
 end

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

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],
  { apply nat.add_sub_cancel },
  { 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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Moritz Firsching]

ok, I see, makes sense

[Kevin Buzzard]

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]

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]

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]

Thanks that looks like a good start.