Zulip Chat Archive

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?

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

I'm already on it

Mario Carneiro (Feb 21 2021 at 03:16):

#6333


Last updated: Dec 20 2023 at 11:08 UTC