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?

if all you want is simple undirected graphs on a `finType`

, why not just use `fingraph`

module in the mathcomp-ssreflect package [but with added graph relation symmetry]? Much less packaging in that encoding. For a more general encoding, see: https://github.com/coq-community/graph-theory

some algorithms using `fingraph`

: https://github.com/math-comp/tarjan

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?

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

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)

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

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.

I'm looking at `sgraph.v`

now and the implementation is also quite similar.

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.

Nice. I was also thinking about using `finmap`

.

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?

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`

.

Slly Q: Aren't you asking for a coercion from a set of nats to a nat?

Not sure. How can I know?

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

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.

Yes, that's what I need.

I thought `rel0n`

could be such a function but it doesn't work.

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

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.

in this example you can probably start from

```
Definition empty : sg nat_choiceType nat_choiceType.
refine (@SG nat_choiceType nat_choiceType _ _ _ _).
```

and proceed.

Thank you Paolo! I'll try this.

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?

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`

.

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.

But if you have a function taking `{T : choiceType} (x : T)`

? Then passing `x : nat`

is perfectly fine

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

and I used `abstract`

to ensure the proof isn't visible when you unfold `empty`

.

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.

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

I see. Thank you Ana and Paolo. I thought about how to use a function taking `{T : choiceType} (x : T)`

to be able to write `sg nat nat`

. Since a particular `nat`

value has to be given to the function for it to recreate `T`

, I don't think it's possible. I came up with this simple notation instead.

```
Notation sgn := (sg [choiceType of nat] [choiceType of nat]).
```

I think that'll be enough for now. Thank you.

Ricardo has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC