## Stream: general

### Topic: norm_cast not behaving as expected

#### Johan Commelin (Sep 19 2019 at 08:29):

I'm having some issues with norm_cast. I'll repeat my example from the other thread:

example (k : ℕ) {x y : ℕ} :
(x * x + y * y : ℤ) - ↑((x * y + 1) * k) = ↑y * ↑y - ↑k * ↑x * ↑y + (↑x * ↑x - ↑k) :=
begin
norm_cast, -- this doesn't move enough coes.
ring,
end


#### Johan Commelin (Sep 19 2019 at 08:29):

Nevertheless, int.coe_nat_mul and friends are tagged with the move_cast attribute in tactic/norm_cast.lean

#### Scott Morrison (Sep 19 2019 at 09:49):

Isn't the problem here that norm_cast is moving casts upwards, and you want them moved downwards?

#### Scott Morrison (Sep 19 2019 at 09:53):

import tactic

example (k : ℕ) {x y : ℕ} :
(x * x + y * y : ℤ) - ↑((x * y + 1) * k) = ↑y * ↑y - ↑k * ↑x * ↑y + (↑x * ↑x - ↑k) :=
begin
-- goal is:
--  ↑x * ↑x + ↑y * ↑y - ↑((x * y + 1) * k) = ↑y * ↑y - ↑k * ↑x * ↑y + (↑x * ↑x - ↑k)
norm_cast,
-- goal is:
--  ↑(x * x + y * y) - ↑((x * y + 1) * k) = ↑(y * y) - ↑(k * x * y) + (↑(x * x) - ↑k)
sorry
end


#### Scott Morrison (Sep 19 2019 at 09:55):

norm_cast has done what it's meant to do --- pull casts upwards --- as far as it makes sense to do so --- it isn't going to convert ↑x - ↑y to ↑(x - y) because that requires the side condition y <= x.

#### Scott Morrison (Sep 19 2019 at 09:58):

The problem is just that we need a push_cast tactic here instead, which would hopefully convert the goal to

↑x * ↑x + ↑y * ↑y - ((↑x * ↑y + 1) * ↑k) = ↑y * ↑y - ↑k * ↑x * ↑y + (↑x * ↑x - ↑k)


which ring can cope with:

example (k : ℕ) {x y : ℕ} : (x : ℤ) * (x : ℤ) + (y : ℤ) * (y : ℤ) - (((x : ℤ) * (y : ℤ) + 1) * (k : ℤ)) = (y : ℤ) * (y : ℤ) - (k : ℤ) * (x : ℤ) * (y : ℤ) + ((x : ℤ) * (x : ℤ) - (k : ℤ)) :=
by ring


#### Johan Commelin (Sep 19 2019 at 10:30):

Aha, that makes sense.

#### Johan Commelin (Sep 19 2019 at 10:30):

@Rob Lewis @Paul-Nicolas Madelaine What do you think about adding a push_cast tactic to your bundle?

#### Rob Lewis (Sep 19 2019 at 13:26):

I think push_cast would just be a simp set.

#### Johan Commelin (Sep 19 2019 at 13:36):

Even if it is, it might be nice to wrap it in a tactic. push_cast is shorter than simp with push_cast.

#### Scott Morrison (Sep 20 2019 at 10:54):

I recorded this conversation as an issue, #1464. It should be pretty straightforward to add.

Last updated: Aug 03 2023 at 10:10 UTC