-- -*- coding: utf-8 -*-
/-
Copyright (c) 2026 Denise Vella-Chemla (pilotage), Lumo (rédaction).
Released under Apache 2.0 license.
-/

import Mathlib

/-
# Dancing links pour Goldbach : couvertures singleton et décomposants

Formalisation du programme « dancing links » (note de D. Vella-Chemla du
31.12.2018, revisitée novembre 2026).

Encodage :
- les colonnes sont les nombres premiers q tels que q * q ≤ n ;
- les lignes sont les candidats impairs s tels que 3 ≤ s ≤ n et 2 * s ≤ n ;
- une cellule indique que q ne divise ni s ni n-s.

Une couverture singleton (une ligne couvrant toutes les colonnes à elle
seule) est exactement un décomposant de Goldbach s et n-s premiers,
avec les deux inégalités supplémentaires n < s² et n < (n-s)².

Attention : ce fichier formalise les propriétés mathématiques de la
matrice de couverture. Il ne contient pas encore l'algorithme effectif
Dancing Links (suppression et restauration des lignes et colonnes,
recherche récursive).

Le dernier théorème reste volontairement ouvert : le démontrer
reviendrait à établir la conjecture de Goldbach.
-/

namespace DLGoldbach

/-! ## Colonnes et lignes -/

def columns (n : ℕ) : Finset ℕ :=
  (Finset.range (n + 1)).filter
    (fun q => Nat.Prime q ∧ q * q ≤ n)

def rows (n : ℕ) : Finset ℕ :=
  (Finset.Icc 3 n).filter
    (fun s => s % 2 = 1 ∧ 2 * s ≤ n)

theorem mem_columns {n q : ℕ} :
    q ∈ columns n ↔ Nat.Prime q ∧ q * q ≤ n := by
  unfold columns
  rw [Finset.mem_filter, Finset.mem_range, Nat.lt_succ_iff]
  constructor
  · rintro ⟨_, hp, hq⟩
    exact ⟨hp, hq⟩
  · rintro ⟨hp, hq⟩
    refine ⟨?_, hp, hq⟩
    have hq2 : 2 ≤ q := hp.two_le
    nlinarith

theorem mem_rows {n s : ℕ} :
    s ∈ rows n ↔
      3 ≤ s ∧ s ≤ n ∧ s % 2 = 1 ∧ 2 * s ≤ n := by
  unfold rows
  rw [Finset.mem_filter, Finset.mem_Icc]
  tauto

/-! ## Cellules et couvertures -/

def cell (n s q : ℕ) : Prop :=
  ¬ (q ∣ s) ∧ ¬ (q ∣ (n - s))

def singletonCover (n s : ℕ) : Prop :=
  ∀ q ∈ columns n, cell n s q

def exactCover (n : ℕ) (S : Finset ℕ) : Prop :=
  ∀ q ∈ columns n,
    ∃! s, s ∈ S ∧ cell n s q

/-! ## Lemme arithmétique : facteur premier d'un composé -/

lemma exists_prime_factor_sq_le {m : ℕ}
    (h2 : 2 ≤ m) (hnp : ¬ Nat.Prime m) :
    ∃ p, Nat.Prime p ∧ p ∣ m ∧ p * p ≤ m := by
  refine ⟨m.minFac, Nat.minFac_prime (by omega),
    Nat.minFac_dvd m, ?_⟩
  simpa [pow_two] using
    (Nat.minFac_sq_le_self (show 0 < m by omega) hnp)

/-! ## La colonne 2 élimine les lignes paires -/

theorem cell_two_of_odd {n s : ℕ}
    (hne : n % 2 = 0)
    (hs : s % 2 = 1)
    (hle : s ≤ n) :
    cell n s 2 := by
  refine ⟨?_, ?_⟩
  · intro h
    have h0 : s % 2 = 0 :=
      Nat.dvd_iff_mod_eq_zero.mp h
    omega
  · intro h
    have h0 : (n - s) % 2 = 0 :=
      Nat.dvd_iff_mod_eq_zero.mp h
    omega

/-! ## Caractérisation des couvertures singleton -/

theorem singletonCover_iff {n s : ℕ}
    (hn : 6 ≤ n)
    (hs : s ∈ rows n) :
    singletonCover n s ↔
      Nat.Prime s ∧
      Nat.Prime (n - s) ∧
      n < s * s ∧
      n < (n - s) * (n - s) := by
  constructor
  · intro hcov
    obtain ⟨ha, hb, hmod, hmul⟩ := mem_rows.mp hs

    have h2s : 2 ≤ s := by omega
    have hns_pos : 2 ≤ n - s := by omega

    have hsprime : Nat.Prime s := by
      by_contra hcomp
      obtain ⟨p, hp, hdvd, hpq⟩ :=
        exists_prime_factor_sq_le h2s hcomp
      have hcol : p ∈ columns n :=
        (mem_columns).mpr ⟨hp, by
          calc
            p * p ≤ s := hpq
            _ ≤ n := hb⟩
      exact (hcov p hcol).1 hdvd

    have hsq1 : n < s * s := by
      by_contra hle
      have hs_sq : s * s ≤ n := by omega
      have hcol : s ∈ columns n :=
        (mem_columns).mpr ⟨hsprime, hs_sq⟩
      exact (hcov s hcol).1 (dvd_refl s)

    have hnsprime : Nat.Prime (n - s) := by
      by_contra hcomp
      obtain ⟨p, hp, hdvd, hpq⟩ :=
        exists_prime_factor_sq_le hns_pos hcomp
      have hcol : p ∈ columns n :=
        (mem_columns).mpr ⟨hp, by
          calc
            p * p ≤ n - s := hpq
            _ ≤ n := Nat.sub_le _ _⟩
      exact (hcov p hcol).2 hdvd

    have hsq2 : n < (n - s) * (n - s) := by
      by_contra hle
      have hns_sq : (n - s) * (n - s) ≤ n := by omega
      have hcol : n - s ∈ columns n :=
        (mem_columns).mpr ⟨hnsprime, hns_sq⟩
      exact (hcov (n - s) hcol).2 (dvd_refl (n - s))

    exact ⟨hsprime, hnsprime, hsq1, hsq2⟩

  · rintro ⟨hp1, hp2, hg1, hg2⟩ q hq
    obtain ⟨hq1, hq2⟩ := (mem_columns).mp hq
    have hqbig : 2 ≤ q := hq1.two_le

    refine ⟨?_, ?_⟩
    · intro hdvd
      rcases hp1.eq_one_or_self_of_dvd q hdvd with h | h
      · omega
      · rw [h] at hq2
        omega
    · intro hdvd
      rcases hp2.eq_one_or_self_of_dvd q hdvd with h | h
      · omega
      · rw [h] at hq2
        omega

/-! ## Une couverture exacte ne peut avoir qu'une ligne -/

theorem exactCover_is_singleton {n : ℕ}
    (hn : 6 ≤ n)
    (hne : n % 2 = 0)
    {S : Finset ℕ}
    (hS : exactCover n S)
    (hrows : ∀ s ∈ S, s ∈ rows n) :
    ∃ s, S = {s} ∧ singletonCover n s := by

  have h4 : 4 ≤ n := by omega

  have h2col : (2 : ℕ) ∈ columns n :=
    (mem_columns).mpr ⟨Nat.prime_two, h4⟩

  obtain ⟨s, ⟨hsmem, hscell⟩, hsuniq⟩ :=
    hS 2 h2col

  refine ⟨s, ?_, fun q hq => ?_⟩

  · ext t
    rw [Finset.mem_singleton]
    constructor
    · intro ht
      obtain ⟨-, -, htmod, -⟩ :=
        mem_rows.mp (hrows t ht)
      exact hsuniq t
        ⟨ht, cell_two_of_odd hne htmod
          (mem_rows.mp (hrows t ht)).2.1⟩
    · intro ht
      rw [ht]
      exact hsmem

  · obtain ⟨t, ⟨htin, htcell⟩, htuniq⟩ :=
      hS q hq
    have hts : t = s := by
      obtain ⟨-, -, htmod, -⟩ :=
        mem_rows.mp (hrows t htin)
      exact hsuniq t
        ⟨htin, cell_two_of_odd hne htmod
          (mem_rows.mp (hrows t htin)).2.1⟩
    rw [hts] at htcell
    exact htcell

/-! ## Passage de la couverture à Goldbach -/

theorem singletonCover_goldbach {n s : ℕ}
    (hn : 6 ≤ n)
    (hs : s ∈ rows n)
    (hcov : singletonCover n s) :
    Nat.Prime s ∧
    Nat.Prime (n - s) ∧
    s + (n - s) = n := by
  obtain ⟨h1, h2, _, _⟩ :=
    (singletonCover_iff hn hs).mp hcov
  have hs_le : s ≤ n := (mem_rows.mp hs).2.1
  exact ⟨h1, h2, by omega⟩

/-! ## Un petit décomposant ne peut pas être une couverture -/

theorem small_decomposant_not_covered {n p : ℕ}
    (hp : Nat.Prime p)
    (hpq : p * p ≤ n)
    (_ : p ∈ rows n) :
    ¬ singletonCover n p := by
  intro hcov
  have hcol : p ∈ columns n :=
    (mem_columns).mpr ⟨hp, hpq⟩
  exact (hcov p hcol).1 (dvd_refl p)

/-! ## Équivalence avec les décompositions de Goldbach
     satisfaisant les deux inégalités carrées -/

theorem goldbach_above_sq_iff {n : ℕ}
    (hn : 6 ≤ n)
    (hne : n % 2 = 0) :
    (∃ s, s ∈ rows n ∧ singletonCover n s) ↔
      ∃ p, 3 ≤ p ∧
        2 * p ≤ n ∧
        Nat.Prime p ∧
        Nat.Prime (n - p) ∧
        n < p * p ∧
        n < (n - p) * (n - p) := by

  constructor

  · rintro ⟨s, hs, hcov⟩
    obtain ⟨h1, h2, h3, h4⟩ :=
      (singletonCover_iff hn hs).mp hcov
    obtain ⟨ha, hb, -, hmul⟩ :=
      mem_rows.mp hs
    exact ⟨s, ha, hmul, h1, h2, h3, h4⟩

  · rintro ⟨p, h3, hmul, hp1, hp2, hg1, hg2⟩

    have hodd : p % 2 = 1 := by
      have hcases : p % 2 = 0 ∨ p % 2 = 1 := by omega
      rcases hcases with h | h
      · exfalso
        have h2 : (2 : ℕ) ∣ p :=
          Nat.dvd_iff_mod_eq_zero.mpr h
        rcases hp1.eq_one_or_self_of_dvd 2 h2 with h' | h'
        · omega
        · omega
      · exact h

    have hprow : p ∈ rows n :=
      (mem_rows).mpr ⟨h3, by omega, hodd, hmul⟩

    exact ⟨p, hprow,
      (singletonCover_iff hn hprow).mpr
        ⟨hp1, hp2, hg1, hg2⟩⟩

/-! ## Objectif final : existence d'une couverture singleton -/

theorem exists_singletonCover_of_even (n : ℕ)
    (hn : 6 ≤ n)
    (hne : n % 2 = 0) :
    ∃ s, s ∈ rows n ∧ singletonCover n s := by
  sorry -- équivalent à la conjecture de Goldbach ; volontairement ouvert

end DLGoldbach