Zulip Chat Archive

Stream: Is there code for X?

Topic: lifting sub from Q to N?


view this post on Zulip 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
  admit,
end

Maybe I'm getting something arbitrary wrong, but I had the feeling I could lift to Z\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\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 Q\mathbb{Q} to N\N directly (can_lift Q N does not exist but I didn't really search diligently)

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 03 2021 at 15:02):

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

view this post on Zulip Ryan Lahfa (Feb 03 2021 at 15:07):

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

view this post on Zulip 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?

view this post on Zulip 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