UsedSimps vs. simpTheorems?

Stream: lean4

[Thomas Murrills]

What's the use of the usedSimps argument in simp and dsimp, and how does it differ from the simpTheorems field in the Simp.Context?

Let me also explain what I'm trying to do, to avoid an #xy situation: the mono tactic in mathlib3 unfolds the definitions monotone and strict_mono in theorems that it matches via dsimp.

In the mathlib4 version that I'm writing, this would mean that Monotone and StrictMono ought to be unfolded (and the result telescoped) before we add a given theorem to the discrimination tree. (And that we ought to unfold them in goals we're trying to prove.)

Is dsimp the way to go, or is there a better way to unfold these on the meta level than by using dsimp with Monotone and StrictMono somehow?

(I'm also wondering about whether it'll then be legal to use the proofs of theorems that refer to Monotone in the type as-is, or whether I'll need to compose them with some unfolding lemma or something to get it to typecheck—technically a separate issue, but mentioning it just in case that impacts the discussion at this stage.)

[Thomas Murrills]

(Also, I wonder if down the line it would be better to give the defs Monotone, StrictMono, MonoOn, etc. the attribute @[mono]—I could make it so that defs tagged @[mono] are handled differently than theorems (i.e. are unfolded by mono at the right stage). The mathlib3 handling seems a little ad hoc. But again, technically a separate discussion, and likely a post-port one at that...)

[Jannis Limperg]

dsimp to unfold stuff is fine but you should use the neutralConfig to make sure that it doesn't do anything else. See also docs4#Lean.Meta.unfold. If you use dsimp, the output is always defeq to the input, so proofs of a dsimped type should also work for the non-dsimped type.

UsedSimps collects the theorems which were used by a particular simp/dsimp call. You can pass one to simp in case you want to call simp multiple times and combine the UsedTheorems. In your case, use {}.

SimpTheorems is the collection of theorems which simp/dsimp uses; by default, these are the theorems tagged with @[simp].

[Thomas Murrills]

Ah, that explains everything very well! Thanks so much! :)