push coe

Stream: general

[Johan Commelin]

I've complained that ring didn't do its job (sorry @Mario Carneiro) but I figured out what's wrong.
Here's the example that I had:

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

The reason that ring fails, is that the coercion ↑((x * y + 1) * k) first needs to be pushed through the products and sum.

[Johan Commelin]

simp can do that, but you end up with a non-terminal simp, or an ugly simp only line.

[Mario Carneiro]

does norm_cast help?

[Johan Commelin]

Nope

[Mario Carneiro]

I forget if I've said this before, but nonterminal simp is fine if it is followed by a "blasty" tactic, which doesn't care so much about the exact form of the goal

[Johan Commelin]

I guess the hom tactic would help. But it is still under construction.

[Scott Morrison]

This has nothing to do with hom, I thought.

[Scott Morrison]

Isn't this exactly the sort of thing that norm_cast and friends are for?

[Scott Morrison]

Maybe we're just missing some attributes on lemmas.

[Johan Commelin]

Ok, maybe we need to add attributes to int.coe_mul or something like that...

[Johan Commelin]

Anyway, I've pushed again. For the moment I'll just prove them with simp, ring

[Kevin Buzzard]

you can find simp, ring in complex.lean in mathlib IIRC

[Rob Lewis]

Yeah, this looks like exactly what norm_cast should do, so there's probably a missing attribute. simp, ring is fine here but norm_cast, ring would be better.