push_cast

Stream: Is there code for X?

[Stuart Presnell]

I'm trying to push a coercion past a finset.prod. In this example, with ℕ and ℚ, the goal is closed with push_cast:

example {α : Type*} (s : finset α) {h : α → ℕ} :
  ∏ (a : α) in s, (↑(h a): ℚ) = ↑∏ (a : α) in s, h a :=
begin
  push_cast,
end

but when I generalise from ℕ and ℚ to β and γ, it no longer works

example {α β γ : Type*} (s : finset α) {h : α → β} [comm_monoid β] [comm_monoid γ] [has_coe β γ] :
  ∏ (a : α) in s, (↑(h a): γ) = ↑∏ (a : α) in s, h a :=
begin
  push_cast,
  sorry,
end

Is there some further attribute I need to add, or something else I can change to make this work more generally?

[Mario Carneiro]

you almost never want to assume has_coe β γ, since it's an arbitrary function in this case

[Mario Carneiro]

Instead, replace ↑ with a function f satisfying certain properties; in this case I think you want it to be a group hom

[Mario Carneiro]

and I think the theorem is docs#monoid_hom.map_prod

[Stuart Presnell]

That's great, thank you

[Stuart Presnell]

A related question: in a proof I'm working on I have and expression of the form ↑(f.prod g) (where f : α →₀ M) and I'd like to transform it to something of the form f.prod (λ a b, (↑(g a b):ℚ)). In the example below, if I unfold finsupp.prod to finset.prod then norm_cast can immediately close the goal (or push_cast also works). But without the unfolding these tactics fail. Is there an alternative tactic or a variant of push_cast or norm_cast that can do this?

import data.finsupp
import algebra.big_operators.basic

open_locale big_operators

example {α M N : Type*} [has_zero M] {f : α →₀ M} (g : α → M → ℕ) :
  ↑(f.prod g) = f.prod (λ a b, (↑(g a b):ℚ)) :=
begin
  unfold finsupp.prod,
  norm_cast,
end

(btw, I'm aware that push_cast [finsupp.prod] closes this goal in one step, but in the proof I'm working on this leaves me with an expression in terms of finset.prod, and I'm hoping to remain within the world of finsupp.)

[Johan Commelin]

If library_search doesn't find that lemma, then it's probably missing.

[Johan Commelin]

@Eric Wieser What is the best way forward here? Do we need a new lemma for every coercion that preserves multiplication?

[Eric Wieser]

I think that's the way we currently handle things, yes.

[Eric Wieser]

Eg we have docs#monoid_hom.map_finsupp_prod and docs#monoid_hom.map_prod, so in the same way we need docs#nat.cast_prod (exists) and docs#nat.cast_finsupp_prod (doesn't exist)

[Eric Wieser]

With the old-style is_monoid_hom typeclasses we maybe could have avoided that repetition by just having is_monoid_hom.map_finsupp_prod and not needing the cast version as it would fall out from is_monoid_hom coe, but at least in Lean3 that didn't work with simp

[Anne Baanen]

I'm thinking about defining has_coe subclasses that state the coercion is a monoid/ring hom. We can also use those to get back the "there exists a canonical ring hom" usages of algebra (since the plan is to remove the defeqness of @@algebra_map _ _ (ring_hom.to_algebra f) = f).

[Stuart Presnell]

I've just submitted #10579 to add nat.cast_finsupp_prod and nat.cast_finsupp_sum (and likewise for int) to data/finsupp/basic.

[Eric Wieser]

Thanks!