A bit of coq-proven alga
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
src
.gitignore
LICENSE
Makefile
Makefile.conf
README.md
_CoqProject

README.md

coq-alga

This repository contains some theory about algebraic graphs and prove a few theorems about homomorphisms in Coq.

The files in the src/ directory are organized as follow:

  • Graph.v is containing basic definitions, axioms and tools to use them with Coq.
  • Homomorphism.v is giving a definition and prove some theorems about structural homomorphism.
  • ReducedHomo.v is giving a definition and prove some theorems about a kind of homomorphism, preserving a graph equality relation.
  • SmartHomo.v is giving a definition and prove some theorems about a kind of reduced homomorphism.

A more precise analysis of these results is given at https://blog.nyarlathotep.one/2018/12/algebraic-graphs-homomorphisms/.