Lean 4 analogue of semireducible for TransparencyMode?

Stream: lean4

[Thomas Murrills]

Some tactics expect a TransparencyMode argument, but while Lean 3 used semireducible and reducible as possible values, semireducible doesn't seem to be an option verbatim anymore; instead

inductive TransparencyMode where
  | all | default | reducible | instances
  deriving Inhabited, BEq, Repr

Which of these ought to be used in place of semireducible for a tactic with a ! variant?

I found some documenation for TransparencyMode on page 26 of the metaprogramming book, but I'm still not sure which of these corresponds to semireducibility (if any)—or if things have been totally reworked somehow. Is it default, since as I understand it semireducible was the default in Lean 3?

[Gabriel Ebner]

It's default, yes.

[Thomas Murrills]

Great, thanks!

[Notification Bot]

Thomas Murrills has marked this topic as resolved.

[Notification Bot]

Thomas Murrills has marked this topic as unresolved.

[Thomas Murrills]

So, just to be sure the behavior is the same—the convention is that ! variants use the default transparency mode, while ones without ! use the reducibletransparency mode, right? (Just double checking since based on the names I'd expect it to be flipped)

[Scott Morrison]

Yes, that's the convention. The idea is that ! is telling the tactic to work harder (i.e. by being more willing to unfold definitions).

[Mario Carneiro]

It would be nice to resolve that convention with lean 4 core; Leo pointed out that this could be confusing given that lean 4 declarations ending in ! usually means they panic under some conditions

[Gabriel Ebner]

Speaking of syntax, it would also be great if we could use syntax "contrapose" "!"? (or whatever we end up using instead of bang).

[Mario Carneiro]

Personally I think it's fine to just have this secondary meaning, although it's muddier in the case of macros, which also use ! with incompatible meaning, sometimes to indicate that they are macros (this convention is dying out but still exists in the s!/f!/m! macros), but since they look like terms they might use the term meaning (who's to say what the ! in panic! "" means?) or since they are like tactics they might use the tactic meaning (no macros like that exist right now, but I can imagine some mathlib tactics having term forms that inherit the tactic syntax)

[Mario Carneiro]

I think we could implement something like syntax "contrapose" afterIdent("!")? where afterIdent splits the previous ident token if it consumed the specified string

[Thomas Murrills]

is there a tactic naming convention for specifying the use of other transparency modes? e.g. appending something like !! or !a to indicate all or !i for instances? or do we typically not implement these in tactics for some reason? (I don’t have any usage experience, so I don’t know if this is a reasonable question in practice!)

[Mario Carneiro]

Some tactics that have this kind of option allow a config argument which will have a field for the reducibility setting. They are not used enough for the sigil soup to be worth the readability cost

[Mario Carneiro]

It occurs to me that erw should maybe be renamed to rw! to follow this naming convention (it is the reducibility := .default version of rw)

[Johan Commelin]

Knuth would probably write rw$ and contrapose$ to hint that they are doing "more expensive" stuff.