SETH ⇒ OVC sparsification bundle 10: concrete word-RAM formalization

import Definitions.Def_WordRAMEquivalence_Foundation1
import Definitions.Def_WordRAM_Conjectures
import Definitions.Def_WordRAM_SETHOV_Reduction
import Definitions.Def_SETHOV_Sparsification_09

set_option autoImplicit true

/-! Weak flowers are families of equally sized clauses sharing a nonempty proper
core. Petals may overlap. The selection rule and quantitative recursion bound
are not supplied by this file. -/
namespace WordRAM.Conjectures.Sparsification.Flowers

/-- All clauses of the specified size that contain the core. -/
def family (formula : CNF n) (core : Clause n) (size : Nat) : CNF n :=
  formula.filter (fun clause => decide (clause.length = size ∧ core ⊆ clause))

/-- The core need not be the entire intersection. Enlarging it, when possible,
produces a candidate with smaller petals; priority among candidates is handled
by the branching algorithm. Distinctness follows from normalized input. -/
def Candidate (formula : CNF n) (threshold : Nat → Nat) (core : Clause n) (size : Nat) : Prop :=
  core.Nodup ∧ 0 < core.length ∧ core.length < size ∧
    threshold (size - core.length) ≤ (family formula core size).length

instance (formula : CNF n) (threshold : Nat → Nat) (core : Clause n) (size : Nat) :
    Decidable (Candidate formula threshold core size) := inferInstanceAs
      (Decidable (core.Nodup ∧ 0 < core.length ∧ core.length < size ∧
        threshold (size - core.length) ≤ (family formula core size).length))

def Terminal (formula : CNF n) (threshold : Nat → Nat) : Prop :=
  ∀ core size, ¬ Candidate formula threshold core size

theorem singleton_family (formula : CNF n) (literal : Literal n) (size : Nat) :
    (family formula [literal] size).length = Counting.layerDegree formula literal size := by
  unfold family Counting.layerDegree
  rw [List.filter_filter]
  congr 2
  funext clause
  simp [List.subset_def]

/-- In an antichain a literal belongs to at most one unit clause. -/
theorem unit_degree (formula : CNF n) (chain : Normalize.Antichain formula) (literal : Literal n) :
    Counting.layerDegree formula literal 1 ≤ 1 := by
  rw [← singleton_family]
  have subchain : Normalize.Antichain (family formula [literal] 1) := chain.filter _
  have units : ∀ clause ∈ family formula [literal] 1, clause = [literal] := by
    intro clause member
    obtain ⟨_, properties⟩ := List.mem_filter.mp member
    have properties : clause.length = 1 ∧ [literal] ⊆ clause := of_decide_eq_true properties
    obtain ⟨head, eq⟩ := List.length_eq_one_iff.mp properties.1
    subst clause
    have eqHead : literal = head := List.mem_singleton.mp (properties.2 (by simp))
    simp [eqHead]
  generalize eq : family formula [literal] 1 = selected at *
  cases selected with
  | nil => simp
  | cons first rest =>
    cases rest with
    | nil => simp
    | cons second rest =>
      have firstEq := units first (by simp)
      have secondEq := units second (by simp)
      have apart := (List.pairwise_cons.mp subchain).1 second (by simp)
      have subset : first ⊆ second := by rw [firstEq, secondEq]; exact List.Subset.refl _
      exact False.elim (apart.1 subset)

theorem terminal_layer_bound (formula : CNF n) (threshold : Nat → Nat) (k bound : Nat)
    (chain : Normalize.Antichain formula) (terminal : Terminal formula threshold)
    (positive : 1 ≤ bound)
    (thresholdBound : ∀ i, 0 < i → i < k → threshold i ≤ bound)
    (literal : Literal n) (size : Nat) (sizePositive : 0 < size) (sizeBound : size ≤ k) :
    Counting.layerDegree formula literal size ≤ bound := by
  by_cases unit : size = 1
  · subst size
    exact Nat.le_trans (unit_degree formula chain literal) positive
  · have larger : 1 < size := by omega
    have absent := terminal [literal] size
    have below : (family formula [literal] size).length < threshold (size - 1) := by
      apply Nat.lt_of_not_ge
      intro enough
      apply absent
      exact ⟨by simp, by simp, by simpa using larger, by simpa using enough⟩
    rw [singleton_family] at below
    have upper := thresholdBound (size - 1) (by omega) (by omega)
    omega

/-- Once no eligible weak flower remains, the normalized nonempty clauses are
linearly many. This is the sparse-leaf guarantee, independent of leaf counting. -/
theorem terminal_sparse (formula : CNF n) (threshold : Nat → Nat) (k bound : Nat)
    (chain : Normalize.Antichain formula)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (nonempty : ∀ clause ∈ formula, clause ≠ [])
    (width : ∀ clause ∈ formula, clause.length ≤ k)
    (terminal : Terminal formula threshold) (positive : 1 ≤ bound)
    (thresholdBound : ∀ i, 0 < i → i < k → threshold i ≤ bound) :
    formula.length ≤ (2 * (k * bound)) * n :=
  Counting.sparse_of_layers formula k bound nodup nonempty width
    (terminal_layer_bound formula threshold k bound chain terminal positive thresholdBound)

end WordRAM.Conjectures.Sparsification.Flowers

/-! Finite weak-flower selection. Enumeration is ordered by clause size and
then petal size. This is the computable specification; `SparsificationFlowerSearch` supplies
the wordRAM implementation and its proved running-time bound. -/
namespace WordRAM.Conjectures.Sparsification.Selection

/-- All literal lists of a fixed length. For fixed clause width this is a
polynomial-size search in the variable count. `CoreEnumeration.cores_length`
and `CoreSearch.cost_bound` quantify the search size and machine runtime. -/
def cores (n : Nat) : Nat → CNF n
  | 0 => [[]]
  | length + 1 => (Counting.literals n).flatMap (fun literal =>
      (cores n length).map (literal :: ·))

theorem mem_cores (clause : Clause n) (length : Nat) :
    clause ∈ cores n length ↔ clause.length = length := by
  induction length generalizing clause with
  | zero => simp [cores]
  | succ length ih =>
    cases clause with
    | nil => simp [cores]
    | cons literal rest =>
      simp [cores, List.mem_flatMap, List.mem_map, ih, Counting.mem_literals]

/-- Size is the outer loop; smaller petals are considered first within it. -/
def choices (n k : Nat) : List (Nat × Clause n) :=
  (List.range (k + 1)).flatMap (fun size =>
    (List.range size).flatMap (fun petalSize =>
      (cores n (size - petalSize)).map (fun core => (size, core))))

theorem choice_size (member : (size, core) ∈ choices n k) : size ≤ k := by
  obtain ⟨s, present, member⟩ := List.mem_flatMap.mp member
  obtain ⟨_, _, member⟩ := List.mem_flatMap.mp member
  obtain ⟨_, _, eq⟩ := List.mem_map.mp member
  have same : s = size := congrArg Prod.fst eq
  subst s
  exact Nat.le_of_lt_succ (List.mem_range.mp present)

theorem choice_complete (core : Clause n) (size k : Nat)
    (positive : 0 < core.length) (proper : core.length < size) (bounded : size ≤ k) :
    (size, core) ∈ choices n k := by
  apply List.mem_flatMap.mpr
  refine ⟨size, List.mem_range.mpr (by omega), ?_⟩
  apply List.mem_flatMap.mpr
  refine ⟨size - core.length, List.mem_range.mpr (by omega), ?_⟩
  apply List.mem_map.mpr
  exact ⟨core, (mem_cores core _).mpr (by omega), rfl⟩

def select (formula : CNF n) (threshold : Nat → Nat) (k : Nat) : Option (Nat × Clause n) :=
  (choices n k).find? (fun pair => decide (Flowers.Candidate formula threshold pair.2 pair.1))

theorem select_sound (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (found : select formula threshold k = some (size, core)) :
    Flowers.Candidate formula threshold core size ∧ size ≤ k := by
  unfold select at found
  have valid := List.find?_some found
  exact ⟨of_decide_eq_true valid, choice_size (List.mem_of_find?_eq_some found)⟩

theorem select_none_bounded (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (none : select formula threshold k = .none) (core : Clause n) (size : Nat) (bounded : size ≤ k) :
    ¬ Flowers.Candidate formula threshold core size := by
  intro candidate
  have member := choice_complete core size k candidate.2.1 candidate.2.2.1 bounded
  have absent := List.find?_eq_none.mp none (size, core) member
  exact absent (decide_eq_true candidate)

/-- Width bounds rule out candidates outside the enumerated range too. -/
theorem select_none_terminal (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (width : ∀ clause ∈ formula, clause.length ≤ k)
    (thresholdPositive : ∀ i, 0 < threshold i)
    (none : select formula threshold k = .none) : Flowers.Terminal formula threshold := by
  intro core size candidate
  by_cases bounded : size ≤ k
  · exact select_none_bounded formula threshold k none core size bounded candidate
  · have empty : Flowers.family formula core size = [] := by
      apply List.eq_nil_iff_forall_not_mem.mpr
      intro clause member
      obtain ⟨present, property⟩ := List.mem_filter.mp member
      have property : clause.length = size ∧ core ⊆ clause := of_decide_eq_true property
      have bound := width clause present
      omega
    have enough := candidate.2.2.2
    rw [empty] at enough
    have positive := thresholdPositive (size - core.length)
    simp only [List.length_nil] at enough
    omega

theorem select_none_sparse (formula : CNF n) (threshold : Nat → Nat) (k bound : Nat)
    (chain : Normalize.Antichain formula)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (nonempty : ∀ clause ∈ formula, clause ≠ [])
    (width : ∀ clause ∈ formula, clause.length ≤ k)
    (thresholdPositive : ∀ i, 0 < threshold i)
    (none : select formula threshold k = .none) (positive : 1 ≤ bound)
    (thresholdBound : ∀ i, 0 < i → i < k → threshold i ≤ bound) :
    formula.length ≤ (2 * (k * bound)) * n :=
  Flowers.terminal_sparse formula threshold k bound chain nodup nonempty width
    (select_none_terminal formula threshold k width thresholdPositive none) positive thresholdBound

end WordRAM.Conjectures.Sparsification.Selection

/-! Branching on selected weak flowers in arbitrary list representations of
clauses. The child formulas are normalized before recursion. -/
namespace WordRAM.Conjectures.Sparsification.Branch

/-- Remove the literals belonging to the common core. -/
def petal (core clause : Clause n) : Clause n :=
  clause.filter (fun literal => !decide (literal ∈ core))

def remaining (formula : CNF n) (core : Clause n) (size : Nat) : CNF n :=
  formula.filter (fun clause => !decide (clause.length = size ∧ core ⊆ clause))

def left (formula : CNF n) (core : Clause n) (size : Nat) : CNF n :=
  Normalize.normalize (remaining formula core size ++ [core])

def right (formula : CNF n) (core : Clause n) (size : Nat) : CNF n :=
  Normalize.normalize (remaining formula core size ++
    (Flowers.family formula core size).map (petal core))

theorem clause_split (assignment : Fin n → Bool) (core clause : Clause n) (subset : core ⊆ clause) :
    ClauseHolds assignment clause ↔ ClauseHolds assignment core ∨ ClauseHolds assignment (petal core clause) := by
  constructor
  · rintro ⟨literal, member, truth⟩
    by_cases inCore : literal ∈ core
    · exact Or.inl ⟨literal, inCore, truth⟩
    · exact Or.inr ⟨literal, by simp [petal, member, inCore], truth⟩
  · rintro (⟨literal, member, truth⟩ | ⟨literal, member, truth⟩)
    · exact ⟨literal, subset member, truth⟩
    · exact ⟨literal, (List.mem_filter.mp member).1, truth⟩

theorem formula_split (assignment : Fin n → Bool) (formula : CNF n) (core : Clause n) (size : Nat) :
    Holds assignment formula ↔ Holds assignment (remaining formula core size) ∧
      Holds assignment (Flowers.family formula core size) := by
  constructor
  · intro holds
    exact ⟨fun _ member => holds _ (List.mem_filter.mp member).1,
      fun _ member => holds _ (List.mem_filter.mp member).1⟩
  · rintro ⟨rest, selected⟩ clause member
    by_cases eligible : clause.length = size ∧ core ⊆ clause
    · exact selected clause (by simp [Flowers.family, member, eligible])
    · exact rest clause (List.mem_filter.mpr ⟨member, by
        simp only [decide_eq_false eligible, Bool.not_false]⟩)

theorem family_split (assignment : Fin n → Bool) (formula : CNF n) (core : Clause n) (size : Nat) :
    Holds assignment (Flowers.family formula core size) ↔ ClauseHolds assignment core ∨
      Holds assignment ((Flowers.family formula core size).map (petal core)) := by
  constructor
  · intro holds
    by_cases coreTrue : ClauseHolds assignment core
    · exact Or.inl coreTrue
    · right
      intro p member
      obtain ⟨clause, present, rfl⟩ := List.mem_map.mp member
      have properties := of_decide_eq_true (List.mem_filter.mp present).2
      exact ((clause_split assignment core clause properties.2).mp (holds clause present)).resolve_left coreTrue
  · rintro (coreTrue | petalsTrue) clause member
    · have properties := of_decide_eq_true (List.mem_filter.mp member).2
      exact (clause_split assignment core clause properties.2).mpr (Or.inl coreTrue)
    · have properties := of_decide_eq_true (List.mem_filter.mp member).2
      exact (clause_split assignment core clause properties.2).mpr
        (Or.inr (petalsTrue _ (List.mem_map.mpr ⟨clause, member, rfl⟩)))

theorem holds (assignment : Fin n → Bool) (formula : CNF n) (core : Clause n) (size : Nat) :
    Holds assignment formula ↔ Holds assignment (left formula core size) ∨ Holds assignment (right formula core size) := by
  rw [left, right, Normalize.normalize_holds, Normalize.normalize_holds,
    holds_append, holds_append, formula_split assignment formula core size, family_split]
  have singleton : Holds assignment [core] ↔ ClauseHolds assignment core := by simp [Holds]
  rw [singleton]
  constructor
  · rintro ⟨rest, coreTrue | petalsTrue⟩
    · exact Or.inl ⟨rest, coreTrue⟩
    · exact Or.inr ⟨rest, petalsTrue⟩
  · rintro (⟨rest, coreTrue⟩ | ⟨rest, petalsTrue⟩)
    · exact ⟨rest, Or.inl coreTrue⟩
    · exact ⟨rest, Or.inr petalsTrue⟩

theorem filter_lengths (items : List α) (predicate : α → Bool) :
    (items.filter predicate).length + (items.filter (fun a => !predicate a)).length = items.length := by
  induction items with
  | nil => simp
  | cons item rest ih =>
    cases eq : predicate item <;> simp [eq] <;> omega

theorem filter_weights (formula : CNF n) (predicate : Clause n → Bool) :
    weight (formula.filter predicate) + weight (formula.filter (fun c => !predicate c)) = weight formula := by
  induction formula with
  | nil => simp [weight]
  | cons clause rest ih =>
    cases eq : predicate clause <;> simp [eq, weight, ih, Nat.add_assoc, Nat.add_left_comm]

theorem petal_length (core clause : Clause n) (coreNodup : core.Nodup) (clauseNodup : clause.Nodup)
    (subset : core ⊆ clause) : core.length + (petal core clause).length = clause.length := by
  have eq : (clause.filter (fun literal => decide (literal ∈ core))).length = core.length := by
    apply Nat.le_antisymm
    · apply List.Nodup.length_le_of_subset (clauseNodup.filter _)
      intro literal member
      exact of_decide_eq_true (List.mem_filter.mp member).2
    · apply coreNodup.length_le_of_subset
      intro literal member
      simp [subset member, member]
  have partition := filter_lengths clause (fun literal => decide (literal ∈ core))
  rw [eq] at partition
  exact partition

theorem family_weight (formula : CNF n) (core : Clause n) (size : Nat)
    (coreNodup : core.Nodup) (nodup : ∀ clause ∈ formula, clause.Nodup) :
    weight (Flowers.family formula core size) =
      (Flowers.family formula core size).length * core.length +
        weight ((Flowers.family formula core size).map (petal core)) := by
  have properties : ∀ clause ∈ Flowers.family formula core size, clause.Nodup ∧ core ⊆ clause := by
    intro clause member
    obtain ⟨present, property⟩ := List.mem_filter.mp member
    exact ⟨nodup clause present, (of_decide_eq_true property).2⟩
  generalize Flowers.family formula core size = selected at *
  induction selected with
  | nil => simp [weight]
  | cons clause rest ih =>
    have first := properties clause (by simp)
    have len := petal_length core clause coreNodup first.1 first.2
    have tail := ih (fun c hc => properties c (by simp [hc]))
    simp only [weight, List.length_cons, List.map_cons, Nat.add_mul, Nat.one_mul]
    omega

/-- Both normalized children strictly decrease literal occurrences. This only
proves termination; it does not bound the recursion tree subexponentially. -/
theorem smaller (formula : CNF n) (core : Clause n) (size : Nat)
    (coreNodup : core.Nodup) (nodup : ∀ clause ∈ formula, clause.Nodup)
    (positive : 0 < core.length) (enough : 2 ≤ (Flowers.family formula core size).length) :
    weight (left formula core size) < weight formula ∧ weight (right formula core size) < weight formula := by
  have partition := filter_weights formula (fun clause => decide (clause.length = size ∧ core ⊆ clause))
  change weight (Flowers.family formula core size) + weight (remaining formula core size) = weight formula at partition
  have selectedWeight := family_weight formula core size coreNodup nodup
  have leftBound := Normalize.normalize_weight (remaining formula core size ++ [core])
  have rightBound := Normalize.normalize_weight (remaining formula core size ++
    (Flowers.family formula core size).map (petal core))
  rw [weight_append] at leftBound rightBound
  change weight (left formula core size) ≤ weight (remaining formula core size) + (core.length + 0) at leftBound
  change weight (right formula core size) ≤ weight (remaining formula core size) +
    weight ((Flowers.family formula core size).map (petal core)) at rightBound
  have multiple := Nat.mul_le_mul_right core.length enough
  omega

theorem width (formula : CNF n) (core : Clause n) (size k : Nat)
    (original : ∀ clause ∈ formula, clause.length ≤ k) (coreBound : core.length ≤ k) :
    (∀ clause ∈ left formula core size, clause.length ≤ k) ∧
      (∀ clause ∈ right formula core size, clause.length ≤ k) := by
  have restBound : ∀ clause ∈ remaining formula core size, clause.length ≤ k :=
    fun clause member => original clause (List.mem_filter.mp member).1
  constructor
  · apply Normalize.normalize_kcnf (SATInstance.mk n (remaining formula core size ++ [core]))
    intro clause member
    rcases List.mem_append.mp member with member | member
    · exact restBound clause member
    · have eq := List.mem_singleton.mp member
      subst clause
      exact coreBound
  · apply Normalize.normalize_kcnf (SATInstance.mk n (remaining formula core size ++
      (Flowers.family formula core size).map (petal core)))
    intro clause member
    rcases List.mem_append.mp member with member | member
    · exact restBound clause member
    · obtain ⟨originalClause, present, rfl⟩ := List.mem_map.mp member
      exact Nat.le_trans (List.length_filter_le _ _)
        (original originalClause (List.mem_filter.mp present).1)

end WordRAM.Conjectures.Sparsification.Branch