Zulip Chat Archive

Stream: maths

Topic: dealing with natural number subtraction


Nicholas McConnell (Feb 27 2020 at 16:47):

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 (Feb 27 2020 at 16:51):

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

Scott Morrison (Feb 27 2020 at 16:52):

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

Scott Morrison (Feb 27 2020 at 16:56):

The extract_goal tactic is really useful for this.

Nicholas McConnell (Feb 27 2020 at 17:28):

I'm trying it to no avail...

Nicholas McConnell (Feb 27 2020 at 17:29):

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 (Feb 27 2020 at 17:36):

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 (Feb 27 2020 at 17:38):

For the first step, I would type in:

import tactic.basic

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

Scott Morrison (Feb 27 2020 at 17:39):

to learn what the name of the lemma about injectivity is

Scott Morrison (Feb 27 2020 at 17:39):

it says: int.of_nat.inj

Scott Morrison (Feb 27 2020 at 17:40):

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

Kevin Buzzard (Feb 27 2020 at 17:43):

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 (Feb 27 2020 at 17:44):

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 (Feb 27 2020 at 17:45):

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 (Feb 27 2020 at 17:47):

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 (Feb 27 2020 at 17:47):

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 (Feb 27 2020 at 17:49):

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 (Feb 27 2020 at 17:49):

There's a big norm_cast PR in progress here.

Scott Morrison (Feb 27 2020 at 17:51):

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

Kevin Buzzard (Feb 27 2020 at 17:51):

algebra.group_power?

Kevin Buzzard (Feb 27 2020 at 17:52):

That's where I usually look...

Scott Morrison (Feb 27 2020 at 17:52):

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

Bryan Gin-ge Chen (Feb 27 2020 at 17:52):

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

Rob Lewis (Feb 27 2020 at 17:54):

Still waiting on input from Paul-Nicolas.

Kevin Buzzard (Feb 27 2020 at 17:58):

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 (Feb 27 2020 at 17:59):

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

Scott Morrison (Feb 27 2020 at 18:02):

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 (Feb 27 2020 at 18:05):

Oh so it does come out nice in the end.

Kevin Buzzard (Feb 27 2020 at 18:06):

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 (Feb 27 2020 at 18:07):

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

Nicholas McConnell (Feb 27 2020 at 18:14):

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

Scott Morrison (Feb 27 2020 at 19:32):

@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 (Feb 27 2020 at 19:35):

Scratch that.

Alex J. Best (Feb 27 2020 at 19:59):

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 (Feb 27 2020 at 20:09):

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

Nicholas McConnell (Feb 28 2020 at 03:38):

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 (Feb 28 2020 at 03:43):

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 (Feb 28 2020 at 03:56):

Thanks

Nicholas McConnell (Feb 28 2020 at 04:03):

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 (Feb 28 2020 at 04:04):

That's a general theorem about ordered rings

Nicholas McConnell (Feb 28 2020 at 04:04):

Yeah, so is there a Lean command for it?

Mario Carneiro (Feb 28 2020 at 04:04):

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

Mario Carneiro (Feb 28 2020 at 04:05):

oh hey mul_neg_of_pos_of_neg :)

Scott Morrison (Feb 28 2020 at 04:08):

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 (Feb 28 2020 at 04:41):

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

Scott Morrison (Feb 28 2020 at 04:42):

(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 (Feb 28 2020 at 05:22):

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 (Feb 28 2020 at 05:23):

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

Johan Commelin (Feb 28 2020 at 05:24):

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

Johan Commelin (Feb 28 2020 at 05:25):

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 (Feb 28 2020 at 05:41):

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

Andrew Ashworth (Feb 28 2020 at 05:42):

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

Johan Commelin (Feb 28 2020 at 05:43):

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

Jalex Stark (Feb 28 2020 at 06:04):

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 (Feb 28 2020 at 06:06):

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 (Feb 28 2020 at 06:08):

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

Jalex Stark (Feb 28 2020 at 06:09):

I guess the other way is just coercion

Mario Carneiro (Feb 28 2020 at 06:09):

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


Last updated: Dec 20 2023 at 11:08 UTC