Variant of finsupp.prod_add_index?

Stream: new members

[Stuart Presnell]

By failing to search sufficiently I accidentally re-proved a variant of docs#finsupp.prod_add_index. My version differs by:

• requiring only [add_zero_class M] rather than [add_comm_monoid M]
• requiring only h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1 rather than h_zero : ∀a, h a 0 = 1
• (also, the proof is about 30% shorter)

Is this variant something worth having in mathlib? If so, what would be a good name for it? (We already have one variant called prod_add_index').

For my current purposes I could use the original prod_add_index perfectly happily, so it doesn't much matter if this variant is too small a change to be worth including.

[Yaël Dillies]

It seems like your version strictly dominates the current one, so you could substitute it! However, I'm wondering how you can do without commutativity.

[Stuart Presnell]

Here's the proof:

lemma prod_add_index'' [add_zero_class M] [comm_monoid N] {f g : α →₀ M}
  {h : α → M → N} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1)
  (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
  (f + g).prod h = f.prod h * g.prod h :=
begin
  rw [finsupp.prod_of_support_subset f (subset_union_left _ g.support) h h_zero,
      finsupp.prod_of_support_subset g (subset_union_right f.support _) h h_zero,
      ←finset.prod_mul_distrib,
      finsupp.prod_of_support_subset (f + g) finsupp.support_add h h_zero],
  exact finset.prod_congr rfl (λ x hx, (by apply h_add)),
end

[Stuart Presnell]

Is there any reason to worry that this version might break the @[to_additive] that the current version has? (I still don't have a good sense of how that particular magic works.)

[Stuart Presnell]

I guess the easiest way to find out is to try it and see what falls over!

[Eric Rodriguez]

can you post a full mwe? i seem to get no union instance on finset, which is odd to me

[Eric Rodriguez]

oh, decidable_eq \a

[Eric Rodriguez]

yeah, to_additive works fine! the way to_additive works is that it replaces the multiplicative version of every proof in the full actual proof term with the additive version - in particular, it doesn't mess with tactics, which means that it is usually very stable

[Stuart Presnell]

Hmm, in a mwe I'm getting the same complaint of no has_union (finset α), but it works fine in place in data/finsupp/basic. The output of #where just before the theorem statement doesn't include decidable_eq α.

[Eric Rodriguez]

finsupp has open_locale classical on, which I forgot at the time

[Eric Rodriguez]

the theory is like in some ways decidable but at the time it was thought mathematicians didn't want to bother with it

[Stuart Presnell]

Ah, that's what I missed.

[Stuart Presnell]

#11353

[Stuart Presnell]

So if I wanted to replace the original finsupp.prod_add_index with this new version I should (a) find all instances of the original (in this file and elsewhere), (b) replace them with my new prod_add_index'' and fix the proofs as required, and then finally (c) rename throughout — is that right?

[Eric Rodriguez]

i'd just overwrite the old prod_add_index and look for each time it's mentioned; it should be pretty painless to do this refactor

[Eric Rodriguez]

maybe the unused arguments linter will go off at some point after because some other lemmas only depended on some things for this lemma, and so on

[Stuart Presnell]

Hmm, I'm following the more cautious path that I outlined above and I'm already running into trouble at the first use.

In prod_finset_sum_index I've changed

prod_add_index h_zero h_add

to

prod_add_index'' (λ a _, h_zero a) h_add

This works to prove the lemma as stated, but @[to_additive] is raising a complaint. (If I comment out @[to_additive] and put #exit immediately after the lemma, everything is fine.)

[Stuart Presnell]

Specifically:

type mismatch at application ...
term
  _inst_2
has type
  add_comm_monoid N
but is expected to have type
  comm_monoid N

[Alex J. Best]

You'll also need to apply @[to_additive] to proad_add_index'' if a proof using it has to_additive applied

[Alex J. Best]

Most of the time you see a to_additive error like that its just because one of the things used in the proof needs to_additivizing too

[Stuart Presnell]

Stepping through the 3-step process outlined above, I've now replaced every use of prod_add_index with my new prod_add_index'' (and similarly for sum_add_index). In some places this replacement has gone through with no problems. However, in some places I've needed to change something of the form prod_add_index h1 h2 to the more verbose prod_add_index'' (λ a ha, h1 a) h2 (where h1 : ∀a, h a 0 = 1 and my new variant wants h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1).

Is there a nicer way to do this? Or should I just keep the original variant of prod_add_index as an alternative (proved as a one-liner in terms of prod_add_index'') and then in each case use whichever version is more convenient?

[Eric Wieser]

Often that means a downstream lemma could also have its hypotheses weakened

[Eric Wieser]

Can you link to some examples of where that happens?

[Stuart Presnell]

That's an interesting idea, thanks!

[Stuart Presnell]

Searching through the Files changed page of #11353 for the search term add_index'' (λ gives 9 matches. For most of these I don't see a natural choice of a subset to which a could be restricted, or else it doesn't look useful to do so.

[Stuart Presnell]

Is there something useful that could be done with polynomial.sum_add_index in data/polynomial/basic?

[Stuart Presnell]

Oh, I suppose another separate thing I could look into would be weakening the requirement of [add_comm_monoid M] (used in the original) to [add_zero_class M].

[Stuart Presnell]

After a long delay I think this is ready for review (#11353). I ended up replacing prod_add_index with the new version with weaker premises, and keeping the original as prod_add_index'. Most of the other edits are places where it was more convenient to keep using the old (now renamed) lemma.

[Stuart Presnell]

This probably ended up being more work that it was worth. I should have followed @Eric Rodriguez's advice and just replaced the lemma and fixed whatever broke, rather than trying to carefully manage the change-over.