which tactics change behavior based on the environment?

Stream: general

[Jason Rute]

Lean is sort of unique (at least compared to HOL Light which I was most used to before this) in that tactics are not pure functions (in theory or in practice). Their behavior can change radically based on the environment. The example I'm most aware of is the simp tactic which will automatically apply any theorem labeled with the [simp] attribute. refl, symmetry, and transitivity also have similar attributes.

This means that the lean code

lemma foo : bar → baz := by simp

Might work in one part of the code but not another (even if bar and bar are both in the environment). It sort of makes it tricky when thinking about AI to say, which tactics should I apply, because whether the simp tactic is applicable depends not only on the definitions of bar and baz and the theorems proved along the way, but on other things such as which lemmas are tagged with the [simp] attribute.

Here are my questions:

1. Are there other interactive tactics like this besides these 4? (I'm only interested in tactics which can be found in PRed proofs. Tactics like library_search which aren't used in final proofs aren't important for my interests.)
2. Is there a list of such tactics?
3. Are attributes the only mechanism which causes non-pure behavior or are there others?
4. I think for simp this behavior matters a lot in practice, but how about refl, symmetry and transitivity? Is it common to label a lemma with [refl], [symm], [trans] well after the corresponding relation is defined? (Any definitions or automatic lemmas getting marked with say, [refl], is for my purposes pure behavior and that doesn't concern me.)

[Jesse Michael Han]

tidy will attempt to use any tactic that's been marked by the [tidy] attribute, e.g.

-- uncomment in case of emergency
-- @[tidy] meta def big_bertha : tactic unit := `[finish]

[Jason Rute]

(Also, before I start a flame war, if I'm not using the term "pure" correctly as it relates to functional programming, I hope you will forgive me and look past that to the main essence of my question.)

[Jesse Michael Han]

to avoid the complexity of modelling the dynamics of the environment, you could restrict yourself to simp only [...] and, like DeepHOL, supply lemmas ranked by a separate premise selection head

[Jason Rute]

Yes, I'm thinking about that for simp. I'm curious however if simp is the odd case, or if this is a pervasive behavior in Lean tactics. (For example, I don't even know if there is a form of refl which doesn't use the [refl] lemmas except the definitional ones. But I also don't know if it really matters much in practice.)

[Yury G. Kudryashov]

ext applies the best available extensionality lemma.

[Yury G. Kudryashov]

to_additive attribute depends on all dependencies having this attribute.

[Yury G. Kudryashov]

I mean, all dependencies that should be adjusted from * to +.

[Scott Morrison]

Many tactics depend on the reducibility attributes on declarations, which can be changed after the point of definition.