Zulip Chat Archive

Stream: general

Topic: norm_cast and int.sub_nat_nat


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

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

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