Allow for Config attributes to be set directly

[FrederickPu]

Allow for Config attributes to be set directly when using initialize_simp_projection as per issue #19895
Basically modified initialize_simp_projection so that the user has the option of specifying a tuple of config option values.
Ex:

initialize_simp_projection MulEquiv (toFun → apply, invFun → symm_apply) (fullyApplied := false)

These config options are then converted into projections.
 ---

[FrederickPu]

Please note that the current code may not work, and only intended to sketch the general approach as the PR is still in draft

[github-actions]

PR summary cd065b4a1f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ applyConfigOptions
+ elabConfigOption

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[fpvandoorn]

The simps configuration options should be split in two: lemma-specific configuration (fullyApplied/simpRhs/isSimp/attrs), and "general" configuration options that are for a full attribute application (the rest, I think - most of them decide which simp-lemmas will be generated by this attribute).

My plan - once I have time - was to:

• split up the configuration options in two, as described above.
• the general configuration options can only be placed directly after the word simps in the attribute
• for the lemma-specific configuration options, allow to specify them in three locations: after a specific projection in the initialize_simps_projections command, after the word simps, and after the projection name (and potentially a 4th location: directly after the word initialize_simps_projections which then applies to all projections). There should be a precedence where if a user specifies it for a projection name that should have the highest priority, otherwise look at the value for the simps call, otherwise look at the value given by the initialize_simps_projections-call (for the last projection applied), and otherwise it has the default value. To do this, I was planning to change the type of all these configuration options to Option ... so that we can detect whether the user has specified its value.
• Complication: this design probably conflicts with Kyle's nice +isSimp -fullyApplied syntax. Probably good to discuss this with Kyle to see if there is a solution (maybe by changing this design).
• To store the configuration option, need to add a field config with lemma-specific configuration to ProjectionData (and ParsedProjectionData)

Does this make sense?

[FrederickPu]

I'm not quite sure what you mean by "the general configuration options can only be placed directly after the word simps in the attribute". Also what is the mechanism for actually storing the config options? I notice for the projections you're writing to a NameMapExtension. Where when does the data from the NameMapExtension actually get used to create a config type? Overall, I think I'm just having a bit of trouble understanding the data lifecycle.

[fpvandoorn]

Here an entry to the environment extension gets written. This never gets modified afterwards:

mathlib4/Mathlib/Tactic/Simps/Basic.lean

Line 828 in cd065b4

structureExt.add str (rawLevels, projs)

Currently there is no Config options in this environment extension, but it will be if you add some Config options to ProjectionData

I'm not quite sure what you mean by "the general configuration options can only be placed directly after the word simps in the attribute".

Currently, the syntax for the simps attribute is @[simps (config options)? (list of names)], e.g. @[simps (config := {}) apply symm_apply].
If we make some configuration options lemma-specific, then these options should be applied to only one lemma, e.g. @[simps (config := {rhsMd := .none}) coe (config := {fullyApplied := false}) apply]. Here the second config option will only be used for the lemma coe, not for the lemma apply.

But maybe I'm overcomplicating things, and it's fine if we only allow such options in the initialize_simps_projections command?

@urkud @YaelDillies @sgouezel and others might have an opinion on the design. (We can also move this to a Zulip thread.)

[FrederickPu]

don't you already need to encode some config options in order to support the + and - notation.
Also, how does structureExt work, like where is the value of structureExt being read?

[fpvandoorn]

The configuration elaborator gets generated here, with :

mathlib4/Mathlib/Tactic/Simps/Basic.lean

Line 904 in cd065b4

declare_command_config_elab elabSimpsConfig Config

It requires that the syntax gets declared as optConfig:

mathlib4/Mathlib/Tactic/Simps/Basic.lean

Line 133 in cd065b4

syntax simpsArgsRest := Tactic.optConfig (ppSpace ident)*

Place where structureExt gets read:

mathlib4/Mathlib/Tactic/Simps/Basic.lean

Line 803 in cd065b4

if let some data := (structureExt.getState env).find? str then

Do you have prior experience with metaprogramming? This might be a bit too complicated as a first metaprogramming task.

[FrederickPu]

I've done quite a bit of metaproggraming in lean3 and I've worked my way through most of the lean4 metaproggraming book. I think I have a pretty good understanding of elaborators as well as the metaprogramming monad system. I think my main weakness is understanding how things get stored in the environment such as NamedMapExtension

[FrederickPu]

So how does getRawProjections get used. Cause it seems like the return value is just thrown out:

/-- Function elaborating `initialize_simps_projections`. -/
@[command_elab «initialize_simps_projections»] def elabInitializeSimpsProjections : CommandElab
  | stx@`(initialize_simps_projections $[?%$trc]? $id $[($stxs,*)]? $[($stxs',*)]?) => do
    let stxs := stxs.getD <| .mk #[]
    let rules ← stxs.getElems.raw.mapM elabSimpsRule
    let stxs' := stxs'.getD <| .mk #[]
    let configs ← stxs'.getElems.raw.mapM elabConfigOption
    let nm ← resolveGlobalConstNoOverload id
    _ ← liftTermElabM <| addTermInfo id.raw <| ← mkConstWithLevelParams nm
    _ ← liftCoreM <| getRawProjections stx nm true rules trc.isSome configs
  | _ => throwUnsupportedSyntax

Is its purpose in the elaborator just to write to to structureExt using structureExt.add?
I'm trying to understand where the output of getRawProjections is actually being used. Which to my current understanding seems to be in getProjectionExprs which is used in addProjections which is used in simpsTac

[YaelDillies]

Oh wow! Thank you for this PR, this is a great Christmas present. I was quite literally looking for someone to nerdsnipe into reducing the amount of pain in my PR #19860. Let's discuss the details on Zulip.