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

```
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,

```
[type_of_finset; fset_sub_type] : finset_of >-> 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 type `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`

.

Last updated: Feb 08 2023 at 04:04 UTC