## Stream: math-comp users

### Topic: ✔ Non-instantiated existential variables

#### Ricardo (Nov 14 2022 at 23:04):

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.

#### Ricardo (Nov 14 2022 at 23:47):

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

#### Ricardo (Nov 14 2022 at 23:48):

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

#### Ricardo (Nov 14 2022 at 23:57):

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

#### Notification Bot (Nov 14 2022 at 23:58):

Ricardo has marked this topic as resolved.

#### Cyril Cohen (Nov 14 2022 at 23:59):

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

#### Ricardo (Nov 15 2022 at 00:03):

Nice! Thanks @Cyril Cohen.

#### Julien Puydt (Nov 15 2022 at 06:04):

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: Feb 08 2023 at 07:02 UTC