Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Counting exact covers, packings, set covers, and hitting sets

Lax280166.CountingSetFamilies · concepts/Lax280166/CountingSetFamilies.lean · lax-280166

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The instances are set systems: a universe of elements, a family of sets, and a membership relation, with a marked threshold where a size is asked. #Exact Cover counts the subfamilies covering every element exactly once. #Set Packing counts the subfamilies of pairwise disjoint sets of exactly the threshold size, #Set Cover the covering subfamilies of exactly the threshold size, and #Hitting Set the sets of elements of exactly the threshold size meeting every set of the family.

    Concept map
    9 concepts; 25 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Tactic.FinCases
    2import Mathlib.Order.PiLex
    3import Mathlib.Data.Prod.Lex
    4import Mathlib.Data.Fintype.EquivFin
    5import Mathlib.ModelTheory.Order
    6import Mathlib.ModelTheory.Semantics
    7import Mathlib.ModelTheory.Complexity
    8import Mathlib.Logic.Equiv.Fin.Basic
    9import Mathlib.Data.Fintype.Lattice
    10import Mathlib.Data.Finite.Sigma
    11import Mathlib.Order.Lattice.Nat
    12import Mathlib.Data.Set.Card
    13import Mathlib.Data.Fintype.Pigeonhole
    14import Mathlib.Dynamics.FixedPoints.Basic
    15import Mathlib.ModelTheory.Syntax
    16import Mathlib.Algebra.Order.BigOperators.Group.Finset
    17import Mathlib.Data.Fintype.Card
    18import Mathlib.SetTheory.Cardinal.Finite
    19import Mathlib.Logic.Equiv.Prod
    20import Mathlib.Data.Set.Finite.Lemmas
    21import Mathlib.Data.Fintype.Sort
    22import Mathlib.Order.Hom.Set
    23import Lax799700.SetFamily
    24import Mathlib.SetTheory.Cardinal.Finite
    25import Lax366625.CountingProblems
    26
    27/-!
    28---
    29title: Counting exact covers, packings, set covers, and hitting sets
    30type: definition
    31---
    32The instances are set systems: a universe of elements, a family of sets, and
    33a membership relation, with a marked threshold where a size is asked.
    34#Exact Cover counts the subfamilies covering every element exactly once.
    35#Set Packing counts the subfamilies of pairwise disjoint sets of exactly the
    36threshold size, #Set Cover the covering subfamilies of exactly the threshold
    37size, and #Hitting Set the sets of elements of exactly the threshold size
    38meeting every set of the family.
    39-/
    40
    41namespace Lax280166.CountingSetFamilies
    42
    43open Lax799700.SetFamily
    44
    45open FirstOrder
    46
    47open Language Structure
    48
    49section Solutions
    50
    51variable (A : Type) [setSystem.Structure A]
    52
    53/-- The subfamily `G` is a packing with exactly as many sets as the marked set,
    54in a finite set system. -/
    55def PackingOfSize (G : A → Prop) : Prop :=
    56 Finite A ∧ (∀ s, G s → SSFam s) ∧
    57 (∀ s s', G s → G s' → s ≠ s' → ∀ x : A, SSElem x → ¬(SSMem x s ∧ SSMem x s')) ∧
    58 {s | G s}.ncard = {x : A | SSMarked x}.ncard
    59
    60end Solutions
    61
    62open FirstOrder
    63
    64open Language Structure
    65
    66section Generic
    67
    68variable {A B : Type}
    69
    70/-- The subfamily `G` of the `Fp`-sets covers every `Ep`-element and has
    71exactly as many members as the `Kp`-marked set. -/
    72def CoverFamOfSizeOn (Ep Fp : A → Prop) (Mp : A → A → Prop) (Kp : A → Prop)
    73 (G : A → Prop) : Prop :=
    74 (∀ s, G s → Fp s) ∧ (∀ x, Ep x → ∃ s, G s ∧ Mp x s) ∧
    75 {s | G s}.ncard = {x | Kp x}.ncard
    76
    77end Generic
    78
    79section Problems
    80
    81variable (A : Type) [setSystem.Structure A]
    82
    83/-- The subfamily `G` is a cover with exactly as many sets as the marked set,
    84in a finite set system. -/
    85def SetCoverOfSize (G : A → Prop) : Prop :=
    86 Finite A ∧ CoverFamOfSizeOn (fun x : A => SSElem x) (fun s => SSFam s)
    87 (fun x s => SSMem x s) (fun x => SSMarked x) G
    88
    89/-- The set `H` of ground elements is a hitting set with exactly as many
    90elements as the marked set, in a finite set system. -/
    91def HittingSetOfSize (H : A → Prop) : Prop :=
    92 Finite A ∧ CoverFamOfSizeOn (fun s : A => SSFam s) (fun x => SSElem x)
    93 (fun s x => SSMem x s) (fun x => SSMarked x) H
    94
    95end Problems
    96
    97open FirstOrder
    98
    99open Language Structure
    100
    101section Generic
    102
    103variable {A : Type}
    104
    105/-- The subfamily `G` is an exact cover: it consists of `Fp`-sets, covers every
    106`Ep`-element, and no element belongs to two distinct members. This is the body
    107of `ExactlyCoversOn`, named for the statements that are about a
    108particular cover and not only about the existence of one. -/
    109def ExactCoverBy (Ep Fp : A → Prop) (Mp : A → A → Prop) (G : A → Prop) : Prop :=
    110 (∀ s, G s → Fp s) ∧ (∀ x, Ep x → ∃ s, G s ∧ Mp x s) ∧
    111 ∀ s s', G s → G s' → s ≠ s' → ∀ x, Ep x → ¬(Mp x s ∧ Mp x s')
    112
    113end Generic
    114
    115open Lax366625.CountingProblems Lax799700.SetFamily
    116
    117/-- **#Exact Cover**, as a counting problem. -/
    118noncomputable def SharpExactCover : CountingProblem Lax799700.SetFamily.setSystem :=
    119 CountingProblem.ofFun fun A _ =>
    120 Nat.card {G : A → Prop // ExactCoverBy (SSElem (A := A)) SSFam SSMem G}
    121
    122/-- **#Set Packing**, as a counting problem. -/
    123noncomputable def SharpSetPacking : CountingProblem Lax799700.SetFamily.setSystem :=
    124 CountingProblem.ofFun fun A _ =>
    125 Nat.card {G : A → Prop // PackingOfSize A G}
    126
    127/-- **#Set Cover**, as a counting problem. -/
    128noncomputable def SharpSetCover : CountingProblem Lax799700.SetFamily.setSystem :=
    129 CountingProblem.ofFun fun A _ =>
    130 Nat.card {G : A → Prop // SetCoverOfSize A G}
    131
    132/-- **#Hitting Set**, as a counting problem. -/
    133noncomputable def SharpHittingSet : CountingProblem Lax799700.SetFamily.setSystem :=
    134 CountingProblem.ofFun fun A _ =>
    135 Nat.card {H : A → Prop // HittingSetOfSize A H}
    136
    137end Lax280166.CountingSetFamilies
    138
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…