Finite line guards and a box invariant for king capture

import Definitions.Def_AngelDevil_Game
import Mathlib.Data.Finset.Insert
import Mathlib.Data.Fintype.Fin
import Mathlib.Data.Fintype.Prod

namespace AngelDevil

def kingOffset (i : Fin 3) : Int := (i.val : Int) - 1

def guardSquare (x : Int) (i : Fin 11) : Int := x + (i.val : Int) - 5

def KingGuard : Nat → Int → Finset Int → Prop
  | 0, x, B => ∃ i : Fin 11, ∀ j : Fin 3,
      x + kingOffset j ∈ insert (guardSquare x i) B
  | n+1, x, B => ∃ i : Fin 11, ∀ j : Fin 3,
      KingGuard n (x + kingOffset j) (insert (guardSquare x i) B)

def kingNormal (s : Fin 4) (p : Point) : Int :=
  if s = 0 then p.1 else if s = 1 then p.2 else if s = 2 then -p.1 else -p.2

def kingTangent (s : Fin 4) (p : Point) : Int :=
  if s = 0 ∨ s = 2 then p.2 else p.1

def kingWallPoint (s : Fin 4) (x : Int) : Point :=
  if s = 0 then (100,x) else if s = 1 then (x,100)
  else if s = 2 then (-100,x) else (x,-100)

@[irreducible] def kingBoard : Finset Point := Finset.univ.image
  (fun p : Fin 201 × Fin 201 => ((p.1.val : Int)-100, (p.2.val : Int)-100))

def kingLineBurns (s : Fin 4) (B : Finset Point) : Finset Int :=
  (B.filter fun p => kingNormal s p = 100).image (kingTangent s)

def kingCorners : List Point := (List.finRange 4).flatMap fun s =>
  (List.range 7).flatMap fun (k : Nat) => [kingWallPoint s (-100+(k:Int)), kingWallPoint s (100-(k:Int))]

def KingLineReady (s : Fin 4) (p : Point) (B : Finset Point) : Prop :=
  ∃ n : Nat, n ≤ 4 ∧ (n:Int)+1 ≤ 100-kingNormal s p ∧
    KingGuard n (kingTangent s p) (kingLineBurns s B)

def KingBoxReady (p : Point) (B : Finset Point) : Prop :=
  (∀ z ∈ kingCorners, z ∈ B) ∧
  (∀ s : Fin 4, kingNormal s p < 100) ∧
  ∀ s : Fin 4, KingLineReady s p B

def kingBurned (s : State) : Finset Point := (s.burned.filterMap id).toFinset

end AngelDevil