## Stream: Is there code for X?

### Topic: lifting sub from Q to N?

#### Ryan Lahfa (Feb 03 2021 at 14:56):

I am running into a nasty coercion issue with the following MWE:

import data.rat.basic

example (a: ℕ) (b: ℕ) (s: ℕ) (h: a ^ s - b > 0):
↑(a ^ s - b) = (a: ℚ) ^ s - (b: ℚ) :=
begin
end


Maybe I'm getting something arbitrary wrong, but I had the feeling I could lift to $\Z$ and then finish using int.coe_nat_sub as I had a proof that all of those are integers.

Maybe I could just lift to $\Z$ and prove it there and call it a day, but unsure how to actually do it, I tried many combinations of the zify tactic, lift tactic, manual coercions, norm_cast, push_cast, *_mod_cast variants without success.

Actually it seems like also there is no way to go from $\mathbb{Q}$ to $\N$ directly (can_lift Q N does not exist but I didn't really search diligently)

#### Eric Wieser (Feb 03 2021 at 15:02):

A similar example is:

example (a: ℕ) (b: ℕ) (s: ℕ) (h : b ≤ a ^ s):
↑(a ^ s - b) = (a: ℚ) ^ s - (b: ℚ) :=
begin
rw nat.cast_sub h,
simp,
end


#### Eric Wieser (Feb 03 2021 at 15:02):

Using > is only going to make things hard for you, because mathlib lemmas always use <

#### Ryan Lahfa (Feb 03 2021 at 15:07):

Indeed and it just works fine on my example (I also had < stuff in my equalities) :>

#### Ryan Lahfa (Feb 03 2021 at 15:09):

And I can just factor out the rw in the simp apparently, but I wonder if norm_cast is able to catch local hypothesis in the context and exploit them for this, as cast_sub seems to be marked for normalization of casts?

#### Kevin Buzzard (Feb 03 2021 at 17:45):

import tactic
import data.rat.basic

example (a: ℕ) (b: ℕ) (s: ℕ) (h: 0 < a ^ s - b):
↑(a ^ s - b) = (a: ℚ) ^ s - (b: ℚ) :=
begin
rw nat.cast_sub,
{ norm_cast },
{ exact le_of_lt (nat.lt_of_sub_pos h) }
end


Last updated: May 19 2021 at 03:22 UTC