Function.Involutive best practices

Stream: mathlib4

[Martin Dvořák]

Imagine we have something like the following declarations in Mathlib:

@[simp] lemma foo_foo (x) : x.foo.foo = x :=
  sorry

lemma foo_involutive : foo.Involutive :=
  foo_foo

lemma foo_bijective : foo.Bijective :=
  foo_involutive.bijective

lemma foo_injective : foo.Injective :=
  foo_bijective.injective

lemma foo_surjective : foo.Surjective :=
  foo_bijective.surjective

• Do we want to keep both foo_foo and foo_involutive in the API? Or only one of them?
• Do we want to keep foo_injective in the API, even though it can be obtained from foo_bijective definitionally?
• Do we want to keep foo_surjective in the API, even though it can be obtained from foo_bijective definitionally?

Depending on the answers, I might be more questions.

[Ruben Van de Velde]

I think yes, keep all of them for convenience

[Martin Dvořák]

/poll Assuming we keep all of them, in which order should the lemmas after foo_involutive come?
Bijective first; Injective and Surjective proved from Bijective
Bijective, Injective, Surjective, (in this order) all proved directly from Involutive
Injective, Surjective, Bijective (in this order) all proved directly from Involutive
Injective and Surjective first (proved from Involutive), Bijective last (proved from Injective and Surjective)

[Eric Wieser]

Having both foo_foo and foo_involutive (or foo_foo and foo_bijective when Involutive is ill-typed such as for docs#Equiv.symm) is certainly useful, the other three lemmas are nice for convenience but not so big a deal that I'd push either for their inclusion or removal.

[Damiano Testa]

Does this happen often enough that it should be kept in sync and hence automated?

[Martin Dvořák]

Eric Wieser said:

Having both foo_foo and foo_involutive (or foo_foo and foo_bijective when Injective is ill-typed) is certainly useful, the other three lemmas are nice for convenience but not so big a deal that I'd push either for their inclusion or removal.

I see a bit of a difference between including bijective on top of involutive and including injective and surjective on top of the rest. I see the former as useful because not everybody knows that involutive implies bijective and/or the name of the relevant lemma. The latter looks more like an unnecessary boilerplate because everybody knows they can take injective and surjective directly from the definition.

[Martin Dvořák]

Damiano Testa said:

Does this happen often enough that it should be kept in sync and hence automated?

I don't know. If they should be all included for every Involutive function, there will be quite a few of them I guess!