Stream: math-comp users

Topic: Non-instantiated existential variables


view this post on Zulip 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?

view this post on Zulip Julien Puydt (Nov 14 2022 at 06:17):

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

view this post on Zulip Julien Puydt (Nov 14 2022 at 06:24):

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

view this post on Zulip 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.

view this post on Zulip Julien Puydt (Nov 14 2022 at 06:29):

or is there a trick there too?

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Julien Puydt (Nov 14 2022 at 15:56):

The modifications are:

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.

view this post on Zulip 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.

view this post on Zulip Ricardo (Nov 14 2022 at 16:12):

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

view this post on Zulip Julien Puydt (Nov 14 2022 at 16:25):

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

view this post on Zulip 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.

view this post on Zulip Ricardo (Nov 14 2022 at 16:58):

I'm also not getting the second exists.

view this post on Zulip 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

view this post on Zulip Ricardo (Nov 14 2022 at 18:12):

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

view this post on Zulip Ricardo (Nov 14 2022 at 18:15):

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

view this post on Zulip Ricardo (Nov 14 2022 at 18:45):

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

view this post on Zulip 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

view this post on Zulip 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.
Admitted.

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

view this post on Zulip 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

view this post on Zulip Ricardo (Nov 14 2022 at 19:31):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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).
Admitted.

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Julien Puydt (Nov 14 2022 at 22:42):

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

view this post on Zulip 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