Ricardo (Feb 22 2023 at 21:34): 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?
Ricardo (Feb 22 2023 at 21:35):Maybe I should ask this in #Coq users since it's only tangentially related to mathcomp.
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).
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?
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).
Paolo Giarrusso (Feb 23 2023 at 00:31):but that's new with 8.17
Paolo Giarrusso (Feb 23 2023 at 00:32):(to be released "very soon")
Ricardo (Feb 23 2023 at 00:36):Wow! That's great! :partying_face:
Ricardo (Feb 23 2023 at 00:36):Thank you @Paolo Giarrusso
Ricardo (Feb 23 2023 at 00:36):In the meantime I'm using \c.
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?
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.
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
Paolo Giarrusso (Feb 23 2023 at 00:43):canonical structures are what math-comp uses to overload things like + on different groups/rings/...
Ricardo (Feb 23 2023 at 00:44):How would you use canonical structures to overload this notation?
Ricardo (Feb 23 2023 at 00:45):You would define a third datatype that you convert to using canonical structures?
Paolo Giarrusso (Feb 23 2023 at 00:45):I'd wait for an expert to answer your question :sweat_smile:
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:
Ricardo (Feb 23 2023 at 00:46):No worries. Thank you for all the help so far :smile:
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).
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.
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.
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?
Ricardo (Feb 25 2023 at 06:46):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: Oct 13 2024 at 01:02 UTC