Stream: math-comp users

Topic: Notation for composing functions


view this post on Zulip Ricardo (Feb 22 2023 at 21:34):

I'd like to have something like [ x ; f1 ; ... ; fn ] for fn (... (f1 x) ...)like the alternative postfix notation. I think I know how to write that notation. It would be something like

Notation "[ x ; f1 ; .. ; fn ]" := (fn (.. (f1 x) ..)).

However, it gets trickier, because in the case that f is a finmap {fmap A -> B}, I'd like it to get expanded into [`in_codomf x] so that the return type is codomf f instead of B. Would something like that be at all possible?

view this post on Zulip Ricardo (Feb 22 2023 at 21:35):

Maybe I should ask this in #Coq users since it's only tangentially related to mathcomp.

view this post on Zulip Ricardo (Feb 22 2023 at 22:30):

On a different yet related note, would it be possible to extend the \; notation from ssrfun to finfun? That is,

Definition ffcomp (A B C : finType) (f : {ffun A -> B}) (g : {ffun B -> C})
  : {ffun A -> C} := [ffun x => g (f x)].
Notation "f \; g" := (ffcomp f g)
  (at level 60, right associativity).

view this post on Zulip Ricardo (Feb 22 2023 at 23:54):

Specially annoying is the fact that doing

From mathcomp Require Export -(notations) ssrfun.

to avoid importing the \; and \o notation also bypasses the import of the notation that I'm using to define ffcomp.

Definition ffcomp (f : {ffun A -> B}) (g : {ffun B -> C})
  : {ffun A -> C} := [ffun x => g (f x)].

I get the error Unknown interpretation for notation "[ ffun _ => _ ]". Is it possible to import everything from ssrfun except \; and \o?

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 00:31):

https://coq.github.io/doc/v8.17/refman/changes.html#id13

Added: Enable Notation and Disable Notation commands to enable or disable previously defined notations (#12324 and #16945, by Hugo Herbelin and Pierre Roux, extending previous work by Lionel Rieg, review by Jim Fehrle).

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 00:31):

but that's new with 8.17

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 00:32):

(to be released "very soon")

view this post on Zulip Ricardo (Feb 23 2023 at 00:36):

Wow! That's great! :partying_face:

view this post on Zulip Ricardo (Feb 23 2023 at 00:36):

Thank you @Paolo Giarrusso

view this post on Zulip Ricardo (Feb 23 2023 at 00:36):

In the meantime I'm using \c.

view this post on Zulip Ricardo (Feb 23 2023 at 00:39):

Going back to the original question, do you know if it would be possible to have a notation like [ x ; f1 ; .. ; fn ] that does something different when f is a finmap or a function?

view this post on Zulip Ricardo (Feb 23 2023 at 00:42):

I imagine something like an overloaded function that can take either a function or a finmap and do something different depending on which one is getting. I believe there are no overloaded functions in Coq but there might be some language feature that I'm not aware of that can do something similar in this situation.

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 00:42):

canonical structures and typeclasses are both ways to encode overloading, but type classes don't really work well with math-comp in most cases

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 00:43):

canonical structures are what math-comp uses to overload things like + on different groups/rings/...

view this post on Zulip Ricardo (Feb 23 2023 at 00:44):

How would you use canonical structures to overload this notation?

view this post on Zulip Ricardo (Feb 23 2023 at 00:45):

You would define a third datatype that you convert to using canonical structures?

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 00:45):

I'd wait for an expert to answer your question :sweat_smile:

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 00:46):

sorry but this is much too hard for me — I don't use math-comp remotely enough :sweat_smile: :sweat_smile:

view this post on Zulip Ricardo (Feb 23 2023 at 00:46):

No worries. Thank you for all the help so far :smile:

view this post on Zulip Pierre Roux (Feb 23 2023 at 07:31):

The internals of the use of canonical structures in MathComp are well explained in Part II of the MathComp book (more specifically, chapter 8). Note however that this requires a lot of boilerplate that can be automated with the use of hierarchy builder https://github.com/math-comp/hierarchy-builder (MathComp itself is in the process of being ported to hierarchy builder, an alpha release is already available but some documentation is missing before we actually release it).

view this post on Zulip Ricardo (Feb 23 2023 at 15:25):

@Pierre Roux, could you be a bit more specific? Which of telescopes, packed classes, or phantom parameters do you think would be useful to define this overloaded notation?

Also, are there good guides to HB? Specially useful would be guides that look at it from a programming point of view probably. The project I'm involved in is mostly concerned with a specific representation of a specific type of graphs and working with maps and rewriting rules between them. The goal is to prove that rewriting rules generated in a certain way have a certain property.

view this post on Zulip Ricardo (Feb 25 2023 at 03:59):

I could make the notation work with this code.

From mathcomp Require Import all_ssreflect finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope fset.
Local Open Scope fmap.

Definition ffcomp (A B C : finType) (f : {ffun A -> B}) (g : {ffun B -> C})
  : {ffun A -> C} := [ffun x => g (f x)].
Notation "f \c g" := (ffcomp f g) (at level 60, right associativity).

Record funlike (K V : finType) := { fn : {ffun K -> V} }.
Coercion ffun_to_funlike (K V : finType) (f : {ffun K -> V}) := {| fn := f |}.
Coercion fmap_to_funlike (K V : choiceType) (f : {fmap K -> V}) :=
  {| fn := [ffun k : domf f => [`in_codomf k]] |}.

Definition comp (K V W : finType) (f : funlike K V) (g : funlike V W)
  : funlike K W := {| fn := (fn f) \c (fn g) |}.

Notation "[ x ; f1 ]" := (fn f1 x).
Notation "[ x ; f1 ; .. ; fi ; fj ]" := (fn (comp f1 .. (comp fi fj) ..) x).

However this notation has the issue that if I want to prove [x; f; g; h] = [x; f'; g'; h] and I have an hypothesis H : [x; f; g] = [x; f'; g'] then I can't just do rewrite H and be done with it, as far as I can tell.

view this post on Zulip Ricardo (Feb 25 2023 at 06:29):

This gets better. Changed the notation to

Notation "[ f1 ; .. ; fi ; fj ]" := (fn (comp f1 .. (comp fi fj) ..)).

and have an associativity lemma for ffcomp.

Lemma ffcompA (A B C D : finType)
  (f : {ffun A -> B}) (g : {ffun B -> C}) (h : {ffun C -> D}) :
  (f \c g) \c h = f \c g \c h.
Proof. apply/ffunP => a. by rewrite !ffunE. Qed.

So now what I want to prove is [f1; h1; h2] = [g1; g2; f3] knowing that H1 : [f1; h1] = [g1; f2] and H2 : [f2; h2] = [g2; f3]. I can do that with

  move: H2 H1. rewrite /= ffcompA => <-.
  rewrite -ffcompA => ->. by rewrite ffcompA.

Is there a direct way in ssreflect to simplify a term before using it for rewrite? Or is there a function that, when applied to a hypothesis, gives the simplified version of the hypothesis?

view this post on Zulip Ricardo (Feb 25 2023 at 06:46):

I imagine something like

by rewrite ffcompA -(simplP H2) -ffcompA (simplP H1) ffcompA.

view this post on Zulip Ricardo (Feb 25 2023 at 07:19):

This is the best I've been able to do so far.

move: H1 H2 => /= H1 H2.
by rewrite ffcompA -H2 -ffcompA H1 ffcompA.

Last updated: Jul 15 2024 at 20:02 UTC