refactor(CNF): share count transport and guarded counting APIs

Complexity.lean

@@ -2133,6 +2133,7 @@ public import Complexity.Logics.Propositional.CNF.Gadgets
 public import Complexity.Logics.Propositional.CNF.ImplicationChain
 public import Complexity.Logics.Propositional.CNF.ImplicationCycle
 public import Complexity.Logics.Propositional.CNF.ModelCount
+public import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 public import Complexity.Logics.Propositional.CNF.Occurrence
 public import Complexity.Logics.Propositional.CNF.Parity
 public import Complexity.Logics.Propositional.CNF.Planar.Crossover

Complexity/Computability/Complexity/CookLevin/Parsimonious.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.SharpP
 public import Complexity.Computability.Complexity.CookLevin.Reduction
 public import Complexity.Logics.Propositional.CNF.ModelCount
+import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 
 /-!
 # The Cook–Levin reduction is parsimonious

Complexity/Computability/Complexity/Problems/CountingSAT.lean

@@ -17,6 +17,7 @@ import Complexity.Computability.Complexity.CookLevin.Counting
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Logics.Propositional.CNF.PolyTime
+import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 
 /-!
 # Complete problems for the counting classes

Complexity/Computability/Complexity/Problems/PlanarThreeSATThree.lean

@@ -149,7 +149,7 @@ theorem sharpThreeSATThree_toPlanarThreeSATThree (φ : CNF ℕ) :
     SharpThreeSATThree (toPlanarThreeSATThree φ) = SharpThreeSATThree φ := by
   have hout := (ThreeSATThree.syntaxCheck_iff (toPlanarThreeSATThree φ)).2
     ⟨width_toPlanarThreeSATThree φ, count_vars_toPlanarThreeSATThree φ⟩
-  simp only [SharpThreeSATThree, hout, ↓reduceIte]
+  simp only [SharpThreeSATThree, SharpSAT, hout, ↓reduceIte]
   by_cases hg : ThreeSATThree.syntaxCheck φ = true
   · have hs := (ThreeSATThree.syntaxCheck_iff φ).1 hg
     rw [modelCount_toPlanarThreeSATThree φ hs.1 hs.2]

Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCorrectness.lean

@@ -46,7 +46,7 @@ theorem crossing_axes_exist {φ : CNF ℕ}
           StraightThrough (occurrencePath φ t) p (0, 1) := by
   have hc := ((PlanarCompile.mem_crossingSites φ p).1 hp).2.2
   rw [← PlanarCompile.occurrencePaths_eq_paths] at hc
-  obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := List.exists_pair_indices_of_two_le_filter_contains _ p hc
+  obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := (List.two_le_filter_contains_iff _ p).1 hc
   have hi' : i < (Cslib.Logic.PL.occurrences φ).length := by
     simpa only [List.length_map] using hi
   have hj' : j < (Cslib.Logic.PL.occurrences φ).length := by

Complexity/Computability/Complexity/Problems/SAT/Planar/PathAssignments.lean

@@ -100,8 +100,7 @@ theorem occurrencePath_crossing_straight {φ : CNF ℕ}
   have hdeg : ∀ v, G.incidenceVertices.count v ≤ 3 := SAT.incidenceGraph_degree_le hw hv
   have hi := occurrence_index_lt ho
   obtain ⟨j, hj, hji, hpj⟩ := List.exists_other_index_of_two_le_filter_contains (paths φ) p
-    ((Cslib.Logic.PL.occurrences φ).idxOf o)
-    (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi) hsite.2.2
+    ((Cslib.Logic.PL.occurrences φ).idxOf o) hsite.2.2
   have hj' : j < G.2.length := by
     simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hj
   have hpi' : p ∈ G.unitPath ((Cslib.Logic.PL.occurrences φ).idxOf o) := by
@@ -181,10 +180,11 @@ theorem shared_ordinary_cell_center {φ : CNF ℕ}
   apply hp
   apply (mem_crossingSites φ p).2
   refine ⟨hcandidate, hc, ?_⟩
-  exact List.two_le_filter_contains_of_indices (paths φ) p
-    (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho)
-    (by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ht)
-    hij (path_mem_paths_get ho hpo) (path_mem_paths_get ht hpt)
+  exact (List.two_le_filter_contains_iff (paths φ) p).2
+    ⟨_, _,
+      by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ho,
+      by simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using occurrence_index_lt ht,
+      hij, path_mem_paths_get ho hpo, path_mem_paths_get ht hpt⟩
 
 /-- No retained wire cell is the clause-center endpoint removed by `dropLast`. -/
 theorem clause_center_not_mem_dropLast {φ : CNF ℕ} {o : Occurrence ℕ}

Complexity/Computability/Complexity/Problems/SAT/Planar/Paths/Occupancy.lean

@@ -43,7 +43,7 @@ theorem paths_filter_length_le_one {φ : CNF ℕ}
   by_contra h
   have ht : 2 ≤ ((paths φ).filter fun r => r.contains p).length := by omega
   obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ :=
-    List.exists_pair_indices_of_two_le_filter_contains (paths φ) p ht
+    (List.two_le_filter_contains_iff (paths φ) p).1 ht
   have hi' : i < (SAT.incidenceGraph φ).2.length := by
     simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi
   have hj' : j < (SAT.incidenceGraph φ).2.length := by

Complexity/Computability/Complexity/Problems/ThreeSATThree.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Complexity.Problems.ThreeSAT
 public import Complexity.Logics.Propositional.CNF.ThreeOccurrence
+import Complexity.Logics.Propositional.CNF.ModelCount.Relabel
 import Complexity.Logics.Propositional.CNF.ThreeOccurrence.PolyTime
 import Complexity.Computability.Complexity.Problems.SAT.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain

Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.Classes.SharpP.Completeness
+public import Complexity.Computability.Complexity.Problems.SharpSAT
 public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Size
 public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax
 
@@ -17,7 +18,7 @@ public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax
 The existing occurrence splitter preserves the number of satisfying assignments. Each source
 variable has one value on every copy in its implication cycle, and numbering copies is injective.
 The counting problems below count only occurring variables and return zero outside their syntax.
-They reuse `CNF.modelCount` and the existing syntax guards rather than introducing new assignment
+They reuse `SharpSAT` and the existing syntax guards rather than introducing new assignment
 or satisfiability semantics.
 
 ## Main definitions
@@ -28,12 +29,15 @@ or satisfiability semantics.
 ## Main results
 
 * `Cslib.Complexity.sharpThreeSATThree_toThreeSATThree`: exact counts for the total compiler.
+* `Cslib.Complexity.SharpThreeSAT.mem_ThreeSAT_iff`,
+  `Cslib.Complexity.SharpThreeSATThree.mem_ThreeSATThree_iff`: positivity recovers the languages.
 * `Cslib.Complexity.parsimoniousReducible_SharpThreeSAT_SharpThreeSATThree`: the existing
   polynomial-time compiler is a parsimonious reduction.
 
 ## References
 
-The occurrence construction and its source credit are documented in `ThreeSATThree`.
+The occurrence construction and its source credit are documented in `ThreeSATThree`. Its count
+preservation is an original elementary consequence of `CNF.copies_agree`.
 -/
 
 @[expose] public section
@@ -45,24 +49,43 @@ open Cslib.Logic.PL
 /-- Count satisfying assignments of width-at-most-three CNF; reject other syntax with count zero.
 Only variables occurring in the formula are counted. -/
 def SharpThreeSAT (φ : CNF ℕ) : ℕ :=
-  if φ.all (fun c => decide (c.length ≤ 3)) then φ.modelCount else 0
+  if φ.all (fun c => decide (c.length ≤ 3)) then SharpSAT φ else 0
 
 /-- Count satisfying assignments of width-three, occurrence-three CNF; reject other syntax with
 count zero. Repetitions are literal positions, as in `ThreeSATThree.syntaxCheck`. -/
 def SharpThreeSATThree (φ : CNF ℕ) : ℕ :=
-  if ThreeSATThree.syntaxCheck φ then φ.modelCount else 0
+  if ThreeSATThree.syntaxCheck φ then SharpSAT φ else 0
+
+/-- Membership in `ThreeSAT` is equivalent to a positive guarded model count. -/
+theorem SharpThreeSAT.mem_ThreeSAT_iff {φ : CNF ℕ} :
+    φ ∈ ThreeSAT ↔ 0 < SharpThreeSAT φ := by
+  simp only [ThreeSAT, Set.mem_ofPred_eq, SharpThreeSAT]
+  split <;> simp_all [List.all_eq_true, CNF.modelCount_pos_iff, SharpSAT]
+
+/-- Membership in `ThreeSATThree` is equivalent to a positive guarded model count. -/
+theorem SharpThreeSATThree.mem_ThreeSATThree_iff {φ : CNF ℕ} :
+    φ ∈ ThreeSATThree ↔ 0 < SharpThreeSATThree φ := by
+  by_cases hg : ThreeSATThree.syntaxCheck φ = true
+  · obtain ⟨hw, hv⟩ := (ThreeSATThree.syntaxCheck_iff φ).mp hg
+    simp only [ThreeSATThree, Set.mem_ofPred_eq, SharpThreeSATThree, hg, ↓reduceIte,
+      SharpSAT, CNF.modelCount_pos_iff]
+    exact ⟨fun h => h.2.2, fun hs => ⟨hw, hv, hs⟩⟩
+  · simp only [ThreeSATThree, Set.mem_ofPred_eq, SharpThreeSATThree, hg, Bool.false_eq_true,
+      ite_false, Nat.lt_irrefl, iff_false]
+    rintro ⟨hw, hv, _⟩
+    exact hg ((ThreeSATThree.syntaxCheck_iff φ).mpr ⟨hw, hv⟩)
 
 /-- The total occurrence compiler preserves the count, including rejected inputs. -/
 theorem sharpThreeSATThree_toThreeSATThree (φ : CNF ℕ) :
     SharpThreeSATThree (toThreeSATThree φ) = SharpThreeSAT φ := by
   have hout := (ThreeSATThree.syntaxCheck_iff (toThreeSATThree φ)).2
     ⟨width_toThreeSATThree φ, count_vars_toThreeSATThree_le φ⟩
-  simp only [SharpThreeSATThree, hout, ↓reduceIte]
+  simp only [SharpThreeSATThree, hout, ↓reduceIte, SharpSAT]
   by_cases hw : φ.all (fun c => decide (c.length ≤ 3)) = true
   · have hwidth : ∀ c ∈ φ, c.length ≤ 3 := by
       simpa only [List.all_eq_true, decide_eq_true_eq] using hw
     rw [modelCount_toThreeSATThree φ hwidth]
-    simp only [SharpThreeSAT, hw, ↓reduceIte]
+    simp only [SharpThreeSAT, hw, ↓reduceIte, SharpSAT]
   · simp only [SharpThreeSAT, toThreeSATThree, hw, Bool.false_eq_true, ite_false]
     decide
 

Complexity/Foundations/Data/List/Filter.lean

@@ -18,119 +18,91 @@ They are generalized from the canonical incidence-path occupancy proofs.
 
 ## Main results
 
-* `List.exists_pair_indices_of_two_le_filter_contains`.
-* `List.two_le_filter_contains_of_indices`.
+* `List.two_le_filter_contains_iff`.
 * `List.exists_other_index_of_two_le_filter_contains`.
 -/
 
 @[expose] public section
 
 namespace List
 
-/-- Two filtered memberships occur at distinct indices, even for repeated lists. -/
-theorem exists_pair_indices_of_two_le_filter_contains {α : Type*} [DecidableEq α]
-    (rs : List (List α)) (p : α)
-    (hlen : 2 ≤ (rs.filter fun r => r.contains p).length) :
-    ∃ (i j : ℕ) (hi : i < rs.length) (hj : j < rs.length),
-      i ≠ j ∧ p ∈ rs[i] ∧ p ∈ rs[j] := by
-  induction rs with
-  | nil => simp at hlen
-  | cons r rs ih =>
-    by_cases hp : p ∈ r
-    · have hne : (rs.filter fun r => r.contains p) ≠ [] := by
-        intro h
-        have hf : ((r :: rs).filter fun r => r.contains p) = [r] := by
-          have hpred : r.contains p = true := by simpa using hp
-          simp only [List.filter_cons, hpred, ↓reduceIte, h]
+/-- At least two memberships correspond to distinct indices, even for repeated equal lists. -/
+theorem two_le_filter_contains_iff {α : Type*} [DecidableEq α]
+    (rs : List (List α)) (p : α) :
+    2 ≤ (rs.filter fun r => r.contains p).length ↔
+      ∃ (i j : ℕ) (hi : i < rs.length) (hj : j < rs.length),
+        i ≠ j ∧ p ∈ rs[i] ∧ p ∈ rs[j] := by
+  constructor
+  · intro hlen
+    induction rs with
+    | nil => simp at hlen
+    | cons r rs ih =>
+      by_cases hp : p ∈ r
+      · have hne : (rs.filter fun r => r.contains p) ≠ [] := by
+          intro h
+          have hf : ((r :: rs).filter fun r => r.contains p) = [r] := by
+            have hpred : r.contains p = true := by simpa using hp
+            simp only [List.filter_cons, hpred, ↓reduceIte, h]
+          rw [hf] at hlen
+          simp at hlen
+        cases hf : rs.filter (fun r => r.contains p) with
+        | nil => exact False.elim (hne hf)
+        | cons t ts =>
+          have ht : t ∈ rs.filter (fun r => r.contains p) := by rw [hf]; simp
+          obtain ⟨htmem, htp⟩ := List.mem_filter.mp ht
+          obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp htmem
+          exact ⟨0, j + 1, by simp, by simpa using hj, by omega, hp, by simpa using htp⟩
+      · have hf : ((r :: rs).filter fun r => r.contains p) = rs.filter (fun r => r.contains p) := by
+          simp [hp]
         rw [hf] at hlen
-        simp at hlen
-      cases hf : rs.filter (fun r => r.contains p) with
-      | nil => exact False.elim (hne hf)
-      | cons t ts =>
-        have ht : t ∈ rs.filter (fun r => r.contains p) := by rw [hf]; simp
-        obtain ⟨htmem, htp⟩ := List.mem_filter.mp ht
-        obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp htmem
-        exact ⟨0, j + 1, by simp, by simpa using hj, by omega, hp, by simpa using htp⟩
-    · have hf : ((r :: rs).filter fun r => r.contains p) = rs.filter (fun r => r.contains p) := by
-        simp [hp]
-      rw [hf] at hlen
-      obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := ih hlen
-      exact ⟨i + 1, j + 1, by simpa using hi, by simpa using hj, by omega, hpi, hpj⟩
-
-/-- Two distinct indices witnessing membership give at least two filtered entries. -/
-theorem two_le_filter_contains_of_indices {α : Type*} [DecidableEq α]
-    (rs : List (List α)) (p : α) {i j : ℕ}
-    (hi : i < rs.length) (hj : j < rs.length) (hij : i ≠ j)
-    (hpi : p ∈ rs[i]) (hpj : p ∈ rs[j]) :
-    2 ≤ (rs.filter fun r => r.contains p).length := by
-  induction rs generalizing i j with
-  | nil => simp at hi
-  | cons r rs ih =>
-    cases i with
-    | zero =>
-      cases j with
-      | zero => exact False.elim (hij rfl)
-      | succ j =>
-        have hj' : j < rs.length := by simpa using hj
-        have hm : rs[j] ∈ rs.filter (fun r => r.contains p) :=
-          List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hj),
-            List.contains_iff_mem.mpr hpj⟩
-        obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm
-        have hphead : p ∈ r := hpi
-        simp only [List.filter_cons, List.contains_iff_mem.mpr hphead,
-          ite_true, List.length_cons]
-        omega
-    | succ i =>
-      cases j with
+        obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := ih hlen
+        exact ⟨i + 1, j + 1, by simpa using hi, by simpa using hj, by omega, hpi, hpj⟩
+  · rintro ⟨i, j, hi, hj, hij, hpi, hpj⟩
+    induction rs generalizing i j with
+    | nil => simp at hi
+    | cons r rs ih =>
+      cases i with
       | zero =>
-        have hi' : i < rs.length := by simpa using hi
-        have hm : rs[i] ∈ rs.filter (fun r => r.contains p) :=
-          List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hi),
-            List.contains_iff_mem.mpr hpi⟩
-        obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm
-        have hphead : p ∈ r := hpj
-        simp only [List.filter_cons, List.contains_iff_mem.mpr hphead,
-          ite_true, List.length_cons]
-        omega
-      | succ j =>
-        have ht := ih (by simpa using hi) (by simpa using hj) (by omega) hpi hpj
-        rw [List.filter_cons]
-        split_ifs
-        · simp only [List.length_cons]
+        cases j with
+        | zero => exact False.elim (hij rfl)
+        | succ j =>
+          have hj' : j < rs.length := by simpa using hj
+          have hm : rs[j] ∈ rs.filter (fun r => r.contains p) :=
+            List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hj),
+              List.contains_iff_mem.mpr hpj⟩
+          obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm
+          have hphead : p ∈ r := hpi
+          simp only [List.filter_cons, List.contains_iff_mem.mpr hphead,
+            ite_true, List.length_cons]
+          omega
+      | succ i =>
+        cases j with
+        | zero =>
+          have hi' : i < rs.length := by simpa using hi
+          have hm : rs[i] ∈ rs.filter (fun r => r.contains p) :=
+            List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hi),
+              List.contains_iff_mem.mpr hpi⟩
+          obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm
+          have hphead : p ∈ r := hpj
+          simp only [List.filter_cons, List.contains_iff_mem.mpr hphead,
+            ite_true, List.length_cons]
           omega
-        · exact ht
+        | succ j =>
+          have ht := ih i j (by simpa using hi) (by simpa using hj) (by omega) hpi hpj
+          rw [List.filter_cons]
+          split_ifs
+          · simp only [List.length_cons]
+            omega
+          · exact ht
 
-/-- At least two filtered memberships give an index different from any given index. -/
+/-- Two filtered memberships give an index different from any given natural number. -/
 theorem exists_other_index_of_two_le_filter_contains {α : Type*} [DecidableEq α]
-    (rs : List (List α)) (p : α) (i : ℕ) (hi : i < rs.length)
+    (rs : List (List α)) (p : α) (i : ℕ)
     (hcount : 2 ≤ (rs.filter fun r => r.contains p).length) :
     ∃ j, ∃ hj : j < rs.length, j ≠ i ∧ p ∈ rs[j] := by
-  induction rs generalizing i with
-  | nil => simp at hi
-  | cons r rs ih =>
-    cases i with
-    | zero =>
-      have hpos : 0 < (rs.filter fun r => r.contains p).length := by
-        rw [List.filter_cons] at hcount
-        split_ifs at hcount
-        · simp only [List.length_cons] at hcount
-          omega
-        · omega
-      obtain ⟨s, hs⟩ := List.exists_mem_of_length_pos hpos
-      have hm := List.mem_filter.mp hs
-      obtain ⟨j, hj, hsj⟩ := List.mem_iff_getElem.mp hm.1
-      refine ⟨j + 1, by simp only [List.length_cons]; omega, by omega, ?_⟩
-      simp only [List.getElem_cons_succ]
-      rw [hsj]
-      exact List.contains_iff_mem.mp hm.2
-    | succ i =>
-      by_cases hmem : r.contains p = true
-      · exact ⟨0, by simp, by omega, by simpa using List.contains_iff_mem.mp hmem⟩
-      · have ht : 2 ≤ (rs.filter fun r => r.contains p).length := by
-          have hp : p ∉ r := fun hp => hmem (List.contains_iff_mem.mpr hp)
-          simpa [List.filter_cons, hp] using hcount
-        obtain ⟨j, hj, hji, hp⟩ := ih i (by simp only [List.length_cons] at hi; omega) ht
-        exact ⟨j + 1, by simp only [List.length_cons]; omega, by omega, by simpa using hp⟩
-
+  obtain ⟨j, k, hj, hk, hjk, hpj, hpk⟩ := (two_le_filter_contains_iff rs p).1 hcount
+  by_cases hji : j = i
+  · exact ⟨k, hk, by omega, hpk⟩
+  · exact ⟨j, hj, hji, hpj⟩
 
 end List

Complexity/Foundations/Data/List/Last.lean

@@ -8,12 +8,13 @@ module
 -- upstream: candidate
 
 public import Complexity.Init
-import Mathlib.Data.List.GetD
+import Init.Data.List.Lemmas
 
 /-!
 # Defaulted last-element lookup
 
-The default is unused for a nonempty list. The proof is moved from the path semantics.
+The default is unused for a nonempty list. This indexed form follows from the core last-element
+lookup API.
 
 ## Main results
 
@@ -27,14 +28,7 @@ namespace List
 /-- A nonempty list's defaulted last lookup is its final indexed element. -/
 theorem getLastD_eq_getElem {α : Type*} (xs : List α) (d : α) (hne : xs ≠ []) :
     xs.getLastD d = xs[xs.length - 1]'(by cases xs <;> simp_all) := by
-  induction xs generalizing d with
-  | nil => exact False.elim (hne rfl)
-  | cons a xs ih =>
-    cases xs with
-    | nil => rfl
-    | cons b xs =>
-      rw [List.getLastD_cons, ih a (List.cons_ne_nil _ _)]
-      simp only [List.length_cons, Nat.add_sub_cancel, List.getElem_cons_succ]
-
+  rw [List.getLastD_eq_getLast?, List.getLast?_eq_some_getLast hne]
+  exact List.getLast_eq_getElem hne
 
 end List