From ac2a93d52a8a624dc46c029d263911d8fce96bb7 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 21:56:49 -0400 Subject: [PATCH] refactor(logics): move the QBF derived connectives into the QBF module Move the derived connectives of quantified Boolean formulas (`QBF.exs`, `alls`, `conj`, `imp`, `iff`, `lit`, `ofClause`, `ofCNF`) and their evaluation and free-variable lemmas from `Classes/Space/TQBF/Formula.lean` into `Logics/Propositional/QBF.lean`, where the type lives. Statements and proofs move unchanged, in the same namespace. `freeVars_alls` is public again, like `freeVars_exs`, because the midpoint formulas in the TQBF module use it across modules now. The tokens of the connectives, which depend on the TQBF encoding, stay in the TQBF module. The QBF module now imports the CNF module. Part of #596 (item 4). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Classes/Space/TQBF/Formula.lean | 190 +----------------- Complexity/Logics/Propositional/QBF.lean | 187 +++++++++++++++++ 2 files changed, 193 insertions(+), 184 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Space/TQBF/Formula.lean b/Complexity/Computability/Complexity/Classes/Space/TQBF/Formula.lean index bba134dad..1dce8e14f 100644 --- a/Complexity/Computability/Complexity/Classes/Space/TQBF/Formula.lean +++ b/Complexity/Computability/Complexity/Classes/Space/TQBF/Formula.lean @@ -33,26 +33,21 @@ gives a closed formula (`Cslib.Complexity.TQBF.savitchFormula`) whose value is free variables of the formula of level `0` lie in its two blocks (`Cslib.Complexity.TQBF.closed_savitchFormula`). -The formulas use derived connectives of `Cslib.Logic.PL.QBF`: blocks of quantifiers +The formulas use the derived connectives of `Cslib.Logic.PL.QBF`: blocks of quantifiers (`Cslib.Logic.PL.QBF.exs`, `Cslib.Logic.PL.QBF.alls`), conjunctions of lists -(`Cslib.Logic.PL.QBF.conj`, `top` for the empty list), implication, equivalence, literals, and -formulas in conjunctive normal form (`Cslib.Logic.PL.QBF.ofCNF`, `bot` for the empty clause). Their -tokens are given explicitly (`Cslib.Logic.PL.QBF.tokens_exs`, …), for the polynomial-time -construction of the formulas. +(`Cslib.Logic.PL.QBF.conj`), implication, equivalence, literals, and formulas in conjunctive normal +form (`Cslib.Logic.PL.QBF.ofCNF`). Their tokens are given here explicitly +(`Cslib.Logic.PL.QBF.tokens_exs`, …), for the polynomial-time construction of the formulas. ## Main definitions -* `Cslib.Logic.PL.QBF.exs`, `Cslib.Logic.PL.QBF.alls`, `Cslib.Logic.PL.QBF.conj`, - `Cslib.Logic.PL.QBF.imp`, `Cslib.Logic.PL.QBF.iff`, `Cslib.Logic.PL.QBF.lit`, - `Cslib.Logic.PL.QBF.ofCNF`: derived connectives. * `Cslib.Complexity.TQBF.blockVar`, `Cslib.Complexity.TQBF.blockVars`: the variables of the blocks. * `Cslib.Complexity.TQBF.midpoint`, `Cslib.Complexity.TQBF.savitchFormula`: the midpoint formulas. ## Main results -* `Cslib.Logic.PL.QBF.eval_exs_eq_true_iff`, `Cslib.Logic.PL.QBF.eval_alls_eq_true_iff`: blocks - of quantifiers range over the assignments that agree outside the block. -* `Cslib.Logic.PL.QBF.eval_ofCNF`: formulas in conjunctive normal form keep their value. +* `Cslib.Logic.PL.QBF.tokens_exs`, `Cslib.Logic.PL.QBF.tokens_alls`, + `Cslib.Logic.PL.QBF.tokens_ofCNF`, …: the tokens of the derived connectives. * `Cslib.Complexity.TQBF.eval_midpoint`, `Cslib.Complexity.TQBF.eval_savitchFormula`: the midpoint formulas express reachability by midpoints. * `Cslib.Complexity.TQBF.closed_savitchFormula`: they are closed. @@ -67,179 +62,6 @@ construction of the formulas. namespace Cslib.Logic.PL.QBF -/-! ### Derived connectives -/ - -variable {V : Type*} - -/-- Existential quantification over each variable of a list, the first one outermost. -/ -def exs (vs : List V) (φ : QBF V) : QBF V := vs.foldr ex φ - -/-- Universal quantification over each variable of a list, the first one outermost. -/ -def alls (vs : List V) (φ : QBF V) : QBF V := vs.foldr all φ - -/-- The conjunction of a list of formulas, `top` for the empty list. -/ -def conj (l : List (QBF V)) : QBF V := l.foldr and top - -/-- Implication. -/ -def imp (φ ψ : QBF V) : QBF V := or (not φ) ψ - -/-- Equivalence. -/ -def iff (φ ψ : QBF V) : QBF V := or (and φ ψ) (and (not φ) (not ψ)) - -/-- The literal of `v` with sign `b`: `v` itself for `true`, its negation for `false`. -/ -def lit (v : V) (b : Bool) : QBF V := if b then var v else not (var v) - -/-- A clause as the disjunction of its literals, `bot` for the empty clause. -/ -def ofClause (c : Clause V) : QBF V := c.foldr (fun l φ => or (lit l.1 l.2) φ) bot - -/-- A formula in conjunctive normal form as the conjunction of its clauses, `top` for the empty -formula. -/ -def ofCNF (φ : CNF V) : QBF V := φ.foldr (fun c ψ => and (ofClause c) ψ) top - -theorem exs_append (vs ws : List V) (φ : QBF V) : exs (vs ++ ws) φ = exs vs (exs ws φ) := - List.foldr_append - -theorem alls_append (vs ws : List V) (φ : QBF V) : alls (vs ++ ws) φ = alls vs (alls ws φ) := - List.foldr_append - -variable [DecidableEq V] (σ : V → Bool) - -/-- **A block of existential quantifiers** ranges over the assignments that agree with the given -one outside the block. -/ -theorem eval_exs_eq_true_iff (vs : List V) (φ : QBF V) : - (exs vs φ).eval σ = true ↔ ∃ τ, (∀ x ∉ vs, τ x = σ x) ∧ φ.eval τ = true := by - induction vs generalizing σ with - | nil => exact ⟨fun h => ⟨σ, fun _ _ => rfl, h⟩, fun ⟨τ, hτ, h⟩ => - (funext fun x => hτ x (List.not_mem_nil)) ▸ h⟩ - | cons v vs ih => - simp only [exs, List.foldr_cons] at ih ⊢ - rw [eval_ex_eq_true_iff] - constructor - · rintro ⟨b, hb⟩ - obtain ⟨τ, hτ, h⟩ := (ih _).mp hb - refine ⟨τ, fun x hx => ?_, h⟩ - rw [hτ x fun h => hx (List.mem_cons_of_mem _ h), - Function.update_of_ne fun h => hx (by simp [h])] - · rintro ⟨τ, hτ, h⟩ - refine ⟨τ v, (ih _).mpr ⟨τ, fun x hx => ?_, h⟩⟩ - by_cases hxv : x = v - · subst hxv - simp - · rw [Function.update_of_ne hxv] - exact hτ x (by simp [hxv, hx]) - -/-- **A block of universal quantifiers** ranges over the assignments that agree with the given one -outside the block. -/ -theorem eval_alls_eq_true_iff (vs : List V) (φ : QBF V) : - (alls vs φ).eval σ = true ↔ ∀ τ, (∀ x ∉ vs, τ x = σ x) → φ.eval τ = true := by - induction vs generalizing σ with - | nil => exact ⟨fun h τ hτ => (funext fun x => hτ x (List.not_mem_nil)) ▸ h, - fun h => h σ fun _ _ => rfl⟩ - | cons v vs ih => - simp only [alls, List.foldr_cons] at ih ⊢ - rw [eval_all_eq_true_iff] - constructor - · intro h τ hτ - refine (ih _).mp (h (τ v)) τ fun x hx => ?_ - by_cases hxv : x = v - · subst hxv - simp - · rw [Function.update_of_ne hxv] - exact hτ x (by simp [hxv, hx]) - · intro h b - refine (ih _).mpr fun τ hτ => h τ fun x hx => ?_ - rw [hτ x fun h => hx (List.mem_cons_of_mem _ h), - Function.update_of_ne fun h => hx (by simp [h])] - -@[simp] theorem eval_conj (l : List (QBF V)) : (conj l).eval σ = l.all (·.eval σ) := by - induction l with - | nil => rfl - | cons φ l ih => - change (φ.and (conj l)).eval σ = _ - simp [ih] - -@[simp] theorem eval_imp (φ ψ : QBF V) : (imp φ ψ).eval σ = (!φ.eval σ || ψ.eval σ) := rfl - -@[simp] theorem eval_iff (φ ψ : QBF V) : (iff φ ψ).eval σ = (φ.eval σ == ψ.eval σ) := by - simp only [iff, eval_or, eval_and, eval_not] - cases φ.eval σ <;> cases ψ.eval σ <;> rfl - -@[simp] theorem eval_lit (v : V) (b : Bool) : (lit v b).eval σ = (σ v == b) := by - cases b <;> simp only [lit, eval_var, eval_not, Bool.false_eq_true, ite_false, ite_true] <;> - cases σ v <;> rfl - -@[simp] theorem eval_ofClause (c : Clause V) : (ofClause c).eval σ = Clause.eval σ c := by - induction c with - | nil => rfl - | cons l c ih => - change ((lit l.1 l.2).or (ofClause c)).eval σ = _ - simp [ih, Literal.eval] - -/-- **A formula in conjunctive normal form keeps its value.** -/ -@[simp] theorem eval_ofCNF (φ : CNF V) : (ofCNF φ).eval σ = CNF.eval σ φ := by - induction φ with - | nil => rfl - | cons c φ ih => - change ((ofClause c).and (ofCNF φ)).eval σ = _ - simp [ih] - -/-! ### Free variables of the derived connectives -/ - -theorem freeVars_exs (vs : List V) (φ : QBF V) : - (exs vs φ).freeVars = φ.freeVars \ vs.toFinset := by - induction vs with - | nil => simp [exs] - | cons v vs ih => - simp only [exs, List.foldr_cons] at ih ⊢ - rw [freeVars_ex, ih, List.toFinset_cons] - ext x - simp only [Finset.mem_erase, Finset.mem_sdiff, Finset.mem_insert] - tauto - -private theorem freeVars_alls (vs : List V) (φ : QBF V) : - (alls vs φ).freeVars = φ.freeVars \ vs.toFinset := by - induction vs with - | nil => simp [alls] - | cons v vs ih => - simp only [alls, List.foldr_cons] at ih ⊢ - rw [freeVars_all, ih, List.toFinset_cons] - ext x - simp only [Finset.mem_erase, Finset.mem_sdiff, Finset.mem_insert] - tauto - -theorem mem_freeVars_conj {l : List (QBF V)} {x : V} : - x ∈ (conj l).freeVars ↔ ∃ φ ∈ l, x ∈ φ.freeVars := by - induction l with - | nil => simp [conj] - | cons φ l ih => - change x ∈ (φ.and (conj l)).freeVars ↔ _ - simp [ih] - -@[simp] theorem freeVars_imp (φ ψ : QBF V) : (imp φ ψ).freeVars = φ.freeVars ∪ ψ.freeVars := rfl - -@[simp] theorem freeVars_iff (φ ψ : QBF V) : (iff φ ψ).freeVars = φ.freeVars ∪ ψ.freeVars := by - ext x - simp only [iff, freeVars_or, freeVars_and, freeVars_not, Finset.mem_union] - tauto - -@[simp] theorem freeVars_lit (v : V) (b : Bool) : (lit v b).freeVars = {v} := by - cases b <;> rfl - -theorem mem_freeVars_ofCNF {x : V} {φ : CNF V} : x ∈ (ofCNF φ).freeVars ↔ x ∈ φ.vars := by - have hc (c : Clause V) : x ∈ (ofClause c).freeVars ↔ ∃ l ∈ c, l.1 = x := by - induction c with - | nil => simp [ofClause] - | cons l c ih => - change x ∈ ((lit l.1 l.2).or (ofClause c)).freeVars ↔ _ - rw [freeVars_or, Finset.mem_union, ih, freeVars_lit, Finset.mem_singleton] - simp [eq_comm] - induction φ with - | nil => simp [ofCNF, CNF.vars] - | cons c φ ih => - change x ∈ ((ofClause c).and (ofCNF φ)).freeVars ↔ _ - simp only [freeVars_and, Finset.mem_union, ih, hc] - simp [CNF.vars] - /-! ### Tokens of the derived connectives -/ theorem tokens_exs (vs : List ℕ) (φ : QBF ℕ) : diff --git a/Complexity/Logics/Propositional/QBF.lean b/Complexity/Logics/Propositional/QBF.lean index 7ef385746..2c794b1a1 100644 --- a/Complexity/Logics/Propositional/QBF.lean +++ b/Complexity/Logics/Propositional/QBF.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Init +public import Complexity.Logics.Propositional.CNF public import Mathlib.Data.Finset.Basic import Mathlib.Data.Finset.Lattice.Lemmas @@ -35,6 +36,11 @@ than an evaluated one, so it is not reused. * `Cslib.Logic.PL.QBF.freeVars`, `Cslib.Logic.PL.QBF.Closed`. * `Cslib.Logic.PL.QBF.vars`, `Cslib.Logic.PL.QBF.size`: the variables, free or bound, and the number of nodes. +* `Cslib.Logic.PL.QBF.exs`, `Cslib.Logic.PL.QBF.alls`, `Cslib.Logic.PL.QBF.conj`, + `Cslib.Logic.PL.QBF.imp`, `Cslib.Logic.PL.QBF.iff`, `Cslib.Logic.PL.QBF.lit`: derived + connectives, blocks of quantifiers and conjunctions of lists. +* `Cslib.Logic.PL.QBF.ofClause`, `Cslib.Logic.PL.QBF.ofCNF`: clauses and formulas in conjunctive + normal form as quantified Boolean formulas. ## Main results @@ -45,6 +51,10 @@ than an evaluated one, so it is not reused. assignment. * `Cslib.Logic.PL.QBF.eval_not_ex`, `Cslib.Logic.PL.QBF.eval_not_all`: De Morgan's laws for the quantifiers. +* `Cslib.Logic.PL.QBF.eval_exs_eq_true_iff`, `Cslib.Logic.PL.QBF.eval_alls_eq_true_iff`: blocks + of quantifiers range over the assignments that agree outside the block. +* `Cslib.Logic.PL.QBF.eval_ofCNF`, `Cslib.Logic.PL.QBF.mem_freeVars_ofCNF`: formulas in + conjunctive normal form keep their value and their variables. ## References @@ -265,4 +275,181 @@ theorem closed_or : (φ.or ψ).Closed ↔ φ.Closed ∧ ψ.Closed := Finset.unio end QBF +namespace QBF + +/-! ### Derived connectives -/ + +variable {V : Type*} + +/-- Existential quantification over each variable of a list, the first one outermost. -/ +def exs (vs : List V) (φ : QBF V) : QBF V := vs.foldr ex φ + +/-- Universal quantification over each variable of a list, the first one outermost. -/ +def alls (vs : List V) (φ : QBF V) : QBF V := vs.foldr all φ + +/-- The conjunction of a list of formulas, `top` for the empty list. -/ +def conj (l : List (QBF V)) : QBF V := l.foldr and top + +/-- Implication. -/ +def imp (φ ψ : QBF V) : QBF V := or (not φ) ψ + +/-- Equivalence. -/ +def iff (φ ψ : QBF V) : QBF V := or (and φ ψ) (and (not φ) (not ψ)) + +/-- The literal of `v` with sign `b`: `v` itself for `true`, its negation for `false`. -/ +def lit (v : V) (b : Bool) : QBF V := if b then var v else not (var v) + +/-- A clause as the disjunction of its literals, `bot` for the empty clause. -/ +def ofClause (c : Clause V) : QBF V := c.foldr (fun l φ => or (lit l.1 l.2) φ) bot + +/-- A formula in conjunctive normal form as the conjunction of its clauses, `top` for the empty +formula. -/ +def ofCNF (φ : CNF V) : QBF V := φ.foldr (fun c ψ => and (ofClause c) ψ) top + +theorem exs_append (vs ws : List V) (φ : QBF V) : exs (vs ++ ws) φ = exs vs (exs ws φ) := + List.foldr_append + +theorem alls_append (vs ws : List V) (φ : QBF V) : alls (vs ++ ws) φ = alls vs (alls ws φ) := + List.foldr_append + +variable [DecidableEq V] (σ : V → Bool) + +/-- **A block of existential quantifiers** ranges over the assignments that agree with the given +one outside the block. -/ +theorem eval_exs_eq_true_iff (vs : List V) (φ : QBF V) : + (exs vs φ).eval σ = true ↔ ∃ τ, (∀ x ∉ vs, τ x = σ x) ∧ φ.eval τ = true := by + induction vs generalizing σ with + | nil => exact ⟨fun h => ⟨σ, fun _ _ => rfl, h⟩, fun ⟨τ, hτ, h⟩ => + (funext fun x => hτ x (List.not_mem_nil)) ▸ h⟩ + | cons v vs ih => + simp only [exs, List.foldr_cons] at ih ⊢ + rw [eval_ex_eq_true_iff] + constructor + · rintro ⟨b, hb⟩ + obtain ⟨τ, hτ, h⟩ := (ih _).mp hb + refine ⟨τ, fun x hx => ?_, h⟩ + rw [hτ x fun h => hx (List.mem_cons_of_mem _ h), + Function.update_of_ne fun h => hx (by simp [h])] + · rintro ⟨τ, hτ, h⟩ + refine ⟨τ v, (ih _).mpr ⟨τ, fun x hx => ?_, h⟩⟩ + by_cases hxv : x = v + · subst hxv + simp + · rw [Function.update_of_ne hxv] + exact hτ x (by simp [hxv, hx]) + +/-- **A block of universal quantifiers** ranges over the assignments that agree with the given one +outside the block. -/ +theorem eval_alls_eq_true_iff (vs : List V) (φ : QBF V) : + (alls vs φ).eval σ = true ↔ ∀ τ, (∀ x ∉ vs, τ x = σ x) → φ.eval τ = true := by + induction vs generalizing σ with + | nil => exact ⟨fun h τ hτ => (funext fun x => hτ x (List.not_mem_nil)) ▸ h, + fun h => h σ fun _ _ => rfl⟩ + | cons v vs ih => + simp only [alls, List.foldr_cons] at ih ⊢ + rw [eval_all_eq_true_iff] + constructor + · intro h τ hτ + refine (ih _).mp (h (τ v)) τ fun x hx => ?_ + by_cases hxv : x = v + · subst hxv + simp + · rw [Function.update_of_ne hxv] + exact hτ x (by simp [hxv, hx]) + · intro h b + refine (ih _).mpr fun τ hτ => h τ fun x hx => ?_ + rw [hτ x fun h => hx (List.mem_cons_of_mem _ h), + Function.update_of_ne fun h => hx (by simp [h])] + +@[simp] theorem eval_conj (l : List (QBF V)) : (conj l).eval σ = l.all (·.eval σ) := by + induction l with + | nil => rfl + | cons φ l ih => + change (φ.and (conj l)).eval σ = _ + simp [ih] + +@[simp] theorem eval_imp (φ ψ : QBF V) : (imp φ ψ).eval σ = (!φ.eval σ || ψ.eval σ) := rfl + +@[simp] theorem eval_iff (φ ψ : QBF V) : (iff φ ψ).eval σ = (φ.eval σ == ψ.eval σ) := by + simp only [iff, eval_or, eval_and, eval_not] + cases φ.eval σ <;> cases ψ.eval σ <;> rfl + +@[simp] theorem eval_lit (v : V) (b : Bool) : (lit v b).eval σ = (σ v == b) := by + cases b <;> simp only [lit, eval_var, eval_not, Bool.false_eq_true, ite_false, ite_true] <;> + cases σ v <;> rfl + +@[simp] theorem eval_ofClause (c : Clause V) : (ofClause c).eval σ = Clause.eval σ c := by + induction c with + | nil => rfl + | cons l c ih => + change ((lit l.1 l.2).or (ofClause c)).eval σ = _ + simp [ih, Literal.eval] + +/-- **A formula in conjunctive normal form keeps its value.** -/ +@[simp] theorem eval_ofCNF (φ : CNF V) : (ofCNF φ).eval σ = CNF.eval σ φ := by + induction φ with + | nil => rfl + | cons c φ ih => + change ((ofClause c).and (ofCNF φ)).eval σ = _ + simp [ih] + +/-! ### Free variables of the derived connectives -/ + +theorem freeVars_exs (vs : List V) (φ : QBF V) : + (exs vs φ).freeVars = φ.freeVars \ vs.toFinset := by + induction vs with + | nil => simp [exs] + | cons v vs ih => + simp only [exs, List.foldr_cons] at ih ⊢ + rw [freeVars_ex, ih, List.toFinset_cons] + ext x + simp only [Finset.mem_erase, Finset.mem_sdiff, Finset.mem_insert] + tauto + +theorem freeVars_alls (vs : List V) (φ : QBF V) : + (alls vs φ).freeVars = φ.freeVars \ vs.toFinset := by + induction vs with + | nil => simp [alls] + | cons v vs ih => + simp only [alls, List.foldr_cons] at ih ⊢ + rw [freeVars_all, ih, List.toFinset_cons] + ext x + simp only [Finset.mem_erase, Finset.mem_sdiff, Finset.mem_insert] + tauto + +theorem mem_freeVars_conj {l : List (QBF V)} {x : V} : + x ∈ (conj l).freeVars ↔ ∃ φ ∈ l, x ∈ φ.freeVars := by + induction l with + | nil => simp [conj] + | cons φ l ih => + change x ∈ (φ.and (conj l)).freeVars ↔ _ + simp [ih] + +@[simp] theorem freeVars_imp (φ ψ : QBF V) : (imp φ ψ).freeVars = φ.freeVars ∪ ψ.freeVars := rfl + +@[simp] theorem freeVars_iff (φ ψ : QBF V) : (iff φ ψ).freeVars = φ.freeVars ∪ ψ.freeVars := by + ext x + simp only [iff, freeVars_or, freeVars_and, freeVars_not, Finset.mem_union] + tauto + +@[simp] theorem freeVars_lit (v : V) (b : Bool) : (lit v b).freeVars = {v} := by + cases b <;> rfl + +theorem mem_freeVars_ofCNF {x : V} {φ : CNF V} : x ∈ (ofCNF φ).freeVars ↔ x ∈ φ.vars := by + have hc (c : Clause V) : x ∈ (ofClause c).freeVars ↔ ∃ l ∈ c, l.1 = x := by + induction c with + | nil => simp [ofClause] + | cons l c ih => + change x ∈ ((lit l.1 l.2).or (ofClause c)).freeVars ↔ _ + rw [freeVars_or, Finset.mem_union, ih, freeVars_lit, Finset.mem_singleton] + simp [eq_comm] + induction φ with + | nil => simp [ofCNF, CNF.vars] + | cons c φ ih => + change x ∈ ((ofClause c).and (ofCNF φ)).freeVars ↔ _ + simp only [freeVars_and, Finset.mem_union, ih, hc] + simp [CNF.vars] + +end QBF + end Cslib.Logic.PL