Stream: math-comp users

Topic: ✔ Shared domain of fmaps


view this post on Zulip Ricardo (Feb 05 2023 at 04:50):

Hi everyone. Hope you're all well. I'm wondering if there's a simple way to have two fmaps 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?

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

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

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

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

view this post on Zulip Laurent Théry (Feb 05 2023 at 12:01):

Maybe you could use option type if you have two maps

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

view this post on Zulip Ricardo (Feb 05 2023 at 19:13):

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.

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 19:37):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 19:38):

(above, P : pred K is arbitrary)

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 19:39):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 19:42):

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

view this post on Zulip Laurent Théry (Feb 05 2023 at 19:49):

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?


view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:11):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:15):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:18):

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

view this post on Zulip Ricardo (Feb 05 2023 at 20:26):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:27):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:28):

maybe mathematicians would talk about a representation (or not)

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:32):

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

view this post on Zulip Ricardo (Feb 05 2023 at 20:33):

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

view this post on Zulip Ricardo (Feb 05 2023 at 20:34):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:35):

Agreed.

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:35):

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?

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:37):

If it's about f_nodes/f_sites, I agree I'd prefer f_sites : nodes dom -> nodes cod or the like.

view this post on Zulip Ricardo (Feb 05 2023 at 20:41):

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

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

view this post on Zulip Ricardo (Feb 05 2023 at 20:42):

comm ensures that this diagram commutes.

view this post on Zulip Ricardo (Feb 05 2023 at 20:44):

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?

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:50):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:51):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:52):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:55):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 20:58):

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.

view this post on Zulip Ricardo (Feb 05 2023 at 21:12):

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.

view this post on Zulip Ricardo (Feb 05 2023 at 21:13):

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

view this post on Zulip Ricardo (Feb 05 2023 at 21:16):

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.

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 21:26):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 21:27):

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

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 21:32):

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.

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 21:33):

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

view this post on Zulip Ricardo (Feb 05 2023 at 21:38):

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.

view this post on Zulip Ricardo (Feb 05 2023 at 21:43):

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.

view this post on Zulip Ricardo (Feb 05 2023 at 21:45):

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.

view this post on Zulip Ricardo (Feb 05 2023 at 21:50):

Maybe a coercion from nodes dom to domf f_nodes would do.

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

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?

view this post on Zulip Paolo Giarrusso (Feb 06 2023 at 02:20):

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

view this post on Zulip Ricardo (Feb 06 2023 at 02:31):

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.

view this post on Zulip Paolo Giarrusso (Feb 06 2023 at 07:10):

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

view this post on Zulip Paolo Giarrusso (Feb 06 2023 at 07:23):

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?

view this post on Zulip Pierre Roux (Feb 06 2023 at 07:32):

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.

view this post on Zulip Paolo Giarrusso (Feb 06 2023 at 08:39):

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

  1. 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...
  2. 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...

view this post on Zulip Paolo Giarrusso (Feb 06 2023 at 08:41):

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

view this post on Zulip Paolo Giarrusso (Feb 06 2023 at 08:43):

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

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

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.

view this post on Zulip Ricardo (Feb 07 2023 at 05:15):

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.

view this post on Zulip Ricardo (Feb 07 2023 at 23:34):

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?

view this post on Zulip Ricardo (Feb 07 2023 at 23:38):

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.

view this post on Zulip Ricardo (Feb 07 2023 at 23:53):

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

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:26):

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.

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:27):

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

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:28):

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.

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

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

view this post on Zulip Ricardo (Feb 08 2023 at 00:41):

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.

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:47):

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.

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:48):

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

view this post on Zulip Ricardo (Feb 10 2023 at 19:18):

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 ifs where one of the branches is never taken. But I understand now that the price for getting rid of the if is high.

view this post on Zulip Paolo Giarrusso (Feb 10 2023 at 19:37):

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

view this post on Zulip Paolo Giarrusso (Feb 10 2023 at 19:38):

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

view this post on Zulip Paolo Giarrusso (Feb 10 2023 at 19:43):

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.

view this post on Zulip Paolo Giarrusso (Feb 10 2023 at 19:49):

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

view this post on Zulip Ricardo (Feb 10 2023 at 19:51):

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

view this post on Zulip Ricardo (Feb 10 2023 at 19:51):

Thank you.

view this post on Zulip Notification Bot (Feb 10 2023 at 19:51):

Ricardo has marked this topic as resolved.


Last updated: Jul 15 2024 at 21:02 UTC