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.

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.

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.

Cyril Cohen (Feb 07 2022 at 10:32):

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

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
what do you think about this?

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: Oct 13 2024 at 01:02 UTC