Zulip Chat Archive

Stream: new members

Topic: Cast with apply


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

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

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

view this post on Zulip Kevin Buzzard (Oct 29 2019 at 00:36):

(typo 2 - 3 = 0)

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

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