0

我正在学习 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 本身来利用，并避免“edges_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 _} 的错误。有没有办法在 finType 中“转换” V_Gp？

4

0 回答 0