finsupp.support_erase

Stream: new members

[Stuart Presnell]

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]

finsupp is meant to be used entirely classically.

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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]

The problem here is finsupp.support_erase is stated badly

[Stuart Presnell]

How so? What would be a better statement?

[Eric Wieser]

It's missing a [decidable_eq _] argument

[Yakov Pechersky]

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]

It belongs in the lemmas but not the definitions

[Eric Wieser]

Indeed the definitions should avoid such arguments

[Eric Wieser]

PR'd as #10649

[Eric Wieser]

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]

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]

required header for c+p:

import data.finsupp.basic

open finsupp

[Eric Rodriguez]

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

[Eric Rodriguez]

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]

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

[Eric Rodriguez]

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

[Eric Rodriguez]

subset_insert seems to be stated correctly, anyways

[Eric Rodriguez]

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]

We never wrote a linter for that

[Eric Wieser]

I started writing one but didn't finish

[Yakov Pechersky]

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]

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

[Eric Wieser]

Lemmas should always be generalized to _any_ decidable instance

[Yakov Pechersky]

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

[Yakov Pechersky]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/timeout.20when.20working.20with.20ideal.20of.20polynomial.20ring #1391

[Eric Wieser]

And the linter to catch it

[Eric Wieser]

#10672 fixes most of these in finsupp/basic

[Eric Wieser]

(and CI is now happy with it)