dealing with natural number subtraction

Stream: maths

[Nicholas McConnell]

What's the best way to solve this goal? y-x is a subtraction of natural numbers and I need to convince Lean that by h : x < y, it coincides with the ring subtraction.

import tactic
import data.int.basic
universe u
local attribute [instance] classical.prop_decidable

def ex1 (x y z : ℕ) : ℕ := x + y * z

def even (n : ℕ) : Prop := ∃ k, n = 2*k
def odd (n : ℕ) : Prop := ∃ k, n = 2*k+1

lemma even_or_odd (n : ℕ) : or (even n) (odd n) :=
begin
sorry,
end

lemma even_plus_even_is_even (n m : ℕ) (h : and (even n) (even m)) : even (n+m) :=
begin
sorry,
end

lemma even_minus_even_is_even (n m : ℕ) (h : (even n) ∧ (even m) ∧ (m ≤ n))
  : even (n - m) :=
begin
sorry,
end

lemma odd_minus_odd_is_even (n m : ℕ) (h : (odd n) ∧ (odd m) ∧ (m ≤ n))
  : even (n - m) :=
begin
sorry,
end

lemma mul_cancel (a b c : ℕ) (h : a*b = a*c) (p : 0 < a) : b = c :=
begin
sorry,
end

lemma halving_first (n x y : ℕ) (h : x < y) (h1 : 2*n = x^2 + y^2) :
  ∃a:ℕ, ∃b:ℕ, n = a^2 + b^2 :=
begin
have zero_lt_two := lt_trans (nat.lt_succ_self 0) (nat.lt_succ_self 1),
have xeo := even_or_odd x,
have yeo := even_or_odd y,
cases xeo with x_even x_odd,
cases yeo with y_even y_odd,
have sum_even := even_plus_even_is_even y x ⟨y_even, x_even⟩,
have diff_even := even_minus_even_is_even y x ⟨y_even, x_even, le_of_lt h⟩,
rw even at sum_even,
cases sum_even with sum' sum_ev,
rw even at diff_even,
cases diff_even with diff' diff_ev,
use sum',
use diff',
have claim : 2*n = 2*(sum'^2 + diff'^2),
rw h1,
have claim' : 2*(x^2+y^2) = 4*(sum'^2+diff'^2),
have thing : 4*(sum'^2+diff'^2) = (2*sum')^2+(2*diff')^2 := by ring,
rw thing,
rw (eq.symm sum_ev),
rw (eq.symm diff_ev),
-- ring doesn't work due the subtraction of natural numbers.
--   (Which takes n - m to be zero if n < m.)
-- How to convince Lean that y-x is ring subtraction as a consequence of h?
end

[Scott Morrison]

Why not try to write a separate lemma which states exactly what you want to use at this point?

[Scott Morrison]

(Any Lean proof longer than 10 lines needs refactoring into smaller chunks. :-)

[Scott Morrison]

The extract_goal tactic is really useful for this.

[Nicholas McConnell]

I'm trying it to no avail...

[Nicholas McConnell]

See prelim below

import tactic
import data.int.basic
universe u
local attribute [instance] classical.prop_decidable

def ex1 (x y z : ℕ) : ℕ := x + y * z

def even (n : ℕ) : Prop := ∃ k, n = 2*k
def odd (n : ℕ) : Prop := ∃ k, n = 2*k+1

lemma even_or_odd (n : ℕ) : or (even n) (odd n) :=
begin
sorry,
end

lemma even_plus_even_is_even (n m : ℕ) (h : and (even n) (even m)) : even (n+m) :=
begin
sorry,
end

lemma even_minus_even_is_even (n m : ℕ) (h : (even n) ∧ (even m) ∧ (m ≤ n))
  : even (n - m) :=
begin
sorry,
end

lemma odd_minus_odd_is_even (n m : ℕ) (h : (odd n) ∧ (odd m) ∧ (m ≤ n))
  : even (n - m) :=
begin
sorry,
end

lemma mul_cancel (a b c : ℕ) (h : a*b = a*c) (p : 0 < a) : b = c :=
begin
sorry,
end

lemma prelim (x y : ℕ) (h : x < y) :
  2 * (x ^ 2 + y ^ 2) = (y + x) ^ 2 + (y - x) ^ 2 :=
begin
have lem : x*x < y*y,
have a := zero_le x,
have thing := nat.mul_le_mul_left x (le_of_lt h),
have thing' := nat.mul_lt_mul_of_pos_right h (lt_of_le_of_lt a h),
exact lt_of_le_of_lt thing thing',

have claim : (y-x)^2 = x^2 + y^2 - 2*x*y,
rw nat.pow_two,
rw nat.pow_two,
rw nat.pow_two,
have thing : y*y = y*y - x*x + x*x := by {
  exact eq.symm (nat.sub_add_cancel (le_of_lt lem))
},
rw add_comm,
rw thing,
rw add_assoc,
-- what the heck should I do next?
end

[Scott Morrison]

You definitely want to take advantage of the fact that this would be trivial to prove if you were in int rather than nat: you could just use ring. So the strategy should be:

• Use injectivity of the map from nat to int to show that it suffices to prove this after coercing both sides to int
• Push the coercion from nat to int inwards (hopefully push_cast will assist you here)
• Possibly have to do some explicit work using the hypothesis h to push the coercion over the subtraction (but ideally push_cast will help you even here)
• Call ring (or even better, state the result in int as a separate lemma, proved with by ring, and apply that lemma)

[Scott Morrison]

For the first step, I would type in:

import tactic.basic

example (x y : ℕ) (h : (x : ℤ) = (y : ℤ)) : x = y := by library_search

[Scott Morrison]

to learn what the name of the lemma about injectivity is

[Scott Morrison]

it says: int.of_nat.inj

[Scott Morrison]

Unfortunately push_cast does the wrong thing at the next step...

[Kevin Buzzard]

Here's another approach:

lemma prelim (x y : ℕ) (h : x < y) :
  2 * (x ^ 2 + y ^ 2) = (y + x) ^ 2 + (y - x) ^ 2 :=
begin
  cases (nat.exists_eq_add_of_lt h) with w hw,
  rw hw,
  rw (show x + w + 1 - x = w + 1, by omega),
  ring,
end

but this is a dirty hack -- what Scott is suggesting is morally the correct thing to do I think.

[Kevin Buzzard]

I'm just observing that because the subtractions are not too bad, you can remove them without too much trouble (replace y with x+w+1) and then ring works anyway.

[Scott Morrison]

It turns out library_search leads you down the wrong track here. It suggests int.of_nat.inj, but this introduces the explicit function int.of_nat, which then doesn't play well with push_cast. Using suggest instead of library_search identifies as the 3rd suggestion the lemma int.coe_nat_inj, which is better.

[Scott Morrison]

Then

example (x y : ℕ) (h : x < y) :
  2 * (x ^ 2 + y ^ 2) = (y + x) ^ 2 + (y - x) ^ 2 :=
begin
  apply int.coe_nat_inj,
  push_cast,
end

gives us the goal

(↑0 + 1 + 1) * (↑(x ^ 2) + ↑(y ^ 2)) = ↑((y + x) ^ 2) + ↑((y - x) ^ 2)

which ... suggests that we haven't correctly tagged lemmas with push_cast! It's lame that ↑2 has been converted to ↑0 + 1 + 1, and it's lame that ↑(x ^ 2) hasn't been converted to (↑x) ^ 2.

[Kevin Buzzard]

To get the norm_cast approach to work I'd like to have x <= y -> ↑y - ↑x = ↑(y - x). It should be all downhill from there.

[Kevin Buzzard]

Scott -- I've started with the int result and am trying to get back to the nat result with norm_cast. You're going the other way.

lemma prelim (x y : ℕ) (h : x < y) :
  2 * (x ^ 2 + y ^ 2) = (y + x) ^ 2 + (y - x) ^ 2 :=
begin
  have this : (2 : ℤ) * (x ^ 2 + y ^ 2) = (y + x) ^ 2 + (y - x) ^ 2,
    ring,
  norm_cast at this,
  -- this involves ↑y - ↑x which can't be normcasted down to ↑(y - x)
end

[Bryan Gin-ge Chen]

There's a big norm_cast PR in progress here.

[Scott Morrison]

Where does one obtain a has_pow ℤ ℕ instance from??

[Kevin Buzzard]

algebra.group_power?

[Kevin Buzzard]

That's where I usually look...

[Scott Morrison]

@Bryan Gin-ge Chen, what's the state of that PR? Do you know if anyone is looking after it?

[Bryan Gin-ge Chen]

I would ask @Paul-Nicolas Madelaine and @Rob Lewis.

[Rob Lewis]

Still waiting on input from Paul-Nicolas.

[Kevin Buzzard]

OK so doing it the other way works fine once you use library_search (thank you thank you thank you @Scott Morrison :heart: :heart: :heart: ) to figure out that bit about y - x :-)

lemma prelim (x y : ℕ) (h : x < y) :
  2 * (x ^ 2 + y ^ 2) = (y + x) ^ 2 + (y - x) ^ 2 :=
begin
  have this : (2 : ℤ) * (x ^ 2 + y ^ 2) = (y + x) ^ 2 + (y - x) ^ 2,
    ring,
  rw ←int.coe_nat_sub (le_of_lt h) at this,
  norm_cast at this,
  exact this
end

[Kevin Buzzard]

It's interesting that norm_cast worked really well and push_cast did all sorts of crazy things.

[Scott Morrison]

Here's my version, with the "finding the right lemmas" cruft at the top left in, for pedagogical purposes:

import tactic.norm_cast
import tactic.ring
import algebra.group_power

example (x y : ℕ) (h : (x : ℤ) = (y : ℤ)) : x = y := by suggest

example (x : ℕ) : ((x^2 : ℕ) : ℤ) = (x : ℤ)^2 := by library_search

-- This attribute is missing, and should be added to mathlib
attribute [push_cast] int.coe_nat_pow

example (x y : ℕ) : ((x - y : ℕ) : ℤ) = (x : ℤ) - (y : ℤ) := by suggest
-- down the list we find `int.coe_nat_sub`

#print int.coe_nat_sub

example (x y : ℕ) (h : x ≤ y) :
  2 * (x ^ 2 + y ^ 2) = (y + x) ^ 2 + (y - x) ^ 2 :=
begin
  apply int.coe_nat_inj,
  push_cast,
  rw int.coe_nat_sub h, -- it would be nice if `push_cast` managed this itself.
  ring,                 -- the output is a bit wonky here
  simp,
end

[Kevin Buzzard]

Oh so it does come out nice in the end.

[Kevin Buzzard]

Related: library_search suggested int.coe_nat_sub.reversed for me, which I was surprised by; you can #check int.coe_nat_sub.reversed to see what it says (and compare with int.coe_nat_sub). But if you right click and go to definition then something surprising happens!

[Kevin Buzzard]

Why use suggest when you can use library_search? Oh -- because your lemma isn't even true!

[Nicholas McConnell]

Thanks very much, Scott and Kevin. I followed Scott's latest approach

[Scott Morrison]

@Simon Hudon, can you point me to an example of copying priorities? I want priorities on move_cast lemmas to to copied to the synthesised push_cast lemmas.

[Scott Morrison]

Scratch that.

[Alex J. Best]

I'm no expert but I did notice once that there seems to be a mixture of whether lemmas of the form ((0 : a) : b) = 0 are marked as squash_cast or `elim_cast. Likewise with 1 instead of zero. Can that be problematic?

[Patrick Massot]

All this will be obsolete when the new norm_cast will land.

[Nicholas McConnell]

Just a basic question, if a is an integer, and one is given the hypothesis 0 ≤ a, how do you get the natural number whose integer cast equals a?

[Mario Carneiro]

There is a theorem int.eq_coe_of_zero_le that gives an existential, or you can use int.to_nat or int.nat_abs

[Nicholas McConnell]

Thanks

[Nicholas McConnell]

What's the best way to get from a > 0 and b < 0 to a*b < 0 in the integers? I looked in int\basic.lean and found nothing that does anything like this

[Mario Carneiro]

That's a general theorem about ordered rings

[Nicholas McConnell]

Yeah, so is there a Lean command for it?

[Mario Carneiro]

it looks like you want a mul to be neg given pos and neg. Let me look that up...

[Mario Carneiro]

oh hey mul_neg_of_pos_of_neg :)

[Scott Morrison]

Mario's method is an excellent one, but there's also

example (a b : ℤ) (ha : 0 < a) (hb : b < 0) : a * b < 0 := by library_search

(which reports the same answer)

[Nicholas McConnell]

Okay, I confess, I should try using "by library_search" more often

[Scott Morrison]

(Unfortunately you do need to have the right imports open, which sometimes is a deal-breaker if you really don't know yet what you're looking for. The advantage of Mario's method is that if you can guess at least a fragment of the name, you can search for it across all files in mathlib.)

[Mario Carneiro]

By the way, it may not have been obvious, but my first comment "that's a general theorem about ordered rings" was actually a search clue. When looking for an algebraic lemma, you should ask yourself if it is a theorem about general algebraic structures of some kind like rings or fields, or if they are particular to the specific set you are working over (e.g. things about natural number subtraction). If they are general, they will usually be in the root namespace (and be in one of the algebra/ files), and if they are specific then they will be in data.int.basic or data.nat.basic or similar and will be in that type's namespace.

[Johan Commelin]

@Nicholas McConnell It seems that you want to know about the lift tactic.

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#lift

[Johan Commelin]

From the docs:

If n : ℤ and hn : n ≥ 0 then the tactic lift n to ℕ using hn creates a new constant of type ℕ, also named n and replaces all occurrences of the old variable (n : ℤ) with ↑n (where n in the new variable). It will remove n and hn from the context.

[Andrew Ashworth]

<_< I would've thought this would be named descend since natural numbers are a subset of the integers

[Andrew Ashworth]

I don't understand when a thing is a lift or when it is a descent, probably

[Johan Commelin]

That's because there are two very much conflicting naming traditions

[Jalex Stark]

Does the lift tactic in fact let you go both ways? (my reading of the documentation is yes but I thought of typing this question before I thought of typing code into a lean interpreter)

[Mario Carneiro]

I don't think so, depending on what you mean by "both ways". The lift tactic allows you to take a variable from a "superset" and produce an element of the "subset" with the same name

[Jalex Stark]

I think you have correctly inferred what I meant by "both ways" and answered my question

[Jalex Stark]

I guess the other way is just coercion

[Mario Carneiro]

If you have an element of the subset and want an element of the superset, you don't need the tactic, because you can just use the coe