coq - 使用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.

实例化。

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

实例化。

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

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

除了坚持使用有限的图或其他可确定的图，您还可以使用经典逻辑或使用双重否定转换。