doc(data/finsupp): module docs and docstrings

[bryangingechen]

In the first commit, I added missing docstrings and module docs to data.finsupp. Some of the docstrings might be a bit wordy – feel free to suggest revisions.

The second commit does some cleanup on the proofs, including some squeeze_simp-powered speed up of some simps as well as removing some unnecessary haveI := classical.dec and some finsupp prefixes.

Question: do we need both finsupp.of_multiset and multiset.to_finsupp? They look the same to me, but maybe I'm missing something.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• make sure definitions and lemmas are not redundant

[robertylewis]

Thanks for the effort! I think "finitely supported" without a hyphen is correct, although I don't mind being shown otherwise.

Do the simp -> simp only changes make a big performance difference? There are reasons to prefer the full simp if it doesn't matter to the speed. I guess the changes are probably fine, mostly just curious.

[robertylewis]

Was this slow before? I didn't open it in an editor but this looks like a fine use of simp to me.

[bryangingechen]

I'll do some tests with the built-in profiler, but for most of the simps there was a noticeable lag when recompiling after edits in VS Code (which may or may not be reliable).

[bryangingechen]

Here's the relevant output with just (by simp) (note the 751 ms time):

finsupp.lean:122:60: information
elaboration: tactic compilation took 5.49ms
finsupp.lean:122:60: information tactic profile data
elaboration: tactic execution took 751ms
num. allocated objects:  88
num. allocated closures: 86
  751ms   100.0%   tactic.istep
  751ms   100.0%   tactic.istep._lambda_1
  751ms   100.0%   _interaction
  751ms   100.0%   tactic.interactive.propagate_tags
  751ms   100.0%   tactic.step
  751ms   100.0%   _interaction._lambda_2
  751ms   100.0%   scope_trace
  751ms   100.0%   tactic.interactive.simp_core
  608ms    81.0%   tactic.mk_simp_set
  608ms    81.0%   tactic.mk_simp_set_core
  607ms    80.8%   simp_lemmas.mk_default
  607ms    80.8%   tactic.join_user_simp_lemmas
  142ms    18.9%   tactic.simp_target
  142ms    18.9%   tactic.interactive.simp_core_aux
  142ms    18.9%   interaction_monad_orelse
  142ms    18.9%   tactic.simplify
  142ms    18.9%   tactic.interactive.simp_core_aux._lambda_5
    1ms     0.1%   simp_lemmas.erase
    1ms     0.1%   tactic.exact
    1ms     0.1%   tactic.try
    1ms     0.1%   tactic.try_core
    1ms     0.1%   tactic.triv

And here's the output with (by simp only [...]) (note the 158 ms time):

finsupp.lean:122:60: information
elaboration: tactic compilation took 4.67ms
finsupp.lean:122:60: information tactic profile data
elaboration: tactic execution took 158ms
num. allocated objects:  235
num. allocated closures: 221
  158ms   100.0%   tactic.istep
  158ms   100.0%   tactic.istep._lambda_1
  158ms   100.0%   scope_trace
  158ms   100.0%   tactic.interactive.simp_core
  158ms   100.0%   _interaction._lambda_2
  158ms   100.0%   _interaction
  158ms   100.0%   tactic.interactive.propagate_tags
  158ms   100.0%   tactic.step
  157ms    99.4%   interaction_monad_orelse
  157ms    99.4%   tactic.interactive.simp_core_aux
  157ms    99.4%   tactic.interactive.simp_core_aux._lambda_5
  157ms    99.4%   tactic.simp_target
  156ms    98.7%   tactic.simplify
    1ms     0.6%   tactic.mk_simp_set
    1ms     0.6%   tactic.mk_app
    1ms     0.6%   simp_lemmas.append_pexprs
    1ms     0.6%   simp_lemmas.resolve_and_add
    1ms     0.6%   simp_lemmas.add_pexpr
    1ms     0.6%   tactic.replace_target
    1ms     0.6%   report_invalid_simp_lemma
    1ms     0.6%   string.push
    1ms     0.6%   tactic.mk_id_eq
    1ms     0.6%   tactic.mk_simp_set_core

What are the reasons for preferring full simp in the final proof by the way? My feeling was that more explicit is better (particularly since we make lots of changes to the simp set in mathlib).

[robertylewis]

Okay, that's a big enough improvement that I'll buy it!

What are the reasons for preferring full simp in the final proof by the way?

simp only is more robust in the middle of a proof when you need control over the resulting goal. For finishing a proof, full simp will be more robust to renaming or modifying lemmas. It's a good test when making changes to the simp set that calls to simp don't suddenly fail to finish a goal. It makes for more readable proof scripts.

[robertylewis]

"needs filtered" is a lovely example of Pennsylvania dialect ;) (I agree with the change!)