/-
  Formalisation 4 lettres - 16 règles : impossibilité de prouver Goldbach
  par ce seul formalisme.

  Lean 4, sans Mathlib (bibliothèque standard seulement).
  Correspond à impossibilite_4lettres_16regles.tex.

  Convention : le mot de n est la suite des lettres des couples (x, n-x),
  x impair, 3 <= x <= n/2. La k-ième lettre (k = 0, 1, ...) correspond à
  x = 2k+3. S : Nat -> Bool est l'ensemble « des premiers » (ici arbitraire).
-/

/-- Les quatre lettres : a = (S,S), b = (non S, S), c = (S, non S), d = (non S, non S). -/
inductive L where
  | a | b | c | d
  deriving DecidableEq, Repr

/-- La lettre associée au couple de booléens (u, v). -/
def letter (u v : Bool) : L :=
  match u, v with
  | true,  true  => L.a
  | false, true  => L.b
  | true,  false => L.c
  | false, false => L.d

/-- Les 16 règles de réécriture. -/
def rule : L → L → L
  | .a, .a => .a | .a, .b => .b | .a, .c => .a | .a, .d => .b
  | .b, .a => .a | .b, .b => .b | .b, .c => .a | .b, .d => .b
  | .c, .a => .c | .c, .b => .d | .c, .c => .c | .c, .d => .d
  | .d, .a => .c | .d, .b => .d | .d, .c => .c | .d, .d => .d

/-- Bande rectangulaire : (u,v) · (x,y) = (x,v). -/
theorem rule_letter (u v x y : Bool) :
    rule (letter u v) (letter x y) = letter x v := by
  cases u <;> cases v <;> cases x <;> cases y <;> rfl

/-- Lettre numéro k du mot de n, pour l'ensemble S (couple (2k+3, n-(2k+3))). -/
def letterAt (S : Nat → Bool) (n k : Nat) : L :=
  letter (S (2 * k + 3)) (S (n - (2 * k + 3)))

/-- Longueur du mot de n : nombre d'impairs x avec 3 <= x <= n/2. -/
def len (n : Nat) : Nat := (n / 2 + 1) / 2 - 1

/-- Le mot de n, pour l'ensemble S. -/
def word (S : Nat → Bool) (n : Nat) : List L :=
  (List.range (len n)).map (fun k => letterAt S n k)

/-! ## Proposition 1 : les 16 règles sont vraies pour TOUT ensemble S -/

/-- Réécrire deux lettres consécutives du mot de n donne la lettre
    correspondante du mot de n+2 (une position plus loin). Aucune hypothèse sur S. -/
theorem regles_pour_tout_S (S : Nat → Bool) (n k : Nat) :
    rule (letterAt S n k) (letterAt S n (k + 1)) = letterAt S (n + 2) (k + 1) := by
  have h : n + 2 - (2 * (k + 1) + 3) = n - (2 * k + 3) := by omega
  first
    | (simp only [letterAt, rule_letter, h]; done)
    | (unfold letterAt; rw [h]; exact rule_letter _ _ _ _)
    | (unfold letterAt; rw [rule_letter, h])

/-! ## Proposition 2 : un contre-modèle sans lettre a -/

/-- S4 = les entiers congrus à 3 modulo 4. -/
def S4 (x : Nat) : Bool := decide (x % 4 = 3)

theorem letter_eq_a (u v : Bool) :
    letter u v = L.a ↔ (u = true ∧ v = true) := by
  cases u <;> cases v <;> first | decide | simp [letter]

/-- Pour n ≡ 0 mod 4, le mot de n n'a aucune lettre a, dans le modèle S4. -/
theorem pas_de_a_mod4 (n : Nat) (hn : n % 4 = 0) (k : Nat) :
    letterAt S4 n k ≠ L.a := by
  intro h
  unfold letterAt at h
  rw [letter_eq_a] at h
  obtain ⟨h1, h2⟩ := h
  have h1' : (2 * k + 3) % 4 = 3 := of_decide_eq_true h1
  have h2' : (n - (2 * k + 3)) % 4 = 3 := of_decide_eq_true h2
  omega

/-! ## Corollaire : le formalisme (16 règles) n'implique pas l'existence d'un a -/

/-- Il existe un modèle S dans lequel les 16 règles sont vraies pour tous n, k,
    et où le mot de tout multiple de 4 n'a aucun a. -/
theorem formalisme_sans_a :
    ∃ S : Nat → Bool,
      (∀ n k, rule (letterAt S n k) (letterAt S n (k + 1)) = letterAt S (n + 2) (k + 1)) ∧
      (∀ n, n % 4 = 0 → ∀ k, letterAt S n k ≠ L.a) :=
  ⟨S4, regles_pour_tout_S S4, fun n hn k => pas_de_a_mod4 n hn k⟩

/-! ## Cas de base : il utilise les vrais nombres premiers -/

/-- Primalité décidable simple (suffisante pour les petits cas de base). -/
def isPrimeB (n : Nat) : Bool :=
  decide (2 ≤ n) && (List.range (n - 2)).all (fun i => n % (i + 2) != 0)

/-- Avec les vrais premiers : 6 = 3 + 3 et 8 = 3 + 5 donnent la lettre a. -/
example : letterAt isPrimeB 6 0 = L.a := by first | decide | rfl | native_decide
example : letterAt isPrimeB 8 0 = L.a := by first | decide | rfl | native_decide

/-- Dans le modèle S4, le mot de 8 est c (3 ∈ S4, 5 ∉ S4) : le cas de base de la
    descente échoue, sans contradiction. -/
example : letterAt S4 8 0 = L.c := by first | decide | rfl | native_decide