Приведение finset к finType в Coq / Ssreflect - PullRequest
Новая
       24

Приведение finset к finType в Coq / Ssreflect

0 голосов
/ 07 декабря 2018

Я изучаю Ssreflect и хочу знать, как решить эту ситуацию.Моя идея состоит в том, чтобы определить график (как запись), а затем сгенерировать другой график.Ниже я показываю фрагмент кода (который я извлек из более крупного), который говорит сам за себя: 

Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import eqtype ssrnat fintype finset.

Section Example.

Record ugraph := UGraph { T : finType ;
                          V : {set T} ;
                          E : {set {set T}} ;
        edges_have_vertices : forall e : {set T}, e \in E -> e \subset V ;
             edges_size_two : forall e : {set T}, e \in E -> #|e| == 2}.

Variable G : ugraph.

Definition closed_neigh : T G -> {set T G} := fun u => [set v | [set u; v] \in E G] :|: [set u].
Notation "N[ x ]" := (closed_neigh x) (at level 0, x at level 99).

Definition T_Gp := prod_finType (T G) (T G).

(* V' is the set of (u, v) such that u \in V and v \in N[u] *)
Definition V_Gp := [set x : T_Gp | (x.1 \in V G) && (x.2 \in (N[x.1]))].

(* E' is the set of edges {uv, zr} such that uv, zr \in V', uv != zr and z \in N[v] *)
Definition E_Gp := [set e : {set T_Gp} | [exists x : T_Gp, [exists y : T_Gp, (e == [set x; y]) && (x != y) && (x \in V_Gp) && (y \in V_Gp) && (y.1 \in N[x.2])]]].

Lemma edges_have_vertices_Gp : forall e : {set T_Gp}, e \in E_Gp -> e \subset V_Gp.
Admitted.

Lemma edges_size_two_Gp : forall e : {set T_Gp}, e \in E_Gp -> #|e| == 2.
Admitted.

Definition gen_Gp := @UGraph T_Gp V_Gp E_Gp edges_have_vertices_Gp edges_size_two_Gp.

End Example.

Обратите внимание, что в настоящее время я использую finType T , а затемнабор вершин является каким-то образом подмножеством T. Однако я чувствую, что могу воспользоваться этим, рассматривая набор вершин как сам тип finType и избегая доказательства "dge_have_vertices ", как показано ниже: 

Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import eqtype ssrnat fintype finset.

Section Example.

Record ugraph := UGraph { V : finType ;
                          E : {set {set V}} ;
             edges_size_two : forall e : {set V}, e \in E -> #|e| == 2}.

Variable G : ugraph.

Definition closed_neigh : V G -> {set V G} := fun u => [set v | [set u; v] \in E G] :|: [set u].
Notation "N[ x ]" := (closed_neigh x) (at level 0, x at level 99).

Definition V_Gp := [set x : prod_finType (V G) (V G) | (x.1 \in V G) && (x.2 \in (N[x.1]))].

Definition E_Gp := [set e : {set V_Gp} | ...]. (* <--- error *)

Но тогда я получаю сообщение об ошибке V_Gp (набор вершин нового графа) должен иметь тип finType вместо {set _}.Есть ли способ "конвертировать" V_Gp в finType?

...