Hi everyone. Hope you're all well. I'm wondering if there's a simple way to have two `fmap`

s from mathcomp.finmap sharing their domain, that is, `f : {fmap K -> V1}`

and `g : {fmap K -> V2}`

with `domf f = domf g`

. In particular, I'd like that whenever I have an `x : domf f`

then `g x`

type checks. Would that be possible?

I mean sharing their domain in a way that the type checker acknowledges it.

```
From mathcomp Require Import all_ssreflect finmap.
Variables (K V1 V2 : choiceType).
Variables (f : {fmap K -> V1}) (g : {fmap K -> V2}).
Hypothesis (H : domf f = domf g).
Variable (x : domf f).
Check (g x).
```

Maybe you could use option type if you have two maps

```
Variable x1 : K.
Check (f.[? x1])%fmap.
Check (g.[? x1])%fmap.
```

```
```

Yes, that's what I'm doing, but it's getting quickly out of hand.

```
From mathcomp Require Import all_ssreflect finmap.
Local Open Scope fset.
Local Open Scope fmap.
Section NS.
Variables (N S : choiceType).
Record cg : Type :=
CG { siteMap : {fmap S -> N}
; edges : rel S
; edges_sym : symmetric edges
}.
Section CG.
Variable (g : cg).
Definition nodes : {fset N} := codomf (siteMap g).
Definition sites : {fset S} := domf (siteMap g).
End CG.
Record hom : Type :=
Hom { f_nodes : {fmap N -> N}
; f_sites : {fmap S -> S}
; dom : cg N S
; cod : cg N S
; f_nodes_total :
[forall n : nodes dom, exists m : nodes cod,
f_nodes.[? val n] == Some (val m)]
; f_sites_total :
[forall s : sites dom, exists t : sites cod,
f_sites.[? val s] == Some (val t)]
; comm :
[forall s : sites dom,
f_nodes.[? siteMap dom s] ==
obind (fun s' => (siteMap cod).[? s'])
f_sites.[? val s]]
; edge_pres :
[forall s : sites dom, forall t : sites dom,
edges dom (val s) (val t) ==
if (f_sites.[? val s]) is Some s'
then if (f_sites.[? val t]) is Some t'
then edges cod s' t'
else false
else false]
}.
```

In particular, in `edge_pres`

we know that the else branches will never be taken as a consequence of `f_sites_total`

.

That example could be a bit better with the option monad, but your original request makes more sense. If the common domain is finite type D := { k : K | P k }, then one could use two total maps with domain D — that is, f : D -> V1 and g : D -> V2.

Does math-comp have a better abstraction for *total* maps with finite domain? Funext lets one prove decidable equality on such functions

(above, P : pred K is arbitrary)

(Importantly, the decidable equality computes without getting stuck on funext, and makes their equality proof-irrelevant)

OTOH, there isn't a general way to turn a *propositional* equality Heq : domf f = domf g into a *definitional* one. There are only more or less reasonable syntaxes to use Heq in casts (like EqNotations), but that's going to be a pain

I am not sure what the problem is. Is it because the definition becomes too lengthy?

In that case you could write

```
[forall s : sites dom, forall t : sites dom,
edges dom (val s) (val t) ==
if (f_sites.[? val s], f_sites.[? val t]) is (Some s', Some t')
then edges cod s' t' else false]
```

or you have in mind another formulation, but maybe you could derive it afterward from your initial definition?

```
```

FWIW, usually it's not just definition size: partial lookups usually require a bit of noise in lemmas and proofs, since you must often add hypotheses about it, and prove that your lookups succeed after all. Ltac automation can reduce the boilerplate, but not in ways that are idiomatic in math-comp...

I've basically never seen this overhead go beyond a constant factor or become a showstopper; but total maps could be an improvement.

@Ricardo or just store { fmap K -> (V1, V2) } and *derive* f and g?

@Paolo Giarrusso, that's an interesting suggestion but it mushes together two separate mathematical notions, that of site graphs and their homomorphisms. Site graphs are basically a total function from a set of sites S to a set of nodes N and a symmetric relation on S. Then site graph homomorphisms are a total function between the sites of the two graphs and a total function between the nodes.

That's not necessarily a bad idea: it just means the implementation differs from the interface.

maybe mathematicians would talk about a representation (or not)

Actually, "encoding" might be better: I'd claim this is less bad than many standard set-theoretic encodings (say, of naturals). In both cases, most of your theory will probably mostly talk about the correct interface, not about the encoding details

@Laurent Théry I like the conciseness of your suggestion and I'll adopt it for the time being but I agree with @Paolo Giarrusso that this isn't just about definition size. Handling the impossible None case everytime makes the code less clear and is a waste of energy and time.

@Paolo Giarrusso I'd say the standard set-theoretic encodings aren't a high (or good) bar.

Agreed.

But to be clear, which are the functions with the same domain? Is this about f_nodes and f_sites, or about dom and cod?

If it's about f_nodes/f_sites, I agree I'd prefer `f_sites : nodes dom -> nodes cod`

or the like.

This diagram hopefully helps. For a homomorphism `f : g -> g'`

```
siteMap g
S ---------> N
| f_sites | f_nodes
v v
S' ---------> N'
siteMap g'
```

`comm`

ensures that this diagram commutes.

Paolo Giarrusso said:

If it's about f_nodes/f_sites, I agree I'd prefer

`f_sites : nodes dom -> nodes cod`

or the like.

I tried something similar before

```
Record cg : Type :=
CG { siteMap : {fmap S -> N}
; edges : rel (domf siteMap)
; edges_sym : symmetric edges
}.
```

and it was so painful I gave up with this approach. Do you think it would be different here?

Hm... What was the pain? If it's related to the mismatch between S and domf siteMap, I suspect you might want to avoid partial functions fmap altogether. Your on-paper math claims siteMap is a total function, after all

*but* I don't know that K -> V has the appropriate theory in math-comp, so you might have to build some.

(reminder I'm not actually a math-comp expert)

Basically, IIUC, *all* your functions are actually total, and your diagram only has 4 distinct types

But each time you bind an fmap over S, you're (morally) quantifying over some fresh unknown subset S' of S; and stating `Heq : S' = S''`

won't help the typechecker. Mentioning the same set S in both places seems the only way.

Yes, that's true. You're right that they are all total functions in the math. However, building graphs computationally will be easier stepwise I think. I have the feeling that fmap will make that possible. Also, I have the vague intuition that constructing total functions between fsets will be hard.

I don't remember quite clearly in this moment what the pain was, but I know some of it is documented in this very stream #math-comp users

I think it was related to adding a site to a graph. Since `domf siteMap`

changed, then `edges : rel (domf siteMap)`

wasn't a valid edge relation on the graph anymore and constructing a valid one from the old one was hard for me at the time. I've learned much more about mathcomp.finmap since then but I have the feeling it would still be hard.

Ah, that's not surprising, and it's a general tradeoff, usually described as "dependent types are a pain, especially in Coq"

(this example might involve fewer/no dependent types but the same kind of problem)

In Coq we often accept the annoyance of partial lookups and option, exactly because alternatives tend to be delicate/fragile. They're great when they work, but they *can* sink a project and require starting over when they don't work.

I've had to start over in such cases, and it sounds like you're having to?

Yes, I had to start over at some point. I'm very happy that I was very early in the project when I had to.

Look. I think I'm making some progress.

```
From mathcomp Require Import all_ssreflect finmap.
Local Open Scope fset.
Local Open Scope fmap.
Section NS.
Variables (N S : choiceType).
Record cg : Type :=
CG { siteMap : {fmap S -> N}
; edges : rel S
; edges_sym : symmetric edges
}.
Section CG.
Variable (g : cg).
Definition nodes : {fset N} := codomf (siteMap g).
Definition sites : {fset S} := domf (siteMap g).
End CG.
Section Hom.
Variables (f_nodes : {fmap N -> N})
(f_sites : {fmap S -> S})
(dom : cg N S)
(cod : cg N S).
Hypotheses (f_nodes_total : nodes dom = domf f_nodes)
(f_sites_total : sites dom = domf f_sites).
Definition node_in_cod_of_site (s : sites dom) : N.
Proof. refine (f_nodes.[_]). rewrite -f_nodes_total.
exact: (in_codomf s).
Defined.
Print node_in_cod_of_site.
End Hom.
End NS.
```

Now I'm trying to make sense of the output of `Print node_in_cod_of_site`

. This is hard.

It's close to `f_nodes.[in_codomf s]`

which would be ideal but I'm not sure how to integrate the rewrite into that expression.

Maybe a coercion from `nodes dom`

to `domf f_nodes`

would do.

It works!

```
Coercion nodes_dom_is_domf_f_nodes (n : nodes dom) : domf f_nodes.
Proof. rewrite -f_nodes_total. exact: n. Defined.
```

Now, can this coercion be defined within the record so that I can use it in the declaration of later fields?

Import EqNotations + a term like "rew [id] f_nodes_total in n" would avoid tactics in Defined terms... Then you could use your definition/coercion to define a "mixin"-like thing that abstracts on f_nodes_total; and finally plug that mixin into a larger record bundling mixin + f_nodes_total + any other need

This is the closest I've got to what I'm trying to achieve.

```
From mathcomp Require Import all_ssreflect finmap.
Local Open Scope fset.
Local Open Scope fmap.
Section NS.
Variables (N S : choiceType).
Record cg : Type :=
CG { siteMap : {fmap S -> N}
; edges : rel S
; edges_sym : symmetric edges
}.
Section CG.
Variable (g : cg).
Definition nodes : {fset N} := codomf (siteMap g).
Definition sites : {fset S} := domf (siteMap g).
End CG.
Coercion cast (T : choiceType) (A B : {fset T}) (H : A = B)
(x : A) : B := eq_rect A id x B H.
Record hom : Type :=
Hom { dom : cg N S
; cod : cg N S
; f_nodes : {fmap N -> N}
; f_sites : {fmap S -> S}
; f_nodes_total : nodes dom = domf f_nodes
; f_sites_total : sites dom = domf f_sites
; f_nodes_sub_cod : codomf f_nodes `<=` nodes cod
; f_sites_sub_cod : codomf f_sites `<=` sites cod
; comm : [forall s : sites dom,
let s' := in_codomf (s : domf f_sites) in
f_nodes.[in_codomf s] ==
(siteMap cod).[(fsubsetP fsites_sub_cod) (val [`s']) s']]
; edge_pres : [forall s : sites dom, forall t : sites dom,
edges dom (val s) (val t) ==
edges cod (f_sites s) (f_sites t)]
}.
End NS.
```

It almost works, but `cast`

generates an internal placeholder of type `sites dom = domf f_sites`

for which the typechecker doesn't know what to do, even though there's a previous field that has that type.

A coercion can't really take an equality as an argument; what I meant is that a section parameter would work _in the section_.

OTOH, indexing coercions with hom could work, if they're typed `{h : hom} : foo h -> bar h`

. OTOH, I'm not confirmed that `nodes (dom h) -> domf (f_nodes h)`

would work well; seems it'd violate uniform inheritance?

The only problem with violating IUC is loosing the warning about ambiguous paths. But if you ensure by another mean the absence of ambiguous paths, everything is fine.

I have a comment on this, and a more general concern...

- Not sure how you would, and I was about to suggest
`Record hom := { ... ; nodes_dom := nodes dom; f_nodes_dom := domf f_nodes; ... }.`

and keying the coercion on`nodes_dom -> f_nodes_dom`

to avoid that... - But I fear a bigger problem: these coercions seem likely to hinder proofs, and it's even hard to substitute the underlying equalities since neither extreme's a variable. I fear this is a recipe for "my
`rewrite`

won't typecheck" problems, even tho I can't easily construct an example. Or if there's a pattern to avoid it, I don't know it...

e.g. maybe you must prove that some `n : nodes (dom h)`

is `=`

to some `n' : domf (f_nodes h)`

, but the statement involves `cast (f_nodes_total h)`

, and `f_nodes_total h`

will never become `eq_refl`

...

(and I'm aware of heterogeneous equality, but IME it just lets you defer solving the problem)

It is kind of sad that the typechecker can't pick up the equality from the local context (ie a previous field in the same record) for the coercion. I'm trying a different approach now. Here's the code.

```
Lemma eqEfsubset_id (T : choiceType) (A B : {fset T}) :
A = B -> A `<=` B.
Proof. move/eqP. by rewrite eqEfsubset => /andP[H _]. Qed.
Lemma eqEfsubset_opp (T : choiceType) (A B : {fset T}) :
A = B -> B `<=` A.
Proof. move/eqP. by rewrite eqEfsubset => /andP[_ H]. Qed.
Record hom : Type :=
Hom { dom : cg N S
; cod : cg N S
; f_nodes : {fmap N -> N}
; f_sites : {fmap S -> S}
; f_nodes_total : nodes dom = domf f_nodes
; f_sites_total : sites dom = domf f_sites
; f_nodes_sub_cod : codomf f_nodes `<=` nodes cod
; f_sites_sub_cod : codomf f_sites `<=` sites cod
; comm : [forall s : sites dom,
let s' : _ \in codomf f_sites :=
in_codomf (ct f_sites_total s) in
let n : _ \in nodes dom := in_codomf s in
let H : nodes dom `<=` domf f_nodes :=
eqEfsubset_id f_nodes_total in
let n' : _ \in domf f_nodes := (fsubsetP H) (val [`n]) n in
f_nodes.[n'] ==
(siteMap cod).[(fsubsetP f_sites_sub_cod) (val [`s']) s']]
}.
```

Even though it seems longer and less clear, I'm hopeful that it might lead to a good abstraction.

I forgot to copy the definition of `ct`

.

```
Definition ct (T : choiceType) (A B : {fset T}) (H : A = B)
(x : A) : B := eq_rect A id x B H.
```

Paolo Giarrusso said:

Import EqNotations + a term like "rew [id] f_nodes_total in n" would avoid tactics in Defined terms... Then you could use your definition/coercion to define a "mixin"-like thing that abstracts on f_nodes_total; and finally plug that mixin into a larger record bundling mixin + f_nodes_total + any other need

I don't understand mixins well enough to follow this idea. Do you have any guides or pointers to understand mixins and how they could be useful in this scenario?

On a different note, I'm thinking that module types or functors could be useful to have the coercions "in the air" when defining `comm`

and `edge_pres`

.

Ideally, the code would look like this.

```
Hom { dom : cg N S
; cod : cg N S
; f_nodes : {fmap N -> N}
; f_sites : {fmap S -> S}
; f_nodes_total : nodes dom = domf f_nodes
; f_sites_total : sites dom = domf f_sites
; f_nodes_sub_cod : codomf f_nodes `<=` nodes cod
; f_sites_sub_cod : codomf f_sites `<=` sites cod
; comm : [forall s : sites dom,
f_nodes (siteMap dom s) == siteMap cod (f_sites s)
; edge_pres : [forall s : sites dom, forall t : sites dom,
edges dom s t ==
edges cod (f_sites s) (f_sites t)]
}.
```

Rather than explaining "mixins" let me sketch this example very roughly:

```
Module HomMixin.
Section HomMixin.
Context (dom : ...) (f_nodes : ...) (f_nodes_total : nodes dom = domf f_nodes). (* and `f_sites_total` *)
Local Coercion foo : nodes dom >-> domf f_nodes := eq_rect ... f_nodes_total.
(* And other coercions *)
Record HomMixin := {
comm : [forall s : sites dom,
f_nodes (siteMap dom s) == siteMap cod (f_sites s)]
(* and also edge_pres *)
(* here we can rely on local coercions like `foo` when defining ` *)
}.
End HomMixin.
End HomMixin.
Record Hom := {
dom : ...; f_nodes : ...; f_nodes_total : ...;
hom_mixin : HomMixin dom f_nodes f_nodes_total
}.
(* Now we can define _global_ coercions indexed by `Hom`, if we want: *)
Global Coercion foo_global (h : Hom) : nodes (dom h) >-> domf (f_nodes h) := eq_rect ... f_nodes_total.
(* Boilerplate: lift properties *)
Lemma comm (h : Hom) : [forall s : sites (dom h),
f_nodes h (siteMap h dom s) == siteMap h cod (f_sites h s).
Proof. (* compose hom_mixin and HomMixin.comm, sth like *) apply: HomMixin.comm. exact: hom_mixin. Qed.
```

Basically, `HomMixin dom f_nodes ...`

is _indexed_ by the data `dom`

`f_nodes`

etc, while `Hom`

is a dependent record containing data and the mixin. In this case, the point is that we can define local coercions when declaring `HomMixin`

. I'm not sure that's worth it here (the usual pattern in math-comp has other reasons).

In my example I suggest declaring global coercions indexed by `Hom`

, like `foo_global`

, and then lifting properties with the right statements using the coercion; that might be more useful for clients.

the above section, BTW, is exactly a way to have coercions "in the air" when defining `comm`

.

OTOH, you can't translate this pattern using modules/functors: Coq forbids turning functors into normal functions — and even this definition:

```
Record Hom := {
dom : ...; f_nodes : ...; f_nodes_total : ...;
hom_mixin : HomMixin dom f_nodes f_nodes_total
}.
```

could not be expressed if `HomMixin`

were a functor.

I see. Thank you @Paolo Giarrusso for this example and the explanation. I understand it better now.

The reason why I'm going into all this trouble is that, down the line, I'll be very often chaining fmap applications and there'll be more elaborate commuting diagrams. So if this simple diagram cannot be expressed easily, I fear it'll be quite some trouble to express the more elaborate ones later on. I might be wrong though. These are just the fears of a newcomer to Coq and mathcomp.

Makes sense; FWIW, with partial lookups and option, worst-case you'll have to use `obind`

a lot; that can be improved by adding some decent monadic notation (at least for this case, you don't need something fully general). You'll probably also need to use `obind f oa = Some x -> ∃ a, oa = Some a /\ f a = Some x`

quite a bit.

OTOH, the mixin version shares the upsides and large risks of fancy dependent types — likein https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Shared.20domain.20of.20fmaps/near/326067438 point 2

Thank you very much @Paolo Giarrusso for your sharing your understanding with me and your kindness and time. I'll be using partial lookups and option. What library do you recommend for decent monadic notation? Is the library relatively lightweight?

I think what is difficult for me to get over is that in my mind an advantage of dependently typed languages is that you can avoid these kind of superfluous `if`

s where one of the branches is never taken. But I understand now that the price for getting rid of the `if`

is high.

It's probably worth splitting the "monadic notation" question.

I've used coq-stdpp's monadic notation https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/base.v#L1165-1174, but not worth mixing that with math-comp. I'd rather consider writing similar notations around obind, but I'm not a math-comp expert and there might be better variations (say, maybe abstracting over monads is easy enough; but it's not needed for the present goal).

I forgot: it might also be worth making functions total by using default values: the theory needs side conditions to avoid this case, but some of the overhead of option disappears.

Re dependent types, I agree that it's an alluring upside, and there's research on making that work well more often (say, in the Agda community). But similar concerns apply and people have different opinions on them...

I see. Well, for the time being I think I'll keep using `if ... is Some x then ...`

Thank you.

Ricardo has marked this topic as resolved.

Last updated: Jul 15 2024 at 21:02 UTC