Zulip Chat Archive

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 `coe`s.
  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: Dec 20 2023 at 11:08 UTC