Stream: math-comp users

Topic: surjective functions


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Feb 07 2022 at 10:32):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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