Zulip Chat Archive

Stream: general

Topic: Naming of `right_inverse` lemmas

Eric Wieser (Jan 18 2021 at 17:45):

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 (Jan 18 2021 at 18:25):

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

Eric Wieser (Jan 18 2021 at 18:56):

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

Eric Wieser (Jan 18 2021 at 18:57):

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 (Jan 18 2021 at 18:59):

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 (Jan 19 2021 at 07:12):

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 (Jan 19 2021 at 08:42):

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

Johan Commelin (Jan 20 2021 at 06:24):

@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 (Jan 20 2021 at 08:55):

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 (Jan 20 2021 at 09:43):

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

Eric Wieser (Jan 20 2021 at 09:49):

Which side would be the "one" side?

Anne Baanen (Jan 20 2021 at 09:52):

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

Eric Wieser (Jan 20 2021 at 09:56):

I think that's the current left_inverse then

Eric Wieser (Jan 20 2021 at 09:58):

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

Eric Wieser (Jan 21 2021 at 10:45):

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 (Jan 21 2021 at 10:51):

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 (Jan 21 2021 at 14:52):

I made a PR at #5829 with the above

Bryan Gin-ge Chen (Feb 06 2021 at 22:13):

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

Eric Wieser (Feb 07 2021 at 01:44):

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 (Feb 16 2021 at 23:14):

#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 (Feb 22 2021 at 18:41):

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 (Feb 22 2021 at 18:43):

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 (Feb 22 2021 at 18:45):

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

Last updated: Dec 20 2023 at 11:08 UTC