使用Coq的简单图论证明

Question

是否有一个完善的Coq图库用于证明简单定理？

我想学习如何证明简单的东西:"G1,G2是同构的,当且仅当它们的补语是同构的"时.

是否有相关/类似的示例或教程？

Answer 1

这是一个演示.

允许用等价关系重写.

Require Import Coq.Setoids.Setoid.

图是一组顶点以及邻接关系.

Definition graph : Type := {V : Type & V -> V -> bool}.

顶点和邻接的图形.

Definition create : forall V, (V -> V -> bool) -> graph := @existT _ _.

图中的顶点.

Definition vertices : graph -> Type := @projT1 _ _.

图表的邻接.

Definition adjacent : forall g1, vertices g1 -> vertices g1 -> bool := @projT2 _ _.

图的补码具有相同的顶点,但是具有否定的邻接关系.

Definition complement : graph -> graph := fun g1 => create (vertices g1) (fun v1 v2 => negb (adjacent g1 v1 v2)).

标准的东西.

Definition injective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1 x2, f1 x1 = f1 x2 -> x1 = x2.

Definition surjective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1, exists x2, f1 x2 = x1.

Definition bijective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => injective f1 /\ surjective f1.

如果在它们的顶点之间存在保持邻接的双射,则两个图是同构的.

Definition isomorphic : graph -> graph -> Prop := fun g1 g2 => exists f1, bijective f1 /\ (forall x1 x2, adjacent g1 x1 x2 = adjacent g2 (f1 x1) (f1 x2)).

Infix "~" := isomorphic (at level 70).

一个有用的事实,我留给你的证据.

Conjecture C1 : forall b1 b2, negb b1 = negb b2 <-> b1 = b2.

你的事实.

Goal forall g1 g2, g1 ~ g2 <-> complement g1 ~ complement g2.
Proof.

访问图表的组件.

destruct g1.
destruct g2.

替代定义的定义.

unfold isomorphic, complement, adjacent, vertices, create, projT2, projT1.

一阶逻辑简化.

firstorder.

Instanciation.

exists x1.
firstorder.
rewrite C1.
firstorder.
exists x1.
firstorder.

Instanciation.

specialize (H0 x2 x3).
rewrite C1 in H0.
firstorder.
Qed.

实际上,这是图形的形式化,其邻接关系是可判定的V -> V -> bool.在直觉逻辑中,并非所有具有一般邻接关系的图V -> V -> Prop都具有您想要证明的属性.

您也可以转向经典逻辑或使用双重否定翻译,而不是坚持使用有限或其他可判定的图形.