## Stream: math-comp users

### Topic: Non-instantiated existential variables

#### Ricardo (Nov 14 2022 at 02:37):

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?

#### Julien Puydt (Nov 14 2022 at 06:17):

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

#### Julien Puydt (Nov 14 2022 at 06:24):

Ah, no that's part of the `{fset ...}` notation, not an implicit variable...

#### Julien Puydt (Nov 14 2022 at 06:26):

You know, if you drop your definition of `symmetric`, then your `relF_sym` lemma is just a `by []` away.

#### Julien Puydt (Nov 14 2022 at 06:29):

or is there a trick there too?

#### Julien Puydt (Nov 14 2022 at 06:55):

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

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

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

#### Ricardo (Nov 14 2022 at 15:51):

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?

#### Julien Puydt (Nov 14 2022 at 15:56):

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

End SG_NS.

End SiteGraphs.
``````

#### Ricardo (Nov 14 2022 at 16:11):

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

#### Ricardo (Nov 14 2022 at 16:12):

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

#### Julien Puydt (Nov 14 2022 at 16:25):

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

#### Ricardo (Nov 14 2022 at 16:42):

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.

#### Ricardo (Nov 14 2022 at 16:58):

I'm also not getting the second `exists`.

#### Julien Puydt (Nov 14 2022 at 17:44):

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

#### Ricardo (Nov 14 2022 at 18:12):

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

#### Ricardo (Nov 14 2022 at 18:15):

You mean that the first field of the `fmap` record is `domf`?

#### Ricardo (Nov 14 2022 at 18:45):

I mean, the second `exists` makes sense but I don't understand what it's doing mechanically.

#### Alexander Gryzlov (Nov 14 2022 at 19:06):

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

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

#### Ricardo (Nov 14 2022 at 19:13):

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

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

#### Alexander Gryzlov (Nov 14 2022 at 19:23):

Oh nevermind, it's actually constructing this with the second `exists`: https://github.com/math-comp/finmap/blob/master/finmap.v#L527

#### Ricardo (Nov 14 2022 at 19:31):

@Alexander Gryzlov, how can an `exists` construct an `FSetSub`?

#### Alexander Gryzlov (Nov 14 2022 at 19:34):

It's a form of `constructor` tactic, see https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html?highlight=exists#coq:tacn.exists

#### Ricardo (Nov 14 2022 at 19:36):

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?

#### Ricardo (Nov 14 2022 at 19:38):

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:

#### Ricardo (Nov 14 2022 at 20:03):

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 (Nov 14 2022 at 20:22):

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?

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

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

#### Julien Puydt (Nov 14 2022 at 22:38):

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

and now I just need to find out how to replace `have`: it only gives opaque values...

#### Ricardo (Nov 14 2022 at 22:39):

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:

#### Julien Puydt (Nov 14 2022 at 22:40):

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

#### Julien Puydt (Nov 14 2022 at 22:42):

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

#### Ricardo (Nov 14 2022 at 22:50):

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