## Stream: math-comp users

### Topic: surjective functions

#### Evgeniy Moiseenko (Feb 02 2022 at 11:16):

I wonder, why math-comp has some theory devoted to injective and bijective functions but does not even have a definition of surjective functions? Is that intentional? Is the naive definition of surjectivity is hard to work with in coq?
Is there some alternative in math-comp, that should be used instead?

#### Reynald Affeldt (Feb 02 2022 at 12:04):

We found a use for a definition of surjective function in mathcomp-analysis where we did introduce it but that part of the library is under refactoring.

#### Evgeniy Moiseenko (Feb 02 2022 at 12:13):

Reynald Affeldt said:

We found a use for a definition of surjective function in mathcomp-analysis where we did introduce it but that part of the library is under refactoring.

Well, I had in mind an even simpler thing (no `sets` / propositional predicates involved):

``````Definition surjective f :=
forall (x : rT), exists y, f y = x.
``````

But I was afraid it's some known anti-pattern.

#### Evgeniy Moiseenko (Feb 02 2022 at 12:17):

BTW, I've just proven the expected lemmas:

``````Lemma bij_surj {rT aT : Type} (f : aT -> rT) :
bijective f -> surjective f.

Lemma inj_surj_bij {rT : eqType} {aT : choiceType} (f : aT -> rT) :
injective f -> surjective f -> bijective f.
``````

#### Christian Doczkal (Feb 07 2022 at 08:40):

I have noticed this also from time to time and I'm happy with your definition - although I would favor the alpha-equivalent `forall y : rT, exists x,...`

Maybe it would also be nice to provide a preimage operator:

``````preim_of {aT : choiceType} {rT : eqType}  : surjecive f -> forall y:rT, { x : aT | f x = y}
``````

Presumably, this is already part of the proof of `inj_surj_bij`. In addition, it might be nice to also provide a simply-typed version that takes a default argument:

``````sinv : {aT : choiceType} {rT : eqType} (x:aT) (f : aT -> rT) : rT -> aT
sinvK : {aT : choiceType} {rT : eqType} f y x0 : surjective f -> cancel f (sinv x0 f)
``````

#### Evgeniy Moiseenko (Feb 07 2022 at 09:14):

Christian Doczkal said:

I have noticed this also from time to time and I'm happy with your definition - although I would favor the alpha-equivalent `forall y : rT, exists x,...`

Maybe it would also be nice to provide a preimage operator:

``````preim_of {aT : choiceType} {rT : eqType}  : surjecive f -> forall y:rT, { x : aT | f x = y}
``````

Presumably, this is already part of the proof of `inj_surj_bij`. In addition, it might be nice to also provide a simply-typed version that takes a default argument:

``````sinv : {aT : choiceType} {rT : eqType} (x:aT) (f : aT -> rT) : rT -> aT
sinvK : {aT : choiceType} {rT : eqType} f y x0 : surjective f -> cancel f (sinv x0 f)
``````

Yeap, `preim_of` is actually a part of the proof of `inj_surj_bij`.
Thank you for the very nice ideas regarding `sinv`, I would incorporate them in my code if you don't mind :)

Do you think is it worth doing a proposal/PR to mathcomp?

#### Cyril Cohen (Feb 07 2022 at 10:28):

FTR math-comp/analysis#492 has an extensive theory of (in|sur|bi)jections on its way.

#### Cyril Cohen (Feb 07 2022 at 10:31):

I believe it only relies on classical logic in the builders, and that it could be partially backported to mathcomp.

#### Evgeniy Moiseenko (Feb 07 2022 at 12:27):

Hi @Cyril Cohen.
I have just one little concern with respect to the definition of surjectivity from mathcomp-analysis.
The problem is that `set_inj` is defined as `{in A &, injective f}`, i.e. simple "restriction" of injectivity predicate to a set.
But `set_surj := B <= f @ A` is based inherently on propositional sets from mathcomp-analysis.
I guess, for uniformity, it would be nice to have `surjective` definition which involves no sets, and then derive `set_surj` using some combinators like `in`, `on`, etc, similarly as how `set_inj` is defined?

Also, I am afraid it would not be possible to port the above definition of `set_surj` straightforwardly to mathcomp, because I believe `<=` and `@` exploit the excluded middle informative axiom. For example, `<=` is derived from the `order` instance for `set A`.
But because `order` theory in mathcomp is defined only for decidable relations, it works only due to LEM.

#### Cyril Cohen (Feb 07 2022 at 12:35):

No, it is ` `<=` ` which is a simple implication and `@` hides an existential.
`set_surj A B f` unfolds exactly to `forall y, B y -> exists2 x, A x & f x = y`

#### Cyril Cohen (Feb 07 2022 at 12:39):

note that no existing combinator can provide the restriction that `{in A &, injective f}` provides, since you would need to alter both the domain for `y` (which is doable with `in`) and `x`, for which there is not combinator so far, which is what pushed us to the use of a predicate that bears both a domain and a codomain

#### Cyril Cohen (Feb 07 2022 at 12:40):

In principle, most of the theory and/or builders from `functions.v` in MCA should be valid, sometimes with specializations to boolean predicates, and types to `eqType` and/or `choiceType`, depending.

#### Evgeniy Moiseenko (Feb 07 2022 at 12:42):

Cyril Cohen said:

No, it is ` `<=` ` which is a simple implication and `@` hides an existential.
`set_surj A B f` unfolds exactly to `forall y, B y -> exists2 x, A x & f x = y`

Oh, you are right, I am sorry.
I thought `<=` is derived from `porderType` instance.

#### Evgeniy Moiseenko (Feb 07 2022 at 12:50):

Cyril Cohen said:

note that no existing combinator can provide the restriction that `{in A &, injective f}` provides, since you would need to alter both the domain for `y` (which is doable with `in`) and `x`, for which there is not combinator so far, which is what pushed us to the use of a predicate that bears both a domain and a codomain

But then what would you prefer?

• definition of `set_surj A B` with restriction for both domain and codomain, and then derived definition of `surjective` with `A = B := predT`;
• definition of `set_surj B` with the restriction only for domain and the restriction of codomain derivable with the help of `in`;
• definition of `surjective` with no restrictions, and then a new combinator that would make it possible to also restrict the domain?

#### Cyril Cohen (Feb 07 2022 at 13:01):

I thought `<=` is derived from porderType instance.

You are right `<=` is, but ` `<=` ` is not, and the latter is the one at use in `set_surj`

#### Cyril Cohen (Feb 07 2022 at 13:06):

I do not know yet what I prefer, in my experience with `functions.v` it brings almost no benefit to go half way `set_surj A` would make little sense without the additional restriction on the codomain. So it leaves out the two others... Having a new combinator would make sense if there are other use cases, which I do not have in mind...

#### Christian Doczkal (Feb 08 2022 at 10:05):

It is my understanding that the most natural way would be option three. Note that there is already a special notation for `bijective`. Despite appearances `{on [pred y in codom f], bijective f}` in `bij_on_codom` makes no reference to `bijective`. Although I can't say that I'm a big fan of this particular notation.

#### Evgeniy Moiseenko (Feb 08 2022 at 15:40):

Christian Doczkal said:

It is my understanding that the most natural way would be option three. Note that there is already a special notation for `bijective`. Despite appearances `{on [pred y in codom f], bijective f}` in `bij_on_codom` makes no reference to `bijective`. Although I can't say that I'm a big fan of this particular notation.

I like option 3 too.
BTW, I didn't know that `{in P, bijective}` and `{on P, bijective}` are hardcoded ...
I thought there is some magic trick under the hood.

I have an idea about how a new combinator might look like.
I'll prepare MWE and post it here during the week.

#### Evgeniy Moiseenko (Feb 10 2022 at 12:21):

So let me share my thoughts.
The idea is to restrict a function to a proper subtype so that existential quantification in the definition of `set_surj` also quantifies over the proof of membership to the subtype.

First, let's define the restriction of function:

``````Section RstDef.
Context {T U : Type} {P : pred T} {S : subType P}.
Implicit Types  (f : T -> U).

Definition rst f : S -> U := f \o val.

End RstDef.
``````

A couple of fancy notations:

``````Notation "[ 'rst' f 'to' S ]" := (rst f : S -> _)
(at level 0, f at level 99,
format "[ 'rst'  f  'to'  S ]") : form_scope.

Notation "[ 'rst' f | P ]" := (rst f : (sig P) -> _)
(at level 0, f at level 99,
format "[ 'rst'  f  |  P ]") : form_scope.
``````

Then goes the definition of surjectivity:

``````Section Surjective.
Context {rT aT : Type}.
Implicit Types (f : aT -> rT).

Definition surjective f :=
forall (x : rT), exists y, f y = x.

End Surjective.
``````

A small lemma to make sure we are doing right thing:

``````Lemma surj_subE rP aP f :
{in rP, surjective [rst f | aP]} <-> (forall y, rP y -> exists2 x, aP x & f x = y).
``````

It can be proven with the help of a more general lemma:

``````Lemma rst_existsE f (PU : U -> Prop) :
(exists x, PU ([rst f to S] x)) <-> (exists2 x, P x & PU (f x)).
``````

@Christian Doczkal @Cyril Cohen @Reynald Affeldt

#### Cyril Cohen (Feb 10 2022 at 17:32):

Looks ok, it's difficult for me to assess the impact on the theory without seeing it though.
Note that your `rst` function is a generalization of `sigL` from functions.v

#### Cyril Cohen (Feb 10 2022 at 17:34):

And while I am not fond of the name `rst` I totally agree with the usefulness of such a function, which must come with its own theory (hence the corresponding `valL` from mathcomp/analysis, which is its partial inverse)

#### Evgeniy Moiseenko (Feb 11 2022 at 19:48):

Cyril Cohen said:

Looks ok, it's difficult for me to assess the impact on the theory without seeing it though.
Note that your `rst` function is a generalization of `sigL` from functions.v

The naming convention is up to a debate for sure.
BTW, what does `sigL` stands for?

#### Evgeniy Moiseenko (Feb 11 2022 at 19:50):

Cyril Cohen said:

And while I am not fond of the name `rst` I totally agree with the usefulness of such a function, which must come with its own theory (hence the corresponding `valL` from mathcomp/analysis, which is its partial inverse)

Would you prefer to wait until https://github.com/math-comp/analysis/pull/492 is merged?
After that, we can try to backport it partly to mathcomp, incorporating some of the ideas discussed here.
I would be happy to help, since I also need this theory in my project.

#### Alexander Gryzlov (Jan 19 2023 at 20:03):

Looks like the theory now exists in `mathcomp-classical`, are there still any plans to backport it to core mathcomp?

#### Evgeniy Moiseenko (Jan 30 2023 at 14:26):

BTW, the alternative formulation that was proposed by @Christian Doczkal can be found in my project here

I haven't much time to work on this project recently. But if there is an interest in the community, I can try to also prepare a PR.

Last updated: Feb 08 2023 at 04:04 UTC