Ricardo (Feb 05 2023 at 04:50): 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?
Ricardo (Feb 05 2023 at 05:03):I mean sharing their domain in a way that the type checker acknowledges it.
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).
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.
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
Paolo Giarrusso (Feb 05 2023 at 19:38):(above, P : pred K is arbitrary)
Paolo Giarrusso (Feb 05 2023 at 19:39):(Importantly, the decidable equality computes without getting stuck on funext, and makes their equality proof-irrelevant)
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
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?
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...
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.
Paolo Giarrusso (Feb 05 2023 at 20:18):@Ricardo or just store { fmap K -> (V1, V2) } and derive f and g?
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.
Paolo Giarrusso (Feb 05 2023 at 20:27):That's not necessarily a bad idea: it just means the implementation differs from the interface.
Paolo Giarrusso (Feb 05 2023 at 20:28):maybe mathematicians would talk about a representation (or not)
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
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.
Ricardo (Feb 05 2023 at 20:34):@Paolo Giarrusso I'd say the standard set-theoretic encodings aren't a high (or good) bar.
Paolo Giarrusso (Feb 05 2023 at 20:35):Agreed.
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?
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.
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'
comm ensures that this diagram commutes.
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 codor 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?
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
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.
Paolo Giarrusso (Feb 05 2023 at 20:52):(reminder I'm not actually a math-comp expert)
Paolo Giarrusso (Feb 05 2023 at 20:55):Basically, IIUC, all your functions are actually total, and your diagram only has 4 distinct types
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.
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.
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
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.
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"
Paolo Giarrusso (Feb 05 2023 at 21:27):(this example might involve fewer/no dependent types but the same kind of problem)
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.
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?
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.
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.
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.
Ricardo (Feb 05 2023 at 21:50):Maybe a coercion from nodes dom to domf f_nodes would do.
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?
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
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.
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_.
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?
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.
Paolo Giarrusso (Feb 06 2023 at 08:39):I have a comment on this, and a more general concern...
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...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... 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...
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)
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.
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.
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?
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.
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)]
}.
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.
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.
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.
Ricardo (Feb 08 2023 at 00:36):I see. Thank you @Paolo Giarrusso for this example and the explanation. I understand it better now.
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.
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.
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
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.
Paolo Giarrusso (Feb 10 2023 at 19:37):It's probably worth splitting the "monadic notation" question.
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).
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.
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...
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 ...
Ricardo (Feb 10 2023 at 19:51):Thank you.
Notification Bot (Feb 10 2023 at 19:51):Ricardo has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC