SETH ⇒ OVC sparsification bundle 9: 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_08

set_option autoImplicit true

/-! Computable literal deduplication and clause subsumption elimination for the
sparsification procedure. Lists may initially contain duplicates and permutations. -/
namespace WordRAM.Conjectures.Sparsification.Normalize

/-- Keep the last occurrence of each literal, without enumerating variables. -/
def clean : Clause n → Clause n
  | [] => []
  | literal :: rest => if literal ∈ rest then clean rest else literal :: clean rest

@[simp] theorem mem_clean (literal : Literal n) (clause : Clause n) :
    literal ∈ clean clause ↔ literal ∈ clause := by
  induction clause with
  | nil => simp [clean]
  | cons head rest ih =>
    by_cases duplicate : head ∈ rest
    · simp only [clean, if_pos duplicate, ih, List.mem_cons]
      constructor
      · exact Or.inr
      · rintro (rfl | member) <;> assumption
    · simp [clean, duplicate, ih]

theorem clean_length (clause : Clause n) : (clean clause).length ≤ clause.length := by
  induction clause with
  | nil => simp [clean]
  | cons head rest ih => unfold clean; split <;> simp_all <;> omega

theorem clean_nodup (clause : Clause n) : (clean clause).Nodup := by
  induction clause with
  | nil => simp [clean]
  | cons head rest ih => unfold clean; split <;> simp_all

theorem clean_holds (assignment : Fin n → Bool) (clause : Clause n) :
    ClauseHolds assignment (clean clause) ↔ ClauseHolds assignment clause := by
  simp only [ClauseHolds, mem_clean]

/-- An antichain of literal sets, also excluding clauses that differ only by
literal ordering. Keeping duplicate set representations would invalidate counts. -/
def Antichain (formula : CNF n) : Prop :=
  formula.Pairwise (fun c d => ¬ c ⊆ d ∧ ¬ d ⊆ c)

def insert (clause : Clause n) (formula : CNF n) : CNF n :=
  if ∃ smaller ∈ formula, smaller ⊆ clause then formula
  else clause :: formula.filter (fun larger => !decide (clause ⊆ larger))

def minimize : CNF n → CNF n
  | [] => []
  | clause :: rest => insert clause (minimize rest)

def normalize (formula : CNF n) : CNF n := minimize (formula.map clean)

theorem holds_mono (assignment : Fin n → Bool) (small large : Clause n)
    (subset : small ⊆ large) (holds : ClauseHolds assignment small) : ClauseHolds assignment large := by
  obtain ⟨literal, member, truth⟩ := holds
  exact ⟨literal, subset member, truth⟩

theorem insert_holds (assignment : Fin n → Bool) (clause : Clause n) (formula : CNF n) :
    Holds assignment (insert clause formula) ↔ ClauseHolds assignment clause ∧ Holds assignment formula := by
  unfold insert
  split
  · rename_i subsumed
    obtain ⟨smaller, member, subset⟩ := subsumed
    constructor
    · intro holds; exact ⟨holds_mono assignment smaller clause subset (holds smaller member), holds⟩
    · exact And.right
  · constructor
    · intro holds
      have clauseTrue := holds clause (by simp)
      refine ⟨clauseTrue, ?_⟩
      intro larger member
      by_cases subset : clause ⊆ larger
      · exact holds_mono assignment clause larger subset clauseTrue
      · exact holds larger (by simp [member, subset])
    · rintro ⟨clauseTrue, holds⟩ larger member
      simp only [List.mem_cons, List.mem_filter, Bool.not_eq_true', decide_eq_false_iff_not] at member
      rcases member with rfl | ⟨member, _⟩
      · exact clauseTrue
      · exact holds larger member

theorem insert_antichain (clause : Clause n) (formula : CNF n) (chain : Antichain formula) :
    Antichain (insert clause formula) := by
  unfold insert
  split
  · exact chain
  · rename_i absent
    apply List.pairwise_cons.mpr
    constructor
    · intro larger member
      simp only [List.mem_filter, Bool.not_eq_true', decide_eq_false_iff_not] at member
      exact ⟨member.2, fun subset => absent ⟨larger, member.1, subset⟩⟩
    · exact chain.filter _

theorem insert_member (clause : Clause n) (formula : CNF n) (member : c ∈ insert clause formula) :
    c = clause ∨ c ∈ formula := by
  unfold insert at member
  split at member
  · exact Or.inr member
  · simp only [List.mem_cons, List.mem_filter] at member
    exact member.imp_right And.left

/-- Every discarded clause has a retained subset; this records why removal
preserves truth and later supports the quantitative elimination accounting. -/
theorem insert_cover (clause : Clause n) (formula : CNF n) (c : Clause n)
    (member : c ∈ clause :: formula) : ∃ smaller ∈ insert clause formula, smaller ⊆ c := by
  unfold insert
  split
  · rename_i subsumed
    rcases List.mem_cons.mp member with rfl | member
    · exact subsumed
    · exact ⟨c, member, List.Subset.refl _⟩
  · rcases List.mem_cons.mp member with rfl | member
    · exact ⟨c, by simp, List.Subset.refl _⟩
    · by_cases subset : clause ⊆ c
      · exact ⟨clause, by simp, subset⟩
      · exact ⟨c, by simp [member, subset], List.Subset.refl _⟩

theorem minimize_holds (assignment : Fin n → Bool) (formula : CNF n) :
    Holds assignment (minimize formula) ↔ Holds assignment formula := by
  induction formula with
  | nil => rfl
  | cons clause rest ih =>
    rw [minimize, insert_holds, ih]
    simp [Holds]

theorem minimize_antichain (formula : CNF n) : Antichain (minimize formula) := by
  induction formula with
  | nil => exact .nil
  | cons clause rest ih => exact insert_antichain clause _ ih

theorem minimize_member (formula : CNF n) (member : c ∈ minimize formula) : c ∈ formula := by
  induction formula with
  | nil => exact member
  | cons clause rest ih =>
    rcases insert_member clause (minimize rest) member with rfl | member
    · exact List.mem_cons_self
    · exact List.mem_cons_of_mem _ (ih member)

theorem minimize_cover (formula : CNF n) (c : Clause n) (member : c ∈ formula) :
    ∃ smaller ∈ minimize formula, smaller ⊆ c := by
  induction formula with
  | nil => simp at member
  | cons clause rest ih =>
    rcases List.mem_cons.mp member with rfl | member
    · exact insert_cover c (minimize rest) c (by simp)
    · obtain ⟨smaller, kept, subset⟩ := ih member
      obtain ⟨smallest, kept', subset'⟩ := insert_cover clause (minimize rest) smaller (by simp [kept])
      exact ⟨smallest, kept', List.Subset.trans subset' subset⟩

theorem normalize_holds (assignment : Fin n → Bool) (formula : CNF n) :
    Holds assignment (normalize formula) ↔ Holds assignment formula := by
  rw [normalize, minimize_holds]
  simp only [Holds, List.mem_map, forall_exists_index, and_imp]
  constructor
  · intro h clause member; exact (clean_holds assignment clause).mp (h _ clause member rfl)
  · intro h _ clause member eq; subst eq; exact (clean_holds assignment clause).mpr (h clause member)

theorem normalize_antichain (formula : CNF n) : Antichain (normalize formula) := minimize_antichain _

theorem normalize_nodup_literals (formula : CNF n) : ∀ clause ∈ normalize formula, clause.Nodup := by
  intro clause member
  obtain ⟨original, _, eq⟩ := List.mem_map.mp (minimize_member _ member)
  subst clause
  exact clean_nodup original

theorem normalize_kcnf (f : SATInstance) (hk : f.IsKCNF k) :
    (SATInstance.mk f.variables (normalize f.clauses)).IsKCNF k := by
  intro clause member
  obtain ⟨original, present, eq⟩ := List.mem_map.mp (minimize_member _ member)
  subst clause
  exact Nat.le_trans (clean_length original) (hk original present)

theorem weight_filter (formula : CNF n) (predicate : Clause n → Bool) :
    weight (formula.filter predicate) ≤ weight formula := by
  induction formula with
  | nil => simp [weight]
  | cons clause rest ih =>
    simp only [List.filter_cons]
    split <;> simp only [weight] <;> omega

theorem insert_weight (clause : Clause n) (formula : CNF n) :
    weight (insert clause formula) ≤ clause.length + weight formula := by
  unfold insert
  split
  · omega
  · exact Nat.add_le_add_left (weight_filter formula _) _

theorem minimize_weight (formula : CNF n) : weight (minimize formula) ≤ weight formula := by
  induction formula with
  | nil => exact Nat.le_refl _
  | cons clause rest ih =>
    exact Nat.le_trans (insert_weight clause (minimize rest)) (Nat.add_le_add_left ih _)

theorem clean_weight (formula : CNF n) : weight (formula.map clean) ≤ weight formula := by
  induction formula with
  | nil => exact Nat.le_refl _
  | cons clause rest ih =>
    exact Nat.add_le_add (clean_length clause) ih

theorem normalize_weight (formula : CNF n) : weight (normalize formula) ≤ weight formula :=
  Nat.le_trans (minimize_weight _) (clean_weight formula)

theorem insert_length (clause : Clause n) (formula : CNF n) :
    (insert clause formula).length ≤ formula.length + 1 := by
  unfold insert
  split
  · omega
  · simp only [List.length_cons]
    exact Nat.add_le_add_right (List.length_filter_le _ _) 1

theorem minimize_length (formula : CNF n) : (minimize formula).length ≤ formula.length := by
  induction formula with
  | nil => exact Nat.le_refl _
  | cons clause rest ih =>
    exact Nat.le_trans (insert_length clause _) (Nat.add_le_add_right ih 1)

theorem normalize_length (formula : CNF n) : (normalize formula).length ≤ formula.length := by
  have bound := minimize_length (formula.map clean)
  simpa only [normalize, List.length_map] using bound

/-- Each original clause is represented by a retained clause contained in it. -/
theorem normalize_cover (formula : CNF n) (clause : Clause n) (member : clause ∈ formula) :
    ∃ smaller ∈ normalize formula, smaller ⊆ clause := by
  obtain ⟨smaller, kept, subset⟩ := minimize_cover (formula.map clean) (clean clause)
    (List.mem_map.mpr ⟨clause, member, rfl⟩)
  exact ⟨smaller, kept, fun _ h => (mem_clean _ clause).mp (subset h)⟩

theorem clean_eq (clause : Clause n) (nodup : clause.Nodup) : clean clause = clause := by
  induction clause with
  | nil => rfl
  | cons literal rest ih =>
    obtain ⟨absent, restNodup⟩ := List.nodup_cons.mp nodup
    simp [clean, absent, ih restNodup]

theorem minimize_eq (formula : CNF n) (chain : Antichain formula) : minimize formula = formula := by
  induction formula with
  | nil => rfl
  | cons clause rest ih =>
    obtain ⟨apart, restChain⟩ := List.pairwise_cons.mp chain
    rw [minimize, ih restChain]
    have absent : ¬ ∃ smaller ∈ rest, smaller ⊆ clause := by
      rintro ⟨smaller, member, subset⟩
      exact (apart smaller member).2 subset
    rw [insert, if_neg absent]
    congr 1
    apply List.filter_eq_self.mpr
    intro larger member
    simp [(apart larger member).1]

theorem normalize_eq (formula : CNF n) (chain : Antichain formula)
    (nodup : ∀ clause ∈ formula, clause.Nodup) : normalize formula = formula := by
  have mapped : formula.map clean = formula := by
    induction formula with
    | nil => rfl
    | cons clause rest ih =>
      simp only [List.map_cons]
      rw [clean_eq clause (nodup clause (by simp))]
      congr 1
      exact ih (List.pairwise_cons.mp chain).2 (fun c hc => nodup c (by simp [hc]))
  rw [normalize, mapped, minimize_eq formula chain]

@[simp] theorem normalize_idempotent (formula : CNF n) :
    normalize (normalize formula) = normalize formula :=
  normalize_eq _ (normalize_antichain formula) (normalize_nodup_literals formula)

end WordRAM.Conjectures.Sparsification.Normalize

/-! Incidence counting for the terminal formulas of sparsification. These bounds
are conditional on occurrence bounds; deriving those bounds from the absence of
weak sunflowers is a separate combinatorial obligation. -/
namespace WordRAM.Conjectures.Sparsification.Counting

/-- Both polarities of every variable. -/
def literals (n : Nat) : List (Literal n) :=
  (List.ofFn fun i : Fin n => Literal.mk i true) ++
    (List.ofFn fun i : Fin n => Literal.mk i false)

@[simp] theorem literals_length (n : Nat) : (literals n).length = 2 * n := by
  simp [literals, Nat.two_mul]

theorem mem_literals (literal : Literal n) : literal ∈ literals n := by
  rcases literal with ⟨index, polarity⟩
  cases polarity <;> simp [literals, List.mem_ofFn]

/-- Number of clauses containing a literal, counting each clause once. -/
def degree (formula : CNF n) (literal : Literal n) : Nat :=
  (formula.filter (fun clause => decide (literal ∈ clause))).length

def incidence (carrier : List (Literal n)) (formula : CNF n) : Nat :=
  (carrier.map (degree formula)).sum

theorem incidence_cons (carrier : List (Literal n)) (clause : Clause n) (formula : CNF n) :
    incidence carrier (clause :: formula) =
      (carrier.filter (fun literal => decide (literal ∈ clause))).length + incidence carrier formula := by
  induction carrier with
  | nil => simp [incidence]
  | cons literal rest ih =>
    by_cases member : literal ∈ clause <;>
      simp_all [incidence, degree, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

theorem weight_le_incidence (carrier : List (Literal n)) (formula : CNF n)
    (complete : ∀ literal, literal ∈ carrier)
    (nodup : ∀ clause ∈ formula, clause.Nodup) : weight formula ≤ incidence carrier formula := by
  induction formula with
  | nil => simp [weight, incidence]
  | cons clause rest ih =>
    rw [weight, incidence_cons]
    apply Nat.add_le_add
    · apply (nodup clause (by simp)).length_le_of_subset
      intro literal member
      simp [complete literal, member]
    · exact ih (fun c hc => nodup c (by simp [hc]))

theorem incidence_le (carrier : List (Literal n)) (formula : CNF n) (bound : Nat)
    (bounded : ∀ literal ∈ carrier, degree formula literal ≤ bound) :
    incidence carrier formula ≤ carrier.length * bound := by
  induction carrier with
  | nil => simp [incidence]
  | cons literal rest ih =>
    have first := bounded literal (by simp)
    have later := ih (fun l hl => bounded l (by simp [hl]))
    simpa [incidence, Nat.add_mul, Nat.add_comm] using Nat.add_le_add first later

theorem weight_le (formula : CNF n) (bound : Nat)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (bounded : ∀ literal, degree formula literal ≤ bound) : weight formula ≤ 2 * n * bound := by
  have lower := weight_le_incidence (literals n) formula mem_literals nodup
  have upper := incidence_le (literals n) formula bound (fun literal _ => bounded literal)
  simpa only [literals_length] using Nat.le_trans lower upper

theorem length_le_weight (formula : CNF n) (nonempty : ∀ clause ∈ formula, clause ≠ []) :
    formula.length ≤ weight formula := by
  induction formula with
  | nil => exact Nat.le_refl _
  | cons clause rest ih =>
    have positive : 0 < clause.length := List.length_pos_iff.mpr (nonempty clause (by simp))
    have later := ih (fun c hc => nonempty c (by simp [hc]))
    simp only [List.length_cons, weight]
    omega

/-- A bound on occurrences of each literal gives a linear clause bound.
Empty clauses are excluded here; their presence is an immediate unsatisfiable leaf. -/
theorem sparse (formula : CNF n) (bound : Nat)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (nonempty : ∀ clause ∈ formula, clause ≠ [])
    (bounded : ∀ literal, degree formula literal ≤ bound) : formula.length ≤ (2 * bound) * n := by
  have result := Nat.le_trans (length_le_weight formula nonempty) (weight_le formula bound nodup bounded)
  simpa [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using result

theorem rank_split (items : List α) (rank : α → Nat) (k : Nat)
    (upper : ∀ item ∈ items, rank item ≤ k + 1) :
    items.length = (items.filter (fun item => decide (rank item ≤ k))).length +
      (items.filter (fun item => decide (rank item = k + 1))).length := by
  induction items with
  | nil => simp
  | cons item rest ih =>
    have itemRank := upper item (by simp)
    have restEq := ih (fun a ha => upper a (by simp [ha]))
    by_cases small : rank item ≤ k
    · have other : rank item ≠ k + 1 := by omega
      simp [small, other, restEq, Nat.add_assoc, Nat.add_comm]
    · have other : rank item = k + 1 := by omega
      simp [other, restEq, Nat.add_comm, Nat.add_left_comm]

/-- Elementary counting by positive integer ranks, with multiplicities. -/
theorem length_le_buckets (items : List α) (rank : α → Nat) (k bound : Nat)
    (ranks : ∀ item ∈ items, 0 < rank item ∧ rank item ≤ k)
    (buckets : ∀ j, 0 < j → j ≤ k →
      (items.filter (fun item => decide (rank item = j))).length ≤ bound) :
    items.length ≤ k * bound := by
  induction k generalizing items with
  | zero =>
    have empty : items = [] := by
      cases items with
      | nil => rfl
      | cons item rest => have impossible := ranks item (by simp); omega
    simp [empty]
  | succ k ih =>
    let lower := items.filter (fun item => decide (rank item ≤ k))
    have lowRanks : ∀ item ∈ lower, 0 < rank item ∧ rank item ≤ k := by
      intro item member
      obtain ⟨present, small⟩ := List.mem_filter.mp member
      exact ⟨(ranks item present).1, of_decide_eq_true small⟩
    have lowBuckets : ∀ j, 0 < j → j ≤ k →
        (lower.filter (fun item => decide (rank item = j))).length ≤ bound := by
      intro j positive small
      have sub := (List.filter_sublist (p := fun item => decide (rank item ≤ k)) (l := items)).filter
        (fun item => decide (rank item = j))
      exact Nat.le_trans sub.length_le (buckets j positive (by omega))
    have lowBound := ih lower lowRanks lowBuckets
    have highBound := buckets (k + 1) (by omega) (by omega)
    have split := rank_split items rank k (fun item member => (ranks item member).2)
    rw [split, Nat.add_mul]
    dsimp only [lower] at lowBound
    omega

/-- Occurrences restricted to clauses of one size. -/
def layerDegree (formula : CNF n) (literal : Literal n) (size : Nat) : Nat :=
  ((formula.filter (fun clause => decide (literal ∈ clause))).filter
    (fun clause => decide (clause.length = size))).length

theorem degree_le_layers (formula : CNF n) (k bound : Nat)
    (width : ∀ clause ∈ formula, clause.length ≤ k)
    (bounded : ∀ literal j, 0 < j → j ≤ k → layerDegree formula literal j ≤ bound)
    (literal : Literal n) : degree formula literal ≤ k * bound := by
  apply length_le_buckets _ List.length k bound
  · intro clause member
    obtain ⟨present, occurs⟩ := List.mem_filter.mp member
    have memberLiteral : literal ∈ clause := of_decide_eq_true occurs
    have nonempty : clause ≠ [] := by intro empty; simp [empty] at memberLiteral
    exact ⟨List.length_pos_iff.mpr nonempty, width clause present⟩
  · exact bounded literal

theorem sparse_of_layers (formula : CNF n) (k bound : Nat)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (nonempty : ∀ clause ∈ formula, clause ≠ [])
    (width : ∀ clause ∈ formula, clause.length ≤ k)
    (bounded : ∀ literal j, 0 < j → j ≤ k → layerDegree formula literal j ≤ bound) :
    formula.length ≤ (2 * (k * bound)) * n :=
  sparse formula (k * bound) nodup nonempty (degree_le_layers formula k bound width bounded)

end WordRAM.Conjectures.Sparsification.Counting