Stream: new members
Topic: Cast with apply
Bhavik Mehta (Oct 28 2019 at 19:53):
I'm trying to use
modeq.dvd_of_modeq in the following, and I think it's failing to unify because of the casts? How could I make this work?
invalid apply tactic, failed to unify a - 1 ∣ a ^ n - 1 with ↑?m_1 ∣ ↑?m_2 - ↑?m_3 state: a n : ℕ, ha : 2 ≤ a ⊢ a - 1 ∣ a ^ n - 1
Chris Hughes (Oct 28 2019 at 19:58):
The substraction in the statement of the theorem is natural number subtraction, which returns a natural number, and defaults to zero when the answer should be negative. So, for example
2 - 3 = 0.
There are a couple of ways around this. The easiest is to make
a an integer.
Chris Hughes (Oct 28 2019 at 20:02):
The other way is to
rw [← int.coe_nat_dvd, int.coe_nat_sub, int.coe_nat_sub] and prove that because
2 ≤ a,
a - 1 gives the same answer when done using integer subtraction.
Kevin Buzzard (Oct 29 2019 at 00:36):
2 - 3 = 0)
Bhavik Mehta (Oct 30 2019 at 19:07):
Thanks for these - I'd rather not make
a an integer since this is a lemma I need for a larger theorem
Bhavik Mehta (Oct 30 2019 at 19:09):
I can't seem to get the other way to work - the
int.coe_nat_sub looks like it's getting applied to both terms, and I only want to apply it on the right
Last updated: May 06 2021 at 22:13 UTC