norm_cast not behaving as expected

Stream: general

[Johan Commelin]

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 `coe`s.
  ring,
end

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

Aha, that makes sense.

[Johan Commelin]

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

[Rob Lewis]

I think push_cast would just be a simp set.

[Johan Commelin]

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]

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