Stream: Beginner Questions

Topic: Inverse of bijective function

Nicolò Cavalleri (Jun 23 2021 at 23:32):

Suppose I have a lemma proving that a given function is bijective. How do I define the inverse function? In my real life problem I actually have a function f which satisfies bij_betw f UNIV (S :: 'b set) and I need to build a function 'b => 'a such that it is the inverse if f on S. Can I do this?

Jakub Kądziołka (Jun 23 2021 at 23:34):

see the_inv_into

Nicolò Cavalleri (Jun 24 2021 at 12:13):

Thank you! I am puzzled though: how does that definition work? If f is not surjective the inverse is not unique, and f is never assumed surjective, so how does THE work? My guess is that it uses some very powerful axiom of choice...

Jakub Kądziołka (Jun 24 2021 at 12:50):

THE is a variation on Hilbert's epsilon operator, which is present in Isabelle as SOME. SOME indeed corresponds to the axiom of choice, and is defined as follows: if EX x. P x, then SOME returns some x that has the property, otherwise an arbitrary x from your type. THE additionally requires that there is exactly one x st. P x, which, means the happy case doesn't require AC, as it corresponds to a function {x} \mapsto x, which should be constructible in ZF? Though, the case where ALL x. P x = False corresponds to undefined :: 'a, and I'm not sure whether that's AC or not...

Manuel Eberl (Jun 24 2021 at 19:02):

THE is the unique choice operator, and its existence is actually "weaker" than that of the existence of the SOME operator (non-unique choice). But I'll leave the precise explanation of what that means to people who actually know something about logic (in contrast to me).

Nicolò Cavalleri (Jun 24 2021 at 19:03):

Bu my point is precisely that if the function is not surjective the inverse is not unique! In fact I was very surprised to see a THE there

Manuel Eberl (Jun 24 2021 at 19:06):

In that case you just get some unspecified value that you can prove nothing about (cf. undefined).

Nicolò Cavalleri (Jun 24 2021 at 19:06):

You mean in the case the function is not surjetive?

Manuel Eberl (Jun 24 2021 at 19:07):

HOL cannot prevent you from writing down "nonsense". There are a number of terms that are "nonsensical" in some sense, e.g. 1 / 0. Some of them have some halfway sensible dummy values like 1 / 0 = 0, others are just unspecified (e.g. ln (-1 :: real) or THE x. False).

Manuel Eberl (Jun 24 2021 at 19:10):

Nicolò Cavalleri said:

You mean in the case the function is not surjetive?

The way the_inv_into is defined, the_inv_into A f y is the unique value x such that x ∈ A and f(x) = y if such a unique value exists; otherwise you get "nonsense".

Manuel Eberl (Jun 24 2021 at 19:11):

If the function is not injective and surjective, there will be some values y where the_inv_into A f y will be "nonsense" (i.e. unspecified). It might still work for other values of y though if the choice is unique.

Nicolò Cavalleri (Jun 24 2021 at 19:11):

But then what if I have an injective function of which I want a right inverse? Isn't there a theory of inverse functions that makes use of SOME? In any case I am puzzled that in lemmas involving the_inv_into you often see the hypothesis that the function be injective but never that it be surjective...

Manuel Eberl (Jun 24 2021 at 19:11):

For instance, if $f(x) = x^2$, then the_inv_into UNIV f 0 = 0. For anything other than 0, it's unspecified.

Manuel Eberl (Jun 24 2021 at 19:12):

Nicolò Cavalleri said:

But then what if I have an injective function of which I want a right inverse? Isn't there a theory of inverse functions that makes use of SOME? In any case I am puzzled that in lemmas involving the_inv_into you often see the hypothesis that the function be injective but never that it be surjective...

Yes, there is inv_into. Frankly I've never used the_inv_into; I didn't even know it existed.

Manuel Eberl (Jun 24 2021 at 19:12):

I don't think there is any reason to ever use the_inv_into over inv_into.

Manuel Eberl (Jun 24 2021 at 19:13):

inv_into also works if the value is not unique, it's enough for the preimage to be nonempty.

Nicolò Cavalleri (Jun 24 2021 at 19:13):

Oh great then I was looking for inv_into I guess!

Manuel Eberl (Jun 24 2021 at 19:13):

Nicolò Cavalleri said:

In any case I am puzzled that in lemmas involving the_inv_into you often see the hypothesis that the function be injective but never that it be surjective...

Do you have any examples?

Nicolò Cavalleri (Jun 24 2021 at 19:13):

Manuel Eberl said:

I don't think there is any reason to ever use the_inv_into over inv_into.

Yep I don't see it either!

Manuel Eberl (Jun 24 2021 at 19:13):

I guess surjectivity is generally an unnecessarily strong assumption.

Manuel Eberl (Jun 24 2021 at 19:14):

It's enough for the specific values you're plugging into the the_inv_into to be in the image of A under f, i.e. in f`A.

Last updated: Dec 21 2024 at 16:20 UTC