Domination Chain with Weighted Parameters (Coq files)

This code contains a formal description of basic facts about Graph Theory and Domination Theory in the language Coq/Ssreflect.

It is called DomTheory and consists of:
*) The proof that the sum of degrees equals the cardinal of the edge set.
*) Definitions and results about open and closed neighborhoods, stable sets, dominating sets, irredundant sets, hereditary and superhereditary properties, maximal/minimal sets and sets of maximum/minimum weight.
*) The (weighted version of the) Cockayne-Hedetniemi domination chain.
*) Examples of proofs with domination parameters on complete graphs.

This code also contains:
*) A browsable version made with the tool CoqDocJS, with some ''pretty-print'' symbols (like empty set, summation and set comprehension) added later.
*) A solver that computes the (unweighted and weighted versions of) parameters gamma, ii, alpha, Gamma and IR.
*) (experimental) The solver also generates a Coq file with a proof of alpha(G) >= k, where k is the size of the best stable set found during the optimization.
*) A set of instances.