Naming of `right_inverse` lemmas

Stream: general

[Eric Wieser]

We seem to have a fairly established convention that lemmas with statement injective foo should be called foo_injective.

However, we seem to have little precedent for how to name lemmas with statement right_inverse foo_inv foo.

This came up in this PR, where the question was what to name this lemma:

lemma nat_cast_right_inverse [fact (0 < n)] :
  function.right_inverse val (coe : ℕ → zmod n) :=

The confusion comes when considering whether the lemma is saying "there is a right inverse of "nat_cast" and it is this" (which matches the name I use there), or "val is a right inverse of something" (which would suggest the lemma should be val_right_inverse)

Something to consider when choosing the name is how the projection the_name.surjective : function.surjective (coe : ℕ → zmod n) reads.

[Johan Commelin]

nat_cast is a left inverse, and therefore surjective. Do we have left_inverse.surjective?

[Eric Wieser]

No, we have docs#function.left_inverse.injective and docs#function.right_inverse.surjective

[Eric Wieser]

We also have docs#function.left_inverse.right_inverse and docs#function.right_inverse.left_inverse since the two are defeq with an argument swap, which suggests to me that the intended use case was for the argument of interest to be in the second position

[Eric Wieser]

So if the declaration we provided was instead function.left_inverse (coe : ℕ → zmod n) val, the spelling would be nat_cast_left_inverse.right_inverse.surjective which reads "the right inverse of the thing that is left-inverse to nat_cast is surjective"

[Chris Hughes]

I think the existence of right_inverse as a definition is kind of strange, and I would just prove val_coe, or coe_val (I don't remember which way round it is).

[Eric Wieser]

The motivation for using right_inverse is that you get useful projections like .surjective

[Johan Commelin]

@Eric Wieser should we just define left_inverse.surjective and right_inverse.injective?

@others if you have good suggestions about the convention here, please chime in

[Eric Wieser]

My feeling is no, since at that point we'd have a >/<-type situation where the two are indistinguishable and we need to declare one simp-normal.

If we decide the convention is backwards though, we could switch those members between left and right.

[Anne Baanen]

Why do we have both left_inverse and right_inverse anyway? Why not merge them into one_sided_inverse?

[Eric Wieser]

Which side would be the "one" side?

[Anne Baanen]

Preferably in the same order as they appear, so one_sided_inverse f g means f \circ g = id.

[Eric Wieser]

I think that's the current left_inverse then

[Eric Wieser]

Note that if we did that rename then docs#has_left_inverse would no longer have a matching name

[Eric Wieser]

Johan Commelin said:

Eric Wieser should we just define left_inverse.surjective and right_inverse.injective?

The names left_inverse.inv_surjective and right_inverse.inv_injective would be fine I think, to make it clear what the (in|sur)jectivity refers too - although I don't know if the extra API is needed

[Eric Wieser]

As an alternative approach here - we already have docs#embedding to bundle a function with a proof of its injectivity - could we have two more bundled function types for function-with-right-inverse and function-with-left-inverse? The API could be roughly

structure left_invertible :=
(to_fun : A → B)
(inv_fun: B → A)
(left_inverse: left_inverse inv_fun to_fun)

structure right_invertible :=
(to_fun : A → B)
(inv_fun: B → A)
(left_inverse: left_inverse inv_fun to_fun)

def left_invertible.symm (f : left_invertible A B) : right_invertible B A := sorry
def right_invertible.symm (f : right_invertible A B) : left_invertible B A := sorry

instance : has_coe (left_invertible A B) (embedding A B) := sorry

-- a pile of simp lemmas like those for equiv

-- no need for any fields any more
structure equiv extends left_invertible, right_invertible

Can anyone think of better names than left_invertible and right_invertible? injection and surjection? Distinguishing the bundle with a computable inverse left_invertible from the bundled with a non-computable inverse embedding by name along seems difficult.

[Eric Wieser]

I made a PR at #5829 with the above

[Bryan Gin-ge Chen]

#5797 is stuck on this naming issue, right? Does anyone have any concrete suggestions for a way forward?

[Eric Wieser]

Yes, I think that PR is stuck on this thread - although perhaps I could just insert a todo comment referencing a github issue / add clear docstrings resolving name ambiguities to unstick it.

[Eric Wieser]

#6167 adds some new definitions taking left_inverse arguments. It would be great to unblock the naming problem so that we actually have those arguments to pass.

[Anne Baanen]

Since this has gone on for a while without resolution, I think you should do whatever you feel is best and when someone later has a good idea to fix it, they can go ahead and implement it. (That person might turn out to be me, but no promises.)

[Eric Wieser]

Most of the content of #5797 got merged in another PR - it's now just creating aliases of lemmas with defeq-but-different types for the sake of projection notation

[Eric Wieser]

But I would probably lean to just merging it and sorting out renames later - the statement ought to be clear from its type, and the name should be enough to at least find it