I'm trying to define an `add_node`

function in the following code.

```
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
}.
Section SG_NS.
Variables (N S : choiceType).
Definition empty : sg N S :=
@SG _ _ fset0 fmap0 _ (relF_sym (domf fmap0)).
Variable (G : sg N S).
Definition add_node (n : N) : sg N S.
case: G => ns sm ss es es_sym.
refine (@SG _ _ (n |` ns)%fset _ _ _).
exact: es_sym.
```

After the last tactic I get this warning.

```
No more goals, but there are non-instantiated existential variables:
Existential 1 =
...
You can use Unshelve.
```

If I use Unshelve, nothing seems to happen. How can I transform the non-instantiated existential variables into subgoals here?

Shouldn't the `(foo: {someType})`

actually be `{foo: someType}`

?

Ah, no that's part of the `{fset ...}`

notation, not an implicit variable...

You know, if you drop your definition of `symmetric`

, then your `relF_sym`

lemma is just a `by []`

away.

or is there a trick there too?

I modified your code slightly and obtained a goal which seems attainable: prove that `sm`

which is a finite map from `S`

to `ns`

is also a finite map from `S`

to `n | ns`

, but since I never worked with `ffun`

, I don't know how to do that yet...

Julien Puydt said:

You know, if you drop your definition of

`symmetric`

, then your`relF_sym`

lemma is just a`by []`

away.

I'm not sure I understand this. If I write the following

```
Lemma relF_sym (C : choiceType) (F : {fset C}) :
[forall x, forall y, (@relF C F) x y == (@relF C F) y x].
Proof. by []. Qed.
```

I get `Error: No applicable tactic.`

Julien Puydt said:

I modified your code slightly and obtained a goal which seems attainable: prove that

`sm`

which is a finite map from`S`

to`ns`

is also a finite map from`S`

to`n | ns`

, but since I never worked with`ffun`

, I don't know how to do that yet...

That's the goal I thought I'd have to prove, but I don't know how to get that as a goal from

```
Definition add_node (n : N) : sg N S.
```

@Julien Puydt, would you share with us your modified code?

The modifications are:

- modify
`relF`

to simplify the lemma ; - modify the record because I didn't like having
`sites`

if it's computable from the rest.

As you see, there are still two holes...

```
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.
(* FIXME: both the definition and the lemma should be there already *)
Definition relF {F : Type} (_ _ : F) := false.
Lemma relF_sym {C : choiceType} (F : {fset C}) : symmetric (@relF F).
Proof.
by [].
Qed.
Record sg (N S : choiceType) : Type :=
SG {
nodes : {fset N};
siteMap : {fmap S -> nodes};
edges : rel (domf siteMap);
_ : symmetric edges
}.
Section SG_NS.
Variables (N S : choiceType).
Definition empty : sg N S := @SG N S fset0 fmap0 relF (@relF_sym _ _).
Variable (G : sg N S).
Definition add_node (n : N) : sg N S.
case: G => ns sm es es_sym.
have sm_plus: {fmap S -> (n |` ns)%fset}.
exists (domf sm).
refine [ffun x => _].
exists (val (sm x)). (* FIXME: suggestion of YB to understand *)
rewrite in_fsetU.
apply/orP.
right.
by case: (sm x) => v Hv.
have es_plus: rel (domf sm_plus).
have ->: domf sm_plus = domf sm ; last by [].
admit. (* FIXME: too many phantoms haunt the place *)
have symmetric_es_plus: symmetric es_plus.
admit. (* FIXME: should go like a breeze after the previous *)
exact (@SG _ _ (n |` ns)%fset sm_plus es_plus symmetric_es_plus).
Admitted.
End SG_NS.
End SiteGraphs.
```

I see. You're using the `Prop`

-based `symmetric`

instead of the `bool`

-based I defined. I thought it'd be more aligned with ssreflect's spirit to write and use a `bool`

-based `symmetric`

.

Thank you! With these ideas I'll try to continue.

I'm not sure that's the right track... I'm a beginner too!

I'm not getting why the line `exists (domf sm)`

after the first `have`

transforms `{fmap S -> (n |` ns)%fset}`

into `{ffun domf sm -> (n |` ns)%fset}`

. I can replicate the transformation with `apply: (@FinMap S ns' ss).`

where `ns' := (n |` ns)%fset`

and `ss := (domf sm)`

. Why does `exists`

help here? What is the existential variable that we are instantiating with `exists`

? I tried unfolding everything in sight but didn't find any existential variables.

I'm also not getting the second `exists`

.

The first exist is because an fmap is first a domain ; the second I haven't grasped yet

What does it mean that fmap is first a domain? How's that related to existential variables?

You mean that the first field of the `fmap`

record is `domf`

?

I mean, the second `exists`

makes sense but I don't understand what it's doing mechanically.

https://github.com/math-comp/finmap/blob/master/finmap.v#L488

https://github.com/math-comp/finmap/blob/master/finmap.v#L2885

I'm trying to understand how to work with the goal we reach after the `refine`

in your code.

```
Goal forall (N S : choiceType) (G : sg N S), (nodes G).
(* move=> N S G. exact: (nodes G). *)
move=> N S.
case=> ns sm ss es es_sym.
(* case: ns. *)
case: (enum_fset ns) => [| n ns' ].
- (* exact: fset0. *) admit.
- exists n.
Admitted.
```

Why doesn't the first commented line work? How can I prove this goal? Is it provable?

Oh nevermind, it's actually constructing this with the second `exists`

: https://github.com/math-comp/finmap/blob/master/finmap.v#L527

@Alexander Gryzlov, how can an `exists`

construct an `FSetSub`

?

It's a form of `constructor`

tactic, see https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html?highlight=exists#coq:tacn.exists

To prove `es_plus`

it'd be nice if we could remember how `sm_plus`

was constructed, since `domf sm_plus = domf sm`

by construction. Am I understading correctly that `have`

is designed not to remember the computationally relevant part?

Alexander Gryzlov said:

It's a form of

`constructor`

tactic, see https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html?highlight=exists#coq:tacn.exists

I see. Thank you! That helps me a lot :smile:

With the line `case: (sm x)`

it seems we are doing case-analysis on something of type `FSetSub`

. Why is that so? Because the codomain of `sm`

is an `fset`

? Or more precisely because `sm x`

is an element of `ns`

? Or because there is a coercion from `fset`

to `fset_sub_type`

?

Ricardo said:

With the line

`case: (sm x)`

it seems we are doing case-analysis on something of type`FSetSub`

. Why is that so? Because the codomain of`sm`

is an`fset`

? Or more precisely because`sm x`

is an element of`ns`

? Or because there is a coercion from`fset`

to`fset_sub_type`

?

It seems we can do case-analysis on any element of an `fset`

as if it was an element of `fset_sub_type`

. Is that due to a coercion?

I used `Pring Graph`

and searched for `> fset`

to find coercions into `fset_sub_type`

but didin't find anything. There are lots of coercion paths that mention `fset_sub_type`

though. For example,

```
[fset_sub_type] : finSet >-> predArgType
```

Is this the coercion I'm looking for? If so, I'm not getting why `case: (sm x)`

is case-analysing on something of the form `FSetSub`

when `predArgType = Type`

.

I simplified things a bit:

```
Definition add_node (n : N) : sg N S.
case: G => ns sm es es_sym.
have sm_plus: {fmap S -> (n |` ns)%fset}.
refine [fmap x: domf sm => fincl _ (sm x)].
by rewrite /fsubset (fsetKUC _ _).
have same_dom: domf sm_plus = domf sm.
admit. (* FIXME: sm_plus is opaque *)
have es_plus: rel (domf sm_plus).
rewrite same_dom.
exact es.
have symmetric_es_plus: symmetric es_plus.
admit. (* FIXME: es_plus is opaque! *)
exact (@SG _ _ (n |` ns)%fset sm_plus es_plus symmetric_es_plus).
Admitted.
```

and now I just need to find out how to replace `have`

: it only gives opaque values...

By setting `Printing Coercions`

I see that `sm x`

is transformed into `fun_of_fin (ffun_of_fmap sm) x`

of type `fset_sub_type ns`

. By checking with `Check sm`

I see that the type of `sm`

is actually `{fmap Choice.sort S -> fset_sub_type ns}`

instead of `{fmap Choice.sort S -> ns}`

. By printing with `Print sg`

I see that the type of `sg`

does have `fset_sub_type nodes`

in the type of `siteMap`

already.

That solves the puzzle. Thank you everyone :smile:

Here is some sample code showing off what I understand from finmap:

```
From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun eqtype choice fintype seq finfun.
From mathcomp.finmap Require Import finmap.
Section Foo.
Local Open Scope fset.
Local Open Scope fmap.
Variable D T: choiceType. (* Definition and Target *)
Variable A: {fset D}.
Variable B C: {fset T}.
Hypothesis BsubC: B `<=` C.
Variable f: {fmap A -> B}.
Definition ftilde: {fmap A -> C}.
Proof.
refine [fmap x: domf f => fincl _ (f x)].
by rewrite /fsubset.
Defined.
Lemma same_dom: domf f = domf ftilde.
Proof.
by [].
Qed.
(* FIXME: not really satisfying *)
Lemma same_values: forall x, ftilde.[? x] = [ffun x0 => (fincl BsubC) (f x0)].[? x].
Proof.
by rewrite /ftilde.
Qed.
End Foo.
```

@Ricardo If you have working code, I'd like to see it, please.

I haven't solved the puzzle of how to write `add_node`

. I only solved the puzzle of why we can do case analysis on `sm x`

.

Julien Puydt said:

and now I just need to find out how to replace

`have`

: it only gives opaque values...

Yeah that's exactly what I was thinking. Your last code works because `ftilde`

is defined transparently. We need a transparent `have`

for this.

Wow I made it. Thank you @Julien Puydt! Your help was very useful to get here. I mean, you did it really.

```
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.
Local Open Scope fset.
Local Open Scope fmap.
(* symmetric relations *)
Definition symmetric (T : finType) (R: rel T) :=
[forall x, forall y, R x y == R y x].
Definition rel0 (C : choiceType) (F : {fset C}) (_ _ : F) := false.
Lemma rel0_sym (C : choiceType) (F : {fset C}) : symmetric (@rel0 C F).
Proof. apply/forallP => x. by apply/forallP. Qed.
(* site graphs *)
Record sg (N S : choiceType) : Type :=
SG { nodes : {fset N}
; siteMap : {fmap S -> nodes}
; sites := domf siteMap (* : {fset S} *)
; edges : rel sites
; _ : symmetric edges
}.
Section SG_NS.
Variables (N S : choiceType).
Definition empty : sg N S :=
@SG _ _ fset0 fmap0 _ (rel0_sym (domf fmap0)).
Variable (G : sg N S).
Definition add_node (n : N) : sg N S.
case: G => ns sm ss es es_sym.
set ns' := (n |` ns). About fsetKUC.
have ns_sub_ns' : ns `<=` ns' by rewrite /fsubset fsetKUC.
set sm' : {fmap S -> ns'} :=
[fmap x: ss => fincl ns_sub_ns' (sm x)].
have eq_sites : domf sm' = ss by [].
pose es' : rel (domf sm') := fun x y => es x y.
have es'_sym : symmetric es' by [].
exact: (@SG _ _ ns' sm' es' es'_sym).
Defined.
End SG_NS.
End SiteGraphs.
```

Still, it'd be great to know if there's a variant of `have`

that is transparent.

Oh, it was easier than we thought. You just need to put an `@`

in front of the name to make the definition transparent according to the docs, like in

```
have @sm' : {fmap S -> ns'}.
refine [fmap x: ss => fincl _ (sm x)].
by rewrite /fsubset fsetKUC.
```

Ricardo has marked this topic as resolved.

Direct solution

```
Local Open Scope fset_scope.
Definition add_node (n : N) : sg N S :=
@SG N S (n |` nodes G)
(FinMap (finfun (fincl (fsubsetUr [fset n] (nodes G)) \o siteMap G)))
(@edges N S G) (@edges_sym N S G).
```

Nice! Thanks @Cyril Cohen.

I didn't know and didn't find the `have @`

trick! I'm still not entirely satisfied with what I have. Changes: I mostly put some arguments in `{ }`

to turn them optional, use `g`

instead of `G`

because it's a specific object and not a type and use `'`

as suffix instead of `_plus`

:

```
(* Ricardo @ 'math-comp users' *)
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.
(* FIXME: both the definition and the lemma should be there already *)
Definition relF {F : Type} (_ _ : F) := false.
Lemma relF_sym {C : choiceType} {F : {fset C}} : symmetric (@relF F).
Proof.
by [].
Qed.
Record sg {N S : choiceType} : Type :=
SG {
nodes : {fset N};
siteMap : {fmap S -> nodes};
edges : rel (domf siteMap);
edges_sym : symmetric edges
}.
Section SG_NS.
Local Open Scope fset.
Variables (N S : choiceType).
Definition empty : sg := @SG N S fset0 fmap0 relF relF_sym.
Variable (g : @sg N S).
(* after a discussion with Ricardo, this is the result: *)
Definition add_node (n : N) : @sg N S.
case: g => ns sm es es_sym.
set ns' := (n |` ns).
have @sm': {fmap S -> ns'}.
refine [fmap x: domf sm => fincl _ (sm x)].
by rewrite /fsubset (fsetKUC _ _).
have @es': rel (domf sm') := es.
have symmetric_es': symmetric es' by [].
exact (SG symmetric_es').
Qed.
Check g.
Check edges.
Fail Check edges g. (* FIXME: why? consequence: below @edges ... *)
Check g.
Check edges_sym.
Fail Check edges_sym g. (* FIXME: same issue... *)
(* and Cyril Cohen proposes: *)
Definition add_node_bis (n: N): sg :=
@SG _ _ (n |` nodes g)
(FinMap (finfun (fincl (fsubsetUr [fset n] (nodes g)) \o siteMap g)))
(@edges _ _ g) (@edges_sym _ _ g).
End SG_NS.
End SiteGraphs.
```

Last updated: Jul 23 2024 at 21:01 UTC