## Stream: new members

### Topic: finsupp.support_erase

#### Stuart Presnell (Dec 06 2021 at 16:27):

Could someone explain what's going wrong here?

example {α : Type*} {M : Type*} [decidable_eq α] [has_zero M] (f : α →₀ M) (a : α) :
(finsupp.erase a f).support = f.support.erase a :=
begin
rw finsupp.support_erase,
sorry,
end


The documentation for docs#finsupp.support_erase seems to indicate that it should be exactly what I need here:

theorem finsupp.support_erase  {α : Type u_1}  {M : Type u_5}  [has_zero M] {a : α}  {f : α →₀ M} :
(finsupp.erase a f).support = f.support.erase a


However, the rw leaves me with a goal of f.support.erase a = f.support.erase a which refl doesn't close.

Clicking on the two expressions in the Infoview indicates that the left side involves

λ (a b : α), classical.prop_decidable (a = b)


while the right side involves

λ (a b : α), _inst_1 a b


(where _inst_1: decidable_eq α).

But commenting out [decidable_eq α] produces an error.

Is this perhaps an example of a diamond?

#### Yakov Pechersky (Dec 06 2021 at 16:28):

finsupp is meant to be used entirely classically.

#### Yakov Pechersky (Dec 06 2021 at 16:29):

If you want to make statements about decidable finitely supported functions, those are dfinsupp

#### Yakov Pechersky (Dec 06 2021 at 16:30):

In your case, the tactic that should be able to solve your sorry is congr. Or even "convert finsupp.support_erase" for the whole tactic.

#### Yakov Pechersky (Dec 06 2021 at 16:30):

This isn't a diamond, more like a triangle. You have two conflicting instances of decidable equality, one from your hypothesis, and one from your lemma.

#### Eric Wieser (Dec 06 2021 at 16:42):

The problem here is finsupp.support_erase is stated badly

#### Stuart Presnell (Dec 06 2021 at 16:43):

How so? What would be a better statement?

#### Eric Wieser (Dec 06 2021 at 16:44):

It's missing a [decidable_eq _] argument

#### Yakov Pechersky (Dec 06 2021 at 16:49):

We had this discussion last time when I added erase to polynomial, that adding that type of constraint is not in line with how the rest of the polynomial library is written. And my understanding was that that was because of its finsupp implementation

#### Eric Wieser (Dec 06 2021 at 16:50):

It belongs in the lemmas but not the definitions

#### Eric Wieser (Dec 06 2021 at 16:50):

Indeed the definitions should avoid such arguments

PR'd as #10649

#### Eric Wieser (Dec 06 2021 at 22:52):

Yakov Pechersky said:

If you want to make statements about decidable finitely supported functions, those are dfinsupp

While true that these are "more decidable", the d stands for dependent not decidable AFAIK.

#### Stuart Presnell (Dec 08 2021 at 15:34):

I've just run into what looks like a similar issue while investigating something for #10651:

example {α : Type*} {M : Type*} [decidable_eq α] [has_zero M]
{f : α →₀ M} {x q : α} {b : M} (hb : b ≠ 0)  (h : x ∈ f.support) : x ∈ (f.update q b).support :=
begin
simp only [support_update_ne_zero _ _ hb],
have := (finset.subset_insert q f.support) h,
-- exact this,   -- Doesn't work
convert this,
end


The have line produces this: x ∈ insert q f.support, which is the current goal. But the exact line generates the following error:

invalid type ascription, term has type
x ∈ @insert α (finset α) (@finset.has_insert α (λ (a b : α), (λ (a b : α), _inst_1 a b) a b)) q f.support
but is expected to have type
x ∈ @insert α (finset α) (@finset.has_insert α (λ (a b : α), classical.prop_decidable (a = b))) q f.support


(where _inst_1 : decidable_eq α).

#### Eric Rodriguez (Dec 08 2021 at 15:57):

required header for c+p:

import data.finsupp.basic

open finsupp


#### Eric Rodriguez (Dec 08 2021 at 16:03):

the error befuddles me, but you should be doing this in a different way anyways, actually

#### Eric Rodriguez (Dec 08 2021 at 16:04):

if you change that example to a lemma and run #lint, it'll tell you that you should use classical as the decidable_eq is only needed in the proof, not the statement

#### Eric Rodriguez (Dec 08 2021 at 16:04):

so if you letI := classical.prop_decidable at the start of your proof, you're good

#### Eric Rodriguez (Dec 08 2021 at 16:04):

but I'm really not sure why if you feed that argument specifically anyways, it still wants to use classical.prop_decidable

#### Eric Rodriguez (Dec 08 2021 at 16:05):

subset_insert seems to be stated correctly, anyways

#### Eric Rodriguez (Dec 08 2021 at 16:11):

oh, the issue is that support_update_ne_zero doesn't take in a decidable_eq. how come the linter doesn't warn about this? was this part of the push to make finsupp mathematician-friendly?

#### Eric Wieser (Dec 08 2021 at 16:21):

We never wrote a linter for that

#### Eric Wieser (Dec 08 2021 at 16:21):

I started writing one but didn't finish

#### Yakov Pechersky (Dec 08 2021 at 16:24):

The whole file was written with open_locale classical, this is what I was saying the other day. src#finsupp.support_update_ne_zero

#### Eric Wieser (Dec 08 2021 at 16:26):

The right outlook to take is "the definitions in this file use noncomputable classical instances", not "this file uses noncomputable instances throughout"

#### Eric Wieser (Dec 08 2021 at 16:27):

Lemmas should always be generalized to _any_ decidable instance

#### Yakov Pechersky (Dec 08 2021 at 16:27):

I agree with you in principle. But there's a larger cleanup necessary to make that actually be the case.

#### Eric Wieser (Dec 08 2021 at 16:27):

And the linter to catch it

#### Eric Wieser (Dec 08 2021 at 16:42):

#10672 fixes most of these in finsupp/basic

#### Eric Wieser (Dec 08 2021 at 18:37):

(and CI is now happy with it)

Last updated: Dec 20 2023 at 11:08 UTC