Ricardo (Nov 09 2022 at 02:19): Ricardo (Nov 09 2022 at 02:19):Hi. I'm learning math-comp. I read most of Programs and Proofs by Ilya Sergey and now reading the math-comp book, especially the chapter about sub-types and the sections on finite types, sets and functions. Just today I started venturing into writing a data structure for a special case of finite simple undirected graphs. Here's what I wrote.
From mathcomp
Require Import ssreflect ssrbool ssrnat ssrfun
eqtype fintype seq finfun.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module SiteGraphs.
Record sg : Type :=
SG { nodes : finType
; sites : finType
; siteMap : {ffun sites -> nodes}
; edges : rel sites
; _ : [forall s1, forall s2, edges s1 s2 == edges s2 s1]
}.
Definition empty : sg :=
@SG void_finType void_finType [ffun x => match x with end] (fun _ _ => false) _.
End SiteGraphs.
Does the definition of sg make sense to you? Would it be better to use {set T} instead of finType for nodes and sites? But then I'd need the T in {set T} to be a finType anyway so I'm not sure.
Also, the definition of empty doesn't compile in the code above. How would you define the empty graph given the structure above?
Karl Palmskog (Nov 09 2022 at 07:10):if all you want is simple undirected graphs on a finType, why not just use fingraph module in the mathcomp-ssreflect package? Much less packaging in that encoding. For a more general encoding, see: https://github.com/coq-community/graph-theory
Karl Palmskog (Nov 09 2022 at 07:11):some algorithms using fingraph: https://github.com/math-comp/tarjan
Ricardo (Nov 09 2022 at 19:12):Thanks Karl. I had a quick look at fingraph.v and I think it won't be useful for what I'm trying to achieve. I'm trying to formalise graphs that aren't quite like the usual ones. We call them site graphs. In particular, I'm trying to formalise something close to what's described in this paper.
Nevertheless, it might be useful for me to understand how you'd represent an empty graph with fingraph. Would T be void_finType? What would g: T -> seq T be?
Karl Palmskog (Nov 09 2022 at 19:20):fingraph uses both T -> seq T and rel T. I guess the most obvious empty graph would be the rel T one, namely (fun x y => false) : rel T, for example (fun x y => false) : rel void_finType I guess
Karl Palmskog (Nov 09 2022 at 19:24):if fingraph is not enough I still think your best bet is to hook into https://github.com/coq-community/graph-theory in some way, or roughly build on its encodings (it goes far beyond fingraph)
Ricardo (Nov 09 2022 at 20:07):That's great. Thanks! I managed to build an empty graph with
Lemma rel0_sym (R: rel void) :
[forall x, forall y, R x y == R y x].
Proof. by apply/forallP. Qed.
Definition empty : sg :=
@SG void_finType void_finType
(finfun (of_void void)) (of_void _) (rel0_sym _).
I'll check the graph-theory library
Ricardo (Nov 09 2022 at 21:58):It seems the graph-theory library is quite big. I'm reading digraph.v and the approach to graphs there seems very close to what I wrote before.
Ricardo (Nov 09 2022 at 22:28):I'm looking at sgraph.v now and the implementation is also quite similar.
Alexander Gryzlov (Nov 10 2022 at 12:20):I'm also working on graph algorithms in HTT now and I use finite maps on arbitrary ordered types to encode (adjacency lists for) partial quivers - basically graphs where the destination vertex might be missing, this allows to split and combine them.
Ricardo (Nov 10 2022 at 18:50):Nice. I was also thinking about using finmap.
Ricardo (Nov 10 2022 at 21:19):Here's a finmap-based attempt.
Record sg (N S : choiceType) : Type :=
SG { nodes : {fset N}
; siteMap : {fmap S -> nodes}
; sites := domf siteMap
; edges : rel sites
; _ : symmetric edges
}.
Definition rel0n (_ _ : nat_choiceType) := false.
Definition empty : sg nat_choiceType nat_choiceType :=
@SG nat_choiceType nat_choiceType (fset0 : {fset nat_choiceType})
(fmap0 : {fmap nat_choiceType -> nat_choiceType}) rel0n _.
However, the last line doesn't compile because it can't unify {fmap nat_choiceType -> nat_choiceType} with {fmap nat_choiceType -> fset0}. Given that fset0 has type {fset nat_choiceType}, I think Coq is missing a coercion from {fset nat_choiceType} to nat_choiceType. Does anyone know why that could be?
Ricardo (Nov 10 2022 at 21:24):If I remove the type annotations, then it can't unify rel0n with rel (domf [fmap]%fmap).
Definition empty : sg nat_choiceType nat_choiceType :=
@SG nat_choiceType nat_choiceType fset0 fmap0 rel0n _.
The error says it can't unify fset_sub_type (domf [fmap]%fmap) with Choice.sort nat_choiceType.
Paolo Giarrusso (Nov 10 2022 at 21:25):Slly Q: Aren't you asking for a coercion from a set of nats to a nat?
Ricardo (Nov 10 2022 at 21:27):Not sure. How can I know?
Paolo Giarrusso (Nov 10 2022 at 21:29):Given that fset0 has type {fset nat_choiceType}, I think Coq is missing a coercion from {fset nat_choiceType} to nat_choiceType.
But docs say:
{fset K} == finite sets of elements of K
Paolo Giarrusso (Nov 10 2022 at 21:33):Ah, I guess what you need is an (empty) function in {fmap nat_choiceType -> fset0} since finsets can be coerced to types the type of their elements...
(* - There is a coercion from {fset K} to Type in order to interpret any *)
(* finset A as the subType of elements a : K such that a \in A. *)
(* Because of this coercion, writing a : A makes sense. *)
I see. I think I understand.
Ricardo (Nov 10 2022 at 21:34):Yes, that's what I need.
Ricardo (Nov 10 2022 at 21:35):I thought rel0n could be such a function but it doesn't work.
Paolo Giarrusso (Nov 10 2022 at 21:43):I recommend trying out the refine tactic to construct these terms step-by-step. For instance, I've reproduced your first example (since it's complete), and there I can successfully run:
Definition empty : sg.
refine (@SG void_finType void_finType _ _ _).
this will leave some holes that you can try to fill in using refine (or other tactics).
Paolo Giarrusso (Nov 10 2022 at 21:45):I'd recommend assembling the final result back into one piece, but it can make your life much easier when you're using dependent types as heavily as you're doing.
Paolo Giarrusso (Nov 10 2022 at 21:45):in this example you can probably start from
Definition empty : sg nat_choiceType nat_choiceType.
refine (@SG nat_choiceType nat_choiceType _ _ _ _).
and proceed.
Ricardo (Nov 10 2022 at 21:51):Thank you Paolo! I'll try this.
Ricardo (Nov 10 2022 at 22:40):Wow. It worked! I'm impressed by the efficacy of this method. Thank you again Paolo.
I did as you recommended. Here's the full file.
From mathcomp
Require Import ssreflect ssrbool ssrnat ssrfun
eqtype choice fintype seq finfun finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module SiteGraphs.
Definition symmetric (T : finType) (R: rel T) :=
[forall x, forall y, R x y == R y x].
Definition relF (C : choiceType) (F : {fset C}) (_ _ : F) := false.
Lemma relF_sym (C : choiceType) (F : {fset C}) : symmetric (@relF C F).
Proof. apply/forallP => x. by apply/forallP. Qed.
Record sg (N S : choiceType) : Type :=
SG { nodes : {fset N}
; siteMap : {fmap S -> nodes}
; sites := domf siteMap (* : {fset S} *)
; edges : rel sites
; _ : symmetric edges
}.
Definition empty : sg nat_choiceType nat_choiceType.
refine (@SG _ _ fset0 fmap0 _ _).
apply: relF_sym.
Defined.
End SiteGraphs.
Question. Why can't I write sg nat nat instead of sg nat_choiceType nat_choiceType? I see there's a canonical declaration in line 476 of choice.v for nat and nat_choiceType. Shouldn't that help? Or is there something else missing?
Ana de Almeida Borges (Nov 10 2022 at 23:35):Sometimes Coq needs a little help with this, although I don't have a clear model of when. Note that you can use [choiceType of nat] instead of nat_choiceType. Here it doesn't make much of a difference, but it does when the type is more complex, eg [choiceType of nat * nat] is much simpler than prod_choiceType nat_choiceType nat_choiceType.
Paolo Giarrusso (Nov 11 2022 at 01:08):IIUC, you can never pass a Type to a function taking a choiceType (or other structure) directly, like e.g. relF or sg, so math-comp defines these [finType of nat] notations.
Paolo Giarrusso (Nov 11 2022 at 01:08):But if you have a function taking {T : choiceType} (x : T)? Then passing x : nat is perfectly fine
Paolo Giarrusso (Nov 11 2022 at 01:10):Here's a demo (again on the first example):
Record sg : Type :=
SG { nodes : finType
; sites : finType
; siteMap : {ffun sites -> nodes}
; edges : rel sites
; _ : [forall s1, forall s2, edges s1 s2 == edges s2 s1]
}.
Arguments SG nodes {sites} siteMap edges _.
Definition empty : sg.
refine (SG [finType of void] [ffun x : void => match x with end] (fun _ _ => false) _).
abstract exact/forallP.
Defined.
Here, ffun x : void is enough to tell Coq that sites := [finType of void]. OTOH, I passed nodes explicitly using this [finType of void] syntax
Paolo Giarrusso (Nov 11 2022 at 01:13):and I used abstract to ensure the proof isn't visible when you unfold empty.
Paolo Giarrusso (Nov 11 2022 at 01:18):why can Coq infer sites from the void type annotation in [ffun x : void =>? Behind the scenes, the type of siteMap is really {ffun Finite.sort sites -> nodes} — where Finite.sort is an implicit coercion from finType to Type.
The annotation tells Coq that Finite.sort sites must equal void. And solving the equation Finite.sort sites = void is _the_ thing that canonical structures do.
Paolo Giarrusso (Nov 11 2022 at 01:21):https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/What.20is.20the.20problem.20with.20.60seq.20A.60.20if.20.20just.20has.20.60EqType.60.3F/near/306037529 and Enrico's answer has pointers to some good material on CSes
Last updated: Jan 29 2023 at 18:03 UTC