# Zulip Chat Archive

## 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 [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 (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