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?

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

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

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`

?

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

but that's new with 8.17

(to be released "very soon")

Wow! That's great! :partying_face:

Thank you @Paolo Giarrusso

In the meantime I'm using `\c`

.

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?

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.

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

canonical structures are what math-comp uses to overload things like `+`

on different groups/rings/...

How would you use canonical structures to overload this notation?

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

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

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

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

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

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

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.

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?

I imagine something like

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

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