issues at !4#1991 Data.Finsupp.AList

Stream: mathlib4

[Arien Malec]

Could I ask someone to look at !4#1991?

There are a few remaining issues that all appear to be defeq issues:

1. lookupFinsupp has simp_rw that do nothing despite type apparently matching

2. In lookupFinsupp_apply and lookupFinsupp_support I replaced by convert rfl with a simp that leaves the goal state
   Option.getD (lookup a l) 0 = Option.getD (lookup a l) 0 but doesn't close

3. singleton_lookupFinsupp is timing out at isDefEq

[Johan Commelin]

@Arien Malec re 1: does it help if you pass more arguments to the lemmas in the simp_rw?
re 2: does rfl close the goal after simp? If not, what does congr do?

[Arien Malec]

2. rfl does not close, but congr does....

[Arien Malec]

scratch that -- congr closes in one place, but not the other...

[Johan Commelin]

but does it make progress?

[Arien Malec]

Sort of?

I get to

(fun x => decide ¬x.snd = 0) = fun x => decide ¬x.snd = 0 which rfl doesn't close, and (fun a b => Classical.decEq α a b) = fun a b => inst✝¹ a b

inst✝¹ is DecidableEq α

[Arien Malec]

On the first simp_rw issue, I moved mem_toFinset to @mem_toFinset _ _ and got a close...

[Arien Malec]

which seems...odd

[Johan Commelin]

After congr, try apply Subsingleton.elim

[Johan Commelin]

Unfortunately congr doesn't do that on its own. In Lean 3 it did.

[Arien Malec]

huh, that closes one subgoal, but leaves (fun x => decide ¬x.snd = 0) = fun x => decide ¬x.snd = 0 unclosed

[Johan Commelin]

funext and another congr?

[Arien Malec]

Now just the timeout....

[Johan Commelin]

There should be a congr! that does those funexts and apply Subsingleton.elims for us.

[Johan Commelin]

Can you paste a bit of context for that timeout?

[Arien Malec]

@[simp]
theorem singleton_lookupFinsupp (a : α) (m : M) :
    (singleton a m).lookupFinsupp = Finsupp.single a m := by classical simp [← AList.insert_empty]

[Arien Malec]

let me see if I can minimize the full context.

[Arien Malec]

Hmm, now I get a whnf timeout rather than an isDefEq timeout...

[Johan Commelin]

Can you push? I'll try to load the PR here.

[Arien Malec]

it's all up to date...

[Johan Commelin]

ok, I'll take a look

[Arien Malec]

Here's the full context:

import Mathlib.Data.Finsupp.Basic
import Mathlib.Data.List.AList

variable {α M : Type _} [Zero M]

noncomputable def AList.lookupFinsupp (l : AList fun x : α => M) : α →₀ M
    where
  support := by
    haveI := Classical.decEq α <;> haveI := Classical.decEq M <;>
      exact (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset
  toFun a :=
    haveI := Classical.decEq α
    (l.lookup a).getD 0
  mem_support_toFun a := by
    classical
      simp_rw [@List.mem_toFinset _ _, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
      cases lookup a l <;> simp

@[simp]
theorem singleton_lookupFinsupp (a : α) (m : M) :
    (AList.singleton a m).lookupFinsupp = Finsupp.single a m := by classical simp [← AList.insert_empty]

[Johan Commelin]

@Arien Malec I pushed a fix. Here's what I did:

1. replace the proof by _. This showed that the statement didn't give errors, so the problem was with the proof.
2. aha, so probably simp is looping, or so.
3. put the tactics on their own line
4. what does simp? do? -- nothing
5. does simp only [← AList.insert_empty] make progress? -- Yes!
6. what does simp? do now? -- It closes the goal
7. clean up

[Arien Malec]

Nice heuristics!