Zulip Chat Archive

Stream: Is there code for X?

Topic: Inline type hints

view this post on Zulip Chase Norman (Nov 15 2020 at 00:56):

I'm having trouble proving the statement ↑a ≤ ↑b - ↑c → a ≤ b where a, b and c are natural numbers and they are lifted to integers. I cannot even create a lemma which states this fact because lean understandably does not know what type to lift to. How can I provide a type hint to this effect? Alternatively, if there was a way to remove lifts from a hypothesis ("unzify") that would be helpful to proceed. Any ideas?

view this post on Zulip Alex J. Best (Nov 15 2020 at 01:02):

To make the lemma you can explicitly cast like this

example (a b c : ) : (a : )  (b : ) - (c : )  a  b := sorry

view this post on Zulip Heather Macbeth (Nov 15 2020 at 01:03):

And you can solve it by explicitly invoking the fact that 0 ≤ c:

import tactic

example (a b c : ) (h : (a:)  b - c) : a  b :=
  have : (0:)  c := int.coe_zero_le c,

view this post on Zulip Alex J. Best (Nov 15 2020 at 01:03):

unzify would be tactic#lift I think, there is also tactic#norm_cast which is very useful in this sort of situation.

Last updated: May 16 2021 at 05:21 UTC