/-!
# Arithmetic on trees of numbers (used in Lemma 1)

`f : Nat → Nat → Bool` is a *tree of numbers* `f(a, b)`, `a = |A∖B|`, `b = |A∩B|`.
-/

namespace AntiDyn

/-- If `f` has no "local step" in the triangle `a + b ≤ k`, it is constant there. -/
theorem const_of_no_step (f : Nat → Nat → Bool) (k : Nat)
    (h : ∀ a b, a + b ≤ k → (1 ≤ a → f (a-1) b = f a b) ∧ (1 ≤ b → f a (b-1) = f a b)) :
    ∀ a b, a + b ≤ k → f a b = f 0 0 := by
  have h1 : ∀ b a, a + b ≤ k → f a b = f 0 b := by
    intro b a
    induction a with
    | zero => intro _; rfl
    | succ a ih =>
      intro hab
      have := (h (a+1) b hab).1 (by omega)
      simp at this
      rw [← this]
      exact ih (by omega)
  have h2 : ∀ b, b ≤ k → f 0 b = f 0 0 := by
    intro b
    induction b with
    | zero => intro _; rfl
    | succ b ih =>
      intro hb
      have := (h 0 (b+1) (by omega)).2 (by omega)
      simp at this
      rw [← this]
      exact ih (by omega)
  intro a b hab
  rw [h1 b a hab, h2 b (by omega)]

/-- Discrete intermediate value lemma. -/
theorem ivt (g : Nat → Bool) : ∀ (d lo : Nat), 0 < d → g lo ≠ g (lo + d) →
    ∃ x, lo ≤ x ∧ x < lo + d ∧ g x ≠ g (x + 1) := by
  intro d
  induction d with
  | zero => intro lo h; omega
  | succ d ih =>
    intro lo _ hne
    by_cases h : g lo = g (lo + 1)
    · have hd : 0 < d := Nat.pos_of_ne_zero (fun h0 => by subst h0; exact hne h)
      have : g (lo + 1) ≠ g (lo + 1 + d) := by
        intro e; apply hne; rw [h, e]; congr 1; omega
      obtain ⟨x, hx1, hx2, hx3⟩ := ih (lo + 1) hd this
      exact ⟨x, by omega, by omega, hx3⟩
    · exact ⟨lo, Nat.le_refl _, by omega, h⟩

/-- **Paper, proof of Lemma 1(i)** (Cases 1 and 2, with the repaired Case 2).
If `f` is not constant on the triangle `a + b ≤ n`, and `k < n` (some individual lies outside
`P`, `|P| = k`), then there are `(a, b)` and `(i, j)` such that removing `i` non-`Y` and
`j` `Y`-elements of `X` lying outside `P` changes the value of `f`, where the remaining
elements of `X` (`a + b - i - j` of them) all fit in `P`, and at most `n - k` elements
lie outside `P`. -/
theorem find_step (f : Nat → Nat → Bool) (n k : Nat) (hk : k < n)
    (htri : ∃ a b a' b', a + b ≤ n ∧ a' + b' ≤ n ∧ f a b ≠ f a' b') :
    ∃ a b i j, i ≤ a ∧ j ≤ b ∧ a + b - (i + j) ≤ k ∧ i + j ≤ n - k ∧
      f (a - i) (b - j) ≠ f a b := by
  by_cases hA : ∃ a b, a + b ≤ k ∧ ((1 ≤ a ∧ f (a-1) b ≠ f a b) ∨ (1 ≤ b ∧ f a (b-1) ≠ f a b))
  · -- Case 1 of the paper: a local step inside the small triangle
    obtain ⟨a, b, hab, h | h⟩ := hA
    · exact ⟨a, b, 1, 0, h.1, by omega, by omega, by omega, by simpa using h.2⟩
    · exact ⟨a, b, 0, 1, by omega, h.1, by omega, by omega, by simpa using h.2⟩
  · -- Case 2: constant on the small triangle
    have hc := const_of_no_step f k (fun a b hab =>
      ⟨fun h1 => Classical.byContradiction fun hne => hA ⟨a, b, hab, Or.inl ⟨h1, hne⟩⟩,
       fun h1 => Classical.byContradiction fun hne => hA ⟨a, b, hab, Or.inr ⟨h1, hne⟩⟩⟩)
    obtain ⟨a1, b1, a2, b2, h1, h2, hne⟩ := htri
    have : ∃ a b, a + b ≤ n ∧ f a b ≠ f 0 0 := by
      by_cases e : f a1 b1 = f 0 0
      · exact ⟨a2, b2, h2, fun e2 => hne (e.trans e2.symm)⟩
      · exact ⟨a1, b1, h1, e⟩
    obtain ⟨a, b, hab, hne0⟩ := this
    have hbig : k < a + b := by
      by_cases hh : k < a + b
      · exact hh
      · exact absurd (hc a b (by omega)) hne0
    refine ⟨a, b, min a (a + b - k), (a + b - k) - min a (a + b - k), by omega, by omega, by omega,
      by omega, ?_⟩
    rw [hc _ _ (by omega)]
    exact fun e => hne0 e.symm


/-- **The gap in the paper's Case 2 / Zone B** (p. 347).  With `|P| = k = 2`, `n = 8` and
`f(a,b) = [a + b > 2]` (constant on the small triangle `a + b ≤ 2`, non-constant on the big
one), the point `(a*, b*) = (3, 3)` lies in "Zone B" (`b* > |P|`), yet there is *no*
`c` with `0 < c ≤ min(b*, n - |P|)` and `f(a*, b* - c) ≠ f(a*, b*)`: the "horizontal projection
onto the line `a + b = |P|`" does not exist because `a* = 3 > |P|`.  (The lemma's conclusion
still holds: `find_step` produces `(i, j) = (2, 2)`.) -/
theorem paper_zoneB_step_fails :
    let f : Nat → Nat → Bool := fun a b => decide (2 < a + b)
    f 3 3 ≠ f 0 0 ∧ (∀ a b, a + b ≤ 2 → f a b = f 0 0) ∧
    ¬ ∃ c, 0 < c ∧ c ≤ 3 ∧ c ≤ 8 - 2 ∧ f 3 (3 - c) ≠ f 3 3 := by
  intro f
  refine ⟨by decide, ?_, ?_⟩
  · intro a b h; simp [f]; omega
  · rintro ⟨c, h1, h2, h3, h4⟩
    apply h4
    simp only [f]
    have : 2 < 3 + (3 - c) := by omega
    simp [this]

/-- ... while the corrected argument (`find_step`) does find a refuting pair for that `f`. -/
theorem zoneB_repaired :
    ∃ a b i j, i ≤ a ∧ j ≤ b ∧ a + b - (i + j) ≤ 2 ∧ i + j ≤ 8 - 2 ∧
      (fun a b => decide (2 < a + b)) (a - i) (b - j) ≠ (fun a b => decide (2 < a + b)) a b :=
  find_step (fun a b => decide (2 < a + b)) 8 2 (by omega) ⟨0, 0, 3, 3, by omega, by omega, by decide⟩

end AntiDyn