# 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: May 11 2021 at 16:22 UTC