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
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
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
Eric Wieser (Jan 18 2021 at 18:56):
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
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
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
Johan Commelin (Jan 20 2021 at 06:24):
@Eric Wieser should we just define
@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
right_inverse anyway? Why not merge them into
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
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
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: Aug 03 2023 at 10:10 UTC