Counting all independent sets, vertex covers, and 3-colorings
Lax859101.CountingAllSets · concepts/Lax859101/CountingAllSets.lean · lax-859101
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
On a graph, counting all independent sets counts the sets of vertices without an edge between two of their elements, and counting all vertex covers the sets of vertices meeting every edge, whatever their size. #3-Colorability counts the proper colorings with three colors.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Data.Set.Card |
| 2 | import Mathlib.Algebra.BigOperators.Ring.Finset |
| 3 | import Mathlib.Algebra.Order.BigOperators.Group.Finset |
| 4 | import Mathlib.Data.Fintype.BigOperators |
| 5 | import Mathlib.SetTheory.Cardinal.Finite |
| 6 | import Mathlib.Algebra.Group.Action.Defs |
| 7 | import Mathlib.Tactic.Ring |
| 8 | import Mathlib.ModelTheory.Graph |
| 9 | import Mathlib.Order.PiLex |
| 10 | import Mathlib.Data.Prod.Lex |
| 11 | import Mathlib.Data.Fintype.EquivFin |
| 12 | import Mathlib.ModelTheory.Order |
| 13 | import Mathlib.ModelTheory.Semantics |
| 14 | import Mathlib.ModelTheory.Complexity |
| 15 | import Mathlib.Tactic.FinCases |
| 16 | import Mathlib.Logic.Equiv.Fin.Basic |
| 17 | import Mathlib.Data.Fintype.Lattice |
| 18 | import Mathlib.Data.Finite.Sigma |
| 19 | import Mathlib.Order.Lattice.Nat |
| 20 | import Mathlib.Data.Fintype.Pigeonhole |
| 21 | import Mathlib.Dynamics.FixedPoints.Basic |
| 22 | import Mathlib.ModelTheory.Syntax |
| 23 | import Mathlib.Data.Fintype.Card |
| 24 | import Mathlib.Logic.Equiv.Prod |
| 25 | import Mathlib.Data.Set.Finite.Lemmas |
| 26 | import Mathlib.Data.Fintype.Sort |
| 27 | import Mathlib.Order.Hom.Set |
| 28 | import Lax366625.CountingProblems |
| 29 | |
| 30 | /-! |
| 31 | --- |
| 32 | title: Counting all independent sets, vertex covers, and 3-colorings |
| 33 | type: definition |
| 34 | --- |
| 35 | On a graph, counting all independent sets counts the sets of vertices |
| 36 | without an edge between two of their elements, and counting all vertex |
| 37 | covers the sets of vertices meeting every edge, whatever their size. |
| 38 | #3-Colorability counts the proper colorings with three colors. |
| 39 | -/ |
| 40 | |
| 41 | namespace Lax859101.CountingAllSets |
| 42 | |
| 43 | /-- The set `S` is independent for `Adj`: no two distinct elements of it are |
| 44 | related. -/ |
| 45 | def IndepSet {T : Type} (Adj : T → T → Prop) (S : T → Prop) : Prop := |
| 46 | ∀ x y, S x → S y → x ≠ y → ¬Adj x y |
| 47 | |
| 48 | open FirstOrder |
| 49 | |
| 50 | open Language Structure |
| 51 | |
| 52 | section Graph |
| 53 | |
| 54 | variable {A : Type} [Language.graph.Structure A] |
| 55 | |
| 56 | /-- A **vertex cover**: every edge has an end in it. -/ |
| 57 | def GVertexCover (A : Type) [Language.graph.Structure A] (C : A → Prop) : Prop := |
| 58 | ∀ x y : A, x ≠ y → RelMap Language.adj ![x, y] → C x ∨ C y |
| 59 | |
| 60 | end Graph |
| 61 | |
| 62 | open Lax366625.CountingProblems |
| 63 | |
| 64 | /-- **#3-Colorability**, as a counting problem. -/ |
| 65 | noncomputable def SharpThreeCol : CountingProblem FirstOrder.Language.graph := |
| 66 | CountingProblem.ofFun fun A _ => |
| 67 | Nat.card {χ : A → Fin 3 // ∀ x y : A, RelMap Language.adj ![x, y] → χ x ≠ χ y} |
| 68 | |
| 69 | /-- **Counting all independent sets**, as a counting problem. -/ |
| 70 | noncomputable def SharpAllIndependentSets : CountingProblem FirstOrder.Language.graph := |
| 71 | CountingProblem.ofFun fun A _ => |
| 72 | Nat.card {S : A → Prop // IndepSet (fun x y : A => RelMap Language.adj ![x, y]) S} |
| 73 | |
| 74 | /-- **Counting all vertex covers**, as a counting problem. -/ |
| 75 | noncomputable def SharpAllVertexCovers : CountingProblem FirstOrder.Language.graph := |
| 76 | CountingProblem.ofFun fun A _ => |
| 77 | Nat.card {C : A → Prop // GVertexCover A C} |
| 78 | |
| 79 | end Lax859101.CountingAllSets |
| 80 |
Builds on
Used by
Lax859101.AllSetsCompleteLax859101.AllSetsValuesLax859101.BipartiteCompleteLax859101.BipartiteValuesLax859101.ColoringCompleteLax859101.DnfCompleteLax859101.DnfValuesLax859101.NaeSatCompleteLax859101.NaeSatValuesLax859101.OneCallClosureLax859101.RestrictedSatCompleteLax859101.RestrictedSatValuesLax859101.SubtractiveClosure
From Mathlib
Mathlib.Algebra.BigOperators.Ring.FinsetMathlib.Algebra.Group.Action.DefsMathlib.Algebra.Order.BigOperators.Group.FinsetMathlib.Data.Finite.SigmaMathlib.Data.Fintype.BigOperatorsMathlib.Data.Fintype.CardMathlib.Data.Fintype.EquivFinMathlib.Data.Fintype.LatticeMathlib.Data.Fintype.PigeonholeMathlib.Data.Fintype.SortMathlib.Data.Prod.LexMathlib.Data.Set.CardMathlib.Data.Set.Finite.LemmasMathlib.Dynamics.FixedPoints.BasicMathlib.Logic.Equiv.Fin.BasicMathlib.Logic.Equiv.ProdMathlib.ModelTheory.ComplexityMathlib.ModelTheory.GraphMathlib.ModelTheory.OrderMathlib.ModelTheory.SemanticsMathlib.ModelTheory.SyntaxMathlib.Order.Hom.SetMathlib.Order.Lattice.NatMathlib.Order.PiLexMathlib.SetTheory.Cardinal.FiniteMathlib.Tactic.FinCasesMathlib.Tactic.Ring
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments