test(logics): checked examples for clause sets, parity, DNF, QBF and subformulas

ComplexityTests/CNF.lean

@@ -5,10 +5,14 @@ Authors: Samuel Schlesinger
 -/
 
 import Complexity.Logics.Propositional.CNF.ExactlyOne
+import Complexity.Logics.Propositional.CNF.Parity
+import Complexity.Logics.Propositional.ClauseSet.Basic
+import Complexity.Logics.Propositional.DNF
+import Complexity.Logics.Propositional.QBF
 import Complexity.Computability.Complexity.Problems.SAT
 
 /-!
-# Tests for formulas in conjunctive normal form and SAT
+# Tests for propositional normal forms, quantified Boolean formulas and SAT
 -/
 
 namespace ComplexityTests.CNF
@@ -37,4 +41,58 @@ example : (CNF.exactlyOne [0, 1, 2]).eval (fun v => v == 1) = true := by decide
 example : (CNF.exactlyOne [0, 1, 2]).eval (fun v => v != 0) = false := by decide
 example : (CNF.exactlyOne [0, 1, 2]).eval (fun _ => false) = false := by decide
 
+/-! ### Clause sets -/
+
+/-- `φ` and its clause set have the same solutions; its satisfying assignment is one. -/
+example : φ.toClauseSet.Sat (fun _ => true) :=
+  (CNF.sat_toClauseSet_iff φ _).2 rfl
+
+example : ¬ φ.toClauseSet.Sat (fun v => v == 0) := by
+  rw [CNF.sat_toClauseSet_iff]
+  decide
+
+/-- Listing the clauses of a clause set gives a formula with the same solutions. -/
+example : φ.toClauseSet.toCNF.eval (fun _ => true) = true :=
+  (ClauseSet.eval_toCNF_eq_true_iff _ _).2 ((CNF.sat_toClauseSet_iff φ _).2 rfl)
+
+/-! ### Parity constraints -/
+
+/-- The parity of `x₀, x₁` is odd under `x₀ ↦ true, x₁ ↦ false`, so the constraint for odd parity
+holds and the one for even parity fails. -/
+example : (CNF.parityOnEq ({0, 1} : Finset ℕ) true).eval (fun v => v == 0) = true :=
+  (CNF.eval_parityOnEq_eq_true_iff _ _ _).2 (by decide)
+
+example : (CNF.parityOnEq ({0, 1} : Finset ℕ) false).eval (fun v => v == 0) = false := by
+  rw [Bool.eq_false_iff, ne_eq, CNF.eval_parityOnEq_eq_true_iff]
+  decide
+
+/-! ### Disjunctive normal form -/
+
+/-- `(x₀ ∧ ¬x₁) ∨ x₁`. -/
+def δ : DNF ℕ := [[(0, true), (1, false)], [(1, true)]]
+
+example : δ.eval (fun v => v == 0) = true := rfl
+example : δ.eval (fun _ => false) = false := rfl
+
+/-- Negating every literal turns `δ` into a formula in conjunctive normal form for `¬δ`. -/
+example : CNF.eval (fun _ => false) δ.negate = true := by
+  rw [DNF.eval_negate]
+  rfl
+
+/-! ### Quantified Boolean formulas -/
+
+/-- `∀ x₀, ∃ x₁, x₀ ↔ x₁` is closed and true. -/
+def θ : QBF ℕ :=
+  .all 0 (.ex 1 (.or (.and (.var 0) (.var 1)) (.and (.not (.var 0)) (.not (.var 1)))))
+
+example : θ.Closed := by decide
+example : θ.eval (fun _ => false) = true := by decide
+
+/-- `∃ x₀, x₀ ∧ ¬x₀` is closed and false. -/
+example : (QBF.ex 0 (.and (.var 0) (.not (.var 0)))).eval (fun _ => true) = false := by decide
+
+/-- A closed formula has the same value under every assignment. -/
+example (σ : ℕ → Bool) : θ.eval σ = true :=
+  (QBF.eval_eq_of_closed (by decide) σ (fun _ => false)).trans (by decide)
+
 end ComplexityTests.CNF

ComplexityTests/FirstOrderAutomation.lean

@@ -6,6 +6,7 @@ Authors: Samuel Schlesinger
 
 import Complexity.Logics.FirstOrder.Problems.SizedGraph
 import Complexity.Logics.FirstOrder.Projection.Graph
+import Complexity.Logics.FirstOrder.Subformula
 import Complexity.Tactic.FirstOrder
 
 /-!
@@ -15,7 +16,8 @@ Exercise `fo_qf`, `fo_simp` and `fo_reduction` on formulas, interpretations, pro
 reductions, including their documented failure modes: quantified formulas are not
 quantifier-free, bare relation constructors block `simp`, and a domain formula that may fail
 leaves the semantic goal about the interpreted structure. The classes of independent sets and
-cliques are shown nonvacuous and distinct on a two-vertex structure.
+cliques are shown nonvacuous and distinct on a two-vertex structure. The closure properties of
+`subformulas` are checked on the sentence saying that a graph has no loops.
 -/
 
 namespace ComplexityTests.FirstOrderAutomation
@@ -443,4 +445,25 @@ info: 'Cslib.Logic.FO.Projection.tupleModelEquiv' depends on axioms: [Quot.sound
 #print axioms Projection.tupleModelEquiv
 
 
+/-! ### Subformulas -/
+
+section Subformulas
+
+/-- `∀ x, ¬ x ~ x`: a graph has no loops. -/
+private def noLoops : Language.graph.Sentence := ∀' ∼(adj.boundedFormula₂ &0 &0)
+
+example : (subformulas noLoops).Finite := finite_subformulas _
+
+/-- The body of the quantifier, its atom and `⊥` are subformulas. -/
+example : ⟨1, ∼(adj.boundedFormula₂ &0 &0)⟩ ∈ subformulas noLoops :=
+  mem_subformulas_of_all (self_mem_subformulas _)
+
+example : ⟨1, adj.boundedFormula₂ &0 &0⟩ ∈ subformulas noLoops :=
+  mem_subformulas_of_imp_left (mem_subformulas_of_all (self_mem_subformulas _))
+
+example : ⟨1, ⊥⟩ ∈ subformulas noLoops :=
+  mem_subformulas_of_imp_right (mem_subformulas_of_all (self_mem_subformulas _))
+
+end Subformulas
+
 end ComplexityTests.FirstOrderAutomation