norm_cast and int.sub_nat_nat

Stream: general

[Johan Commelin]

I've got the following code:

lemma nat.choose_mul_succ_eq : ∀ (n k : ℕ),
  (n.choose k) * (n + 1) = ((n+1).choose k) * (n + 1 - k)
| _ 0 := by simp
| n (k+1) :=
begin
  by_cases hk : n < k + 1,
  { rw [nat.choose_eq_zero_of_lt hk, nat.sub_eq_zero_of_le hk, zero_mul, mul_zero] },
  push_neg at hk,
  rw nat.choose_succ_succ,
  rw [add_mul, nat.succ_sub_succ],
  rw ← nat.choose_succ_right_eq,
  rw [← nat.succ_sub_succ, nat.mul_sub_left_distrib],
  symmetry,
  apply nat.add_sub_cancel',
  replace hk : k + 1 ≤ n + 1 := le_add_right hk,
  exact nat.mul_le_mul_left _ hk,
end

example (n : ℕ)
  (k : ℕ) (hk : k < n) :
  (nat.choose (nat.succ n) k : ℚ) * (↑n + 1 - ↑k) = ↑(nat.choose n k) * ↑(n + 1) :=
begin
  rw_mod_cast nat.choose_mul_succ_eq n k,
  -- ⊢ ↑(nat.choose (nat.succ n) k) * int.sub_nat_nat (n + 1) k =
  -- ↑(nat.choose (n + 1) k * (n + 1 - k))
end

As you can see, I end up with int.sub_nat_nat after a rw_mod_cast. To me, that isn't exactly expected behaviour. Is this the way it's supposed to be, or is there some bad lemma somewhere?

[Floris van Doorn]

It seems that the move_cast attribute on cast_sub_nat_nat causes this. Since move_cast-lemmas are (sometimes) rewritten backwards, you get the ugly function.
I also noticed this. I want to add the attribute attribute [move_cast] nat.add_one, so that we rewrite succ n to n + 1 in norm_cast.
But does this mean that in certain situations it will rewrite nat.add_one in the forward direction, so that we rewrite n + 1 to succ n? (also, int.coe_nat_succ is marked with [move_cast] but it doesn't seem to fire; is the direction reversed?)

@Paul-Nicolas Madelaine: what is the best way to deal with these rewrite rules that you only want to rewrite in a single direction, but never in the other one? Does #1103 relate to any of this?

[Rob Lewis]

I think you should be able to make it work if you tag it [squash_cast] instead. But yes, this will change with #1103.