Lax Lean Archive

The positive CNF game

Lax689614.PositiveCNF · concepts/Lax689614/PositiveCNF.lean · lax-689614

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

    A positive CNF formula is a list of clauses, each a set of variables. True and False alternately choose an unassigned variable, assigning it their own truth value. True starts and wins exactly when each clause contains a variable assigned true. Empty clauses and unused variables are allowed. At an intermediate position, UU is the set of unassigned variables and TT the set already assigned true.

    Concept map
    1 concept; 8 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Data.Finset.Card
    2import Mathlib.Data.Fintype.Basic
    3
    4/-!
    5---
    6title: The positive CNF game
    7type: definition
    8---
    9A positive CNF formula is a list of clauses, each a set of variables.
    10True and False alternately choose an unassigned variable, assigning it
    11their own truth value. True starts and wins exactly when each clause
    12contains a variable assigned true. Empty clauses and unused variables are
    13allowed. At an intermediate position, `U` is the set of unassigned
    14variables and `T` the set already assigned true.
    15-/
    16
    17namespace Lax689614.PositiveCNF
    18
    19structure Formula where
    20 nvars : ℕ
    21 clauses : List (Finset (Fin nvars))
    22
    23def Satisfied (φ : Formula) (T : Finset (Fin φ.nvars)) : Prop :=
    24 ∀ C ∈ φ.clauses, ∃ x ∈ C, x ∈ T
    25
    26/-- Whether True can force satisfaction from the specified position and turn. -/
    27def TrueWins (φ : Formula) (U T : Finset (Fin φ.nvars)) (trueTurn : Bool) : Prop :=
    28 if U = ∅ then Satisfied φ T
    29 else if trueTurn then
    30 ∃ x : U, TrueWins φ (U.erase x.val) (insert x.val T) false
    31 else
    32 ∀ x : U, TrueWins φ (U.erase x.val) T true
    33termination_by U.card
    34decreasing_by all_goals exact Finset.card_erase_lt_of_mem x.property
    35
    36def FirstWins (φ : Formula) : Prop := TrueWins φ Finset.univ ∅ true
    37
    38end Lax689614.PositiveCNF
    39
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…