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?

see `the_inv_into`

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...

`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...

`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).

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

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

).

You mean in the case the function is not surjetive?

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`

).

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".

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.

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...

For instance, if $f(x) = x^2$, then `the_inv_into UNIV f 0 = 0`

. For anything other than 0, it's unspecified.

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.

I don't think there is any reason to ever use `the_inv_into`

over `inv_into`

.

`inv_into`

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

Oh great then I was looking for `inv_into`

I guess!

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?

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!

I guess surjectivity is generally an unnecessarily strong assumption.

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: Sep 25 2021 at 09:17 UTC