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?

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.

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.

Do you mean this one?

https://github.com/math-comp/analysis/blob/73e92bbf3d558ea79ca521407cf2ffc6aa8d0d8e/theories/cardinality.v#L128

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.

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

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

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?

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

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

cf file https://github.com/math-comp/analysis/blob/functions/theories/functions.v

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.

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`

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

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.

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.

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?

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`

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

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.

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.

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

what do you think about this?

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

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)

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?

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.

Looks like the theory now exists in `mathcomp-classical`

, are there still any plans to backport it to core mathcomp?

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