monomial diamond?

Stream: maths

[Thomas Browning]

This code throws an error that looks like a diamond-ish error. Two different instances of has_zero?

import data.polynomial.basic

open polynomial

example {i j : ℕ} {a b : ℤ} : (monomial i a + monomial j b).support ⊆ {i, j} :=
begin
  refine finset.subset.trans (@finsupp.support_add ℕ ℤ _ (monomial i a) (monomial j b)) _,
  have key := finset.union_subset_union (support_monomial' i a) (support_monomial' j b),
  -- this doesn't work: apply finset.subset.trans key,
  -- this doesn't work: refine finset.subset.trans key _,
  have key' : ({i} : finset ℕ) ∪ ({j} : finset ℕ) ⊆ ({i, j} : finset ℕ),
  { apply finset.union_subset,
    all_goals { rw [finset.singleton_subset_iff, finset.mem_insert] },
    exact or.inl rfl,
    exact or.inr (finset.mem_singleton_self j) },
  have key'' := finset.subset.trans key key',
  exact key'',
end

invalid type ascription, term has type
  @finsupp.support ℕ ℤ
        (@mul_zero_class.to_has_zero ℤ
           (@monoid_with_zero.to_mul_zero_class ℤ (@semiring.to_monoid_with_zero ℤ int.semiring)))
        (⇑(@monomial ℤ int.semiring i) a) ∪
      @finsupp.support ℕ ℤ
        (@mul_zero_class.to_has_zero ℤ
           (@monoid_with_zero.to_mul_zero_class ℤ (@semiring.to_monoid_with_zero ℤ int.semiring)))
        (⇑(@monomial ℤ int.semiring j) b) ⊆
    {i, j}
but is expected to have type
  @finsupp.support ℕ ℤ (@add_monoid.to_has_zero ℤ int.add_monoid) (⇑(@monomial ℤ int.semiring i) a) ∪
      @finsupp.support ℕ ℤ (@add_monoid.to_has_zero ℤ int.add_monoid) (⇑(@monomial ℤ int.semiring j) b) ⊆
    {i, j}

[Mario Carneiro]

convert key'' works

[Mario Carneiro]

If you use set_option pp.notation false you will see that the error is

@has_subset.subset (finset nat) (@finset.has_subset nat)
    (@has_union.union (finset nat) (@finset.has_union nat (λ (a b : nat), (λ (a b : nat), nat.decidable_eq a b) a b))
 ...
but is expected to have type
  @has_subset.subset (finset nat) (@finset.has_subset nat)
    (@has_union.union (finset nat) (@finset.has_union nat (λ (a b : nat), classical.prop_decidable (@eq nat a b)))
...

[Mario Carneiro]

i.e. the problem is in the decidability instance found for the finset union

[Thomas Browning]

is there a better workaround than convert? (it would be nice to able to use apply or refine)

[Mario Carneiro]

This is an issue in the statement of finsupp.support_add

[Mario Carneiro]

changing the lemma to

lemma support_add [decidable_eq α] {g₁ g₂ : α →₀ M} : (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support :=
support_zip_with

fixes the issue

[Mario Carneiro]

although you have to add decidability arguments to other theorems upstream of it too

[Thomas Browning]

should I PR this change?

[Mario Carneiro]

I'm already on it

[Mario Carneiro]

#6333