Proste testy teorii grafów przy użyciu Coq

Question

Czy istnieje dobrze znana biblioteka graficzna Coq do udowodnienia prostych twierdzeń?

Chciałbym nauczyć się, jak udowodnić proste rzeczy takie jak: "G1, G2 są izomorficzne wtedy i tylko wtedy, gdy ich dopełnienia są izomorficzne".

Czy są dostępne podobne/podobne przykłady lub samouczki?

Answer 1

Oto demonstracja.

Umożliwia przepisywanie z uwzględnieniem relacji równoważności.

Require Import Coq.Setoids.Setoid. 

Wykres jest zbiorem wierzchołków wraz z relacją sąsiedztwa.

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

Wykres z wierzchołków i przyległości.

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

Wierzchołki z wykresu.

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

Adjacency od wykresu.

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

Uzupełnienie wykresu ma te same wierzchołki, ale zrównaną relację sąsiedztwa.

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

Standardowe rzeczy.

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. 

dwa wykresy są izomorficzne, jeśli istnieje bijection między ich wierzchołków, który zachowuje przylegania.

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). 

Pomocny fakt, którego dowód zostawiam Tobie.

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

Twój fakt.

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

Dostęp do komponentów wykresów.

destruct g1. 
destruct g2. 

Substytut zdefiniowany z definicji.

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

Uproszczenia logiczne pierwszego rzędu.

firstorder. 

Instanciation.

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

Instanciation.

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

Właściwie to formalizacja wykresach którego relacja sąsiedztwa jest rozstrzygalne V -> V -> bool. W logice intuicjonistycznej nie wszystkie wykresy o ogólnej relacji sąsiedztwa mają wartość, którą chcesz udowodnić.

Zamiast trzymać się skończonych lub w inny sposób rozstrzygających wykresów, można również przejść do klasycznej logiki lub użyć tłumaczenia podwójnej negacji.