Stream: Is there code for X?
Topic: Inline type hints
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?
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
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 := begin have : (0:ℤ) ≤ c := int.coe_zero_le c, linarith, end
Alex J. Best (Nov 15 2020 at 01:03):
Last updated: May 16 2021 at 05:21 UTC