The positive CNF game
Lax783278.PositiveCNF · concepts/Lax783278/PositiveCNF.lean · lax-783278
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural 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, is the set of unassigned variables and the set already assigned true.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Data.Finset.Card |
| 2 | import Mathlib.Data.Fintype.Basic |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: The positive CNF game |
| 7 | type: definition |
| 8 | --- |
| 9 | A positive CNF formula is a list of clauses, each a set of variables. |
| 10 | True and False alternately choose an unassigned variable, assigning it |
| 11 | their own truth value. True starts and wins exactly when each clause |
| 12 | contains a variable assigned true. Empty clauses and unused variables are |
| 13 | allowed. At an intermediate position, `U` is the set of unassigned |
| 14 | variables and `T` the set already assigned true. |
| 15 | -/ |
| 16 | |
| 17 | namespace Lax783278.PositiveCNF |
| 18 | |
| 19 | /-- A conjunction of clauses, each a disjunction of positive variables. -/ |
| 20 | structure Formula where |
| 21 | /-- Number of variables, labeled from zero. -/ |
| 22 | nvars : ℕ |
| 23 | /-- The clauses; an empty clause makes the formula unsatisfiable. -/ |
| 24 | clauses : List (Finset (Fin nvars)) |
| 25 | |
| 26 | /-- Every clause contains a variable belonging to the true set `T`. -/ |
| 27 | def Satisfied (φ : Formula) (T : Finset (Fin φ.nvars)) : Prop := |
| 28 | ∀ C ∈ φ.clauses, ∃ x ∈ C, x ∈ T |
| 29 | |
| 30 | /-- Evaluate the game for a specified number of remaining rounds. |
| 31 | At a True turn some choice must win; at a False turn every choice must win. |
| 32 | A completed assignment is evaluated by the formula's satisfaction rule. -/ |
| 33 | def TrueWinsAfter (φ : Formula) : ℕ → Finset (Fin φ.nvars) → |
| 34 | Finset (Fin φ.nvars) → Bool → Prop |
| 35 | | 0, _, T, _ => Satisfied φ T |
| 36 | | rounds + 1, U, T, trueTurn => |
| 37 | if U = ∅ then Satisfied φ T |
| 38 | else if trueTurn then |
| 39 | ∃ x ∈ U, TrueWinsAfter φ rounds (U.erase x) (insert x T) false |
| 40 | else |
| 41 | ∀ x ∈ U, TrueWinsAfter φ rounds (U.erase x) T true |
| 42 | |
| 43 | /-- Whether True can force satisfaction. Exactly `U.card` assignments remain, |
| 44 | so that many rounds suffice to evaluate every possible continuation. -/ |
| 45 | def TrueWins (φ : Formula) (U T : Finset (Fin φ.nvars)) (trueTurn : Bool) : Prop := |
| 46 | TrueWinsAfter φ U.card U T trueTurn |
| 47 | |
| 48 | /-- True wins the initial game, with every variable unassigned and True to move. -/ |
| 49 | def FirstWins (φ : Formula) : Prop := TrueWins φ Finset.univ ∅ true |
| 50 | |
| 51 | end Lax783278.PositiveCNF |
| 52 |
Builds on
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments