Inconsistent hypothesis convention in `Finsupp`

Stream: mathlib4

[Artie Khovanov]

Let's say you want to simplify (fun₀ | 0 => x | 1 => y) n in the case where you know 1 < n. Let me take you through the simplifcation chain.

First, Lean uses Finsupp.coe_update to bring the goal to Function.update (⇑fun₀ | 0 => x) 1 y n.

Then Lean reduces using Function.update_of_ne, which takes the hypothesis n ≠ 1.

Finally, Lean reduces using Finsupp.single_eq_of_ne, which takes the hypothesis 0 ≠ n.

So the call has to be something like simp [show 0 ≠ i ∧ i ≠ 1 by omega]. Getting the inequalities the wrong way around means the proof breaks.

So, the question: I want to change these to have the same hypothesis direction. Do we want n ≠ 0 or 0 ≠ n?

[Yaël Dillies]

n ≠ ... seems to me like the obvious choice

[Artie Khovanov]

The inconsistency comes back to the RHS of Finsupp.single_apply, which reads
(single a b) a' = if a = a' then b else 0, having the condition a = a' the wrong way around relative to the actual definition of Finsupp.single.

And indeed, the proof of this lemma has a tell-tale eq_comm:

theorem single_apply [Decidable (a = a')] : single a b a' = if a = a' then b else 0 := by
  classical
  simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]

But wait, why do we need simp_rw? And what's up with that highly specific Decidable instance in our noncomputable Finsupp theory?

Well, ite requires its condition to be decidable. If we just write the "corrected" proof naively, this leads to an issue:

theorem single_apply [Decidable (a' = a)] : single a b a' = if a' = a then b else 0 := by
  classical
  rw [single, coe_mk, Pi.single_apply]
  rfl -- error

Tactic `rfl` failed: The left-hand side
  @ite M (a' = a) (Classical.decEq α a' a) b 0
is not definitionally equal to the right-hand side
  @ite M (a' = a) inst✝ b 0

So why doesn't the existing proof run into this problem? Well, the eq_comm creates a classical instance to decide a = a'! That's also why we need simp_rw: otherwise we get a "motive isn't type correct" error.

[Artie Khovanov]

At least I know now why nobody else has tried to clean up this inconsistency yet..
PR coming soon, we'll see if anyone wants to touch it :joy:

[Artie Khovanov]

By the way, I propose removing the Decidable instance

theorem single_apply :
    haveI := Classical.decEq α
    single a b a' = if a' = a then b else 0 := by
  classical
  rw [single, coe_mk, Pi.single_apply]

(which is what the definition of Finsupp.apply already does).

[Yaël Dillies]

This is bad, because you've effectively specialised the RHS to Classical.dec instead of an arbitrary Decidable (a' = a) instance

[Eric Wieser]

I think this lemma is intended to match docs#Pi.single_apply

[Eric Wieser]

It looks like it doesn't though, so indeed we could flip the arguments

[Artie Khovanov]

Yaël Dillies said:

This is bad, because you've effectively specialised the RHS to Classical.dec instead of an arbitrary Decidable (a' = a) instance

Sure. The existing proof still only goes through for nonsense reasons. Do you know how to actually fix it?

[Kevin Buzzard]

Put back the decidable instance?

[Artie Khovanov]

Artie Khovanov said:

If we just write the "corrected" proof naively, this leads to an issue:

theorem single_apply [Decidable (a' = a)] : single a b a' = if a' = a then b else 0 := by
  classical
  rw [single, coe_mk, Pi.single_apply]
  rfl -- error

Tactic `rfl` failed: The left-hand side
  @ite M (a' = a) (Classical.decEq α a' a) b 0
is not definitionally equal to the right-hand side
  @ite M (a' = a) inst✝ b 0

That leads to this issue. I guess I could simp_rw with eq_comm twice, but I wanted to know the real fix.

[Kevin Buzzard]

Find and squash the classical instance which has been inserted in the proof?

[Artie Khovanov]

Kevin Buzzard said:

Find and squash the classical instance which has been inserted in the proof?

There has to be a classical instance inserted in the proof - the definition of single_apply uses a classical instance for its ite! This lemma is effectively a generalisation.

[Yaël Dillies]

convert Pi.single_apply .. or even convert rfl should work as the full proof

[Artie Khovanov]

theorem single_apply [Decidable (a' = a)] : single a b a' = if a' = a then b else 0 := by
  classical
  rw [single, coe_mk, Pi.single_apply]
  congr

:tada:

[Dexin Zhang]

Is there a reason we can't have both?

[Artie Khovanov]

No, but I think the preferred one should be the one that matches the definition and also the intuitive usage. I want to move Finsupp.single_eq_of_ne to Finsupp.single_eq_of_ne', by analogy to Pi.single_eq_of_ne', but I do think single_apply should be the thing I wrote and not the thing it currently is.

[Artie Khovanov]

#29006

[Artie Khovanov]

Didn't touch single_apply yet, only single_eq_of_ne