## Stream: general

### Topic: norm_cast and int.sub_nat_nat

#### Johan Commelin (Feb 01 2020 at 10:31):

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 ← nat.choose_succ_right_eq,
rw [← nat.succ_sub_succ, nat.mul_sub_left_distrib],
symmetry,
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 (Feb 04 2020 at 13:15):

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 (Feb 04 2020 at 13:23):

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

Last updated: May 15 2021 at 00:39 UTC