Stream: maths

Topic: monomial diamond?

Thomas Browning (Feb 21 2021 at 02:28):

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 (Feb 21 2021 at 02:32):

convert key'' works

Mario Carneiro (Feb 21 2021 at 02:34):

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 (Feb 21 2021 at 02:34):

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

Thomas Browning (Feb 21 2021 at 02:41):

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

Mario Carneiro (Feb 21 2021 at 02:42):

This is an issue in the statement of finsupp.support_add

Mario Carneiro (Feb 21 2021 at 02:43):

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 (Feb 21 2021 at 02:43):

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

Thomas Browning (Feb 21 2021 at 02:48):

should I PR this change?