Documentation

Projects.AP.Defense.Box

def AP.Box.offset :

Equations

AP.Box.offset = 106

Instances For

def AP.Box.interior :

Equations

AP.Box.interior = Set'.ofList (Point.nbhd 0 ↑AP.Box.offset)

Instances For

noncomputable def AP.Box.interiorNC :

Equations

AP.Box.interiorNC = Set'.ofList (idNC (Point.nbhd 0) ↑AP.Box.offset)

Instances For

def AP.Box.interior₁ :

Equations

AP.Box.interior₁ = Set'.ofList (Point.nbhd 0 (↑AP.Box.offset - 1))

Instances For

def AP.Box.corner₀ :

Equations

AP.Box.corner₀ = { dir := Dir.up, offset := { x := ↑AP.Box.offset, y := -↑AP.Box.offset } }

Instances For

def AP.Box.corners :

Equations

AP.Box.corners = List.map (fun (x : ℕ) => AP.Corner.rotRight ^[x] AP.Box.corner₀) (List.range 4)

Instances For

def AP.Box.defenses :

Equations

AP.Box.defenses = List.map (fun (x : AP.Corner) => x.defense) AP.Box.corners

Instances For

def AP.Box.defense :

Equations

AP.Box.defense = AP.Defense.ofList AP.Box.defenses

Instances For

def AP.Box.Cnd (s : State) :

Equations

AP.Box.Cnd s = AP.Box.corner₀.RotCnd s

Instances For

def AP.Box.guardTiles :

Equations

AP.Box.guardTiles = Set'.unionList (List.map (fun (c : AP.Corner) => Set'.ofList (Point.nbhd (c.offset * 103 / 106) 2)) AP.Box.corners)

Instances For

@[simp]

theorem AP.Box.length_corners :

corners.length = 4

@[simp]

theorem AP.Box.length_defenses :

defenses.length = 4

@[simp]

theorem AP.Box.getElem_corners_eq_iter_rotRight {i : ℕ} {h : i < corners.length} :

corners [i] = Corner.rotRight ^[i] corner₀

@[simp]

theorem AP.Box.edge₁_corner₀_dist_zero :

corner₀.edge₁.dist 0 = ↑offset

@[simp]

theorem AP.Box.edge₂_corner₀_dist_zero :

corner₀.edge₂.dist 0 = ↑offset

@[simp]

instance AP.Box.instSquareCorner₀ :

corner₀.Square

@[simp]

instance AP.Box.instSquareGeCorner₀OfNatInt :

corner₀.SquareGe 6

theorem AP.Box.compatible_0_1 :

defenses [0].Compatible defenses [1]

theorem AP.Box.compatible'_0_2 :

Defense.Compatible' Cnd defenses [0] defenses [2]

theorem AP.Box.compatible_0_3 :

defenses [0].Compatible defenses [3]

theorem AP.Box.compatible_1_2 :

defenses [1].Compatible defenses [2]

theorem AP.Box.compatible'_1_3 :

Defense.Compatible' Cnd defenses [1] defenses [3]

theorem AP.Box.compatible_2_3 :

defenses [2].Compatible defenses [3]

theorem AP.Box.compatible_getElem_defenses {i j : ℕ} (h₁ : i < j) (h₂ : j < defenses.length) :

Defense.Compatible' Cnd defenses [i] defenses [j]

theorem AP.Box.cnd_eq_forall_cnd :

Cnd = fun (s : State) => ∀ d ∈ defenses, d.cnd s

theorem AP.Box.compatibleList_defenses :

Defense.CompatibleList defenses

@[simp]

instance AP.Box.instWFDefense :

@[simp]

theorem AP.Box.ps_defense :

defense.ps = Set.univ \ interior₁.toSet

theorem AP.Box.mem_interior₁_of_simulate {s : State} {a : AStrat} {d : DStrat} {n : ℕ} {r : State × ℕ} [hs : sys.WF s] [ha : a.WF] [hd : d.WF] (h₁ : defense.cnd s) (h₂ : sys.simulate { a := a, d := defense.st d }.f s n = r) :

r.1.aPos ∈ interior₁

@[simp]

theorem AP.Box.size_guardTiles :

guardTiles.size = 100

@[simp]

theorem AP.Box.offset_corner₀ :

corner₀.offset = { x := 106, y := -106 }

theorem AP.Box.cnd_defense_iff_guardTiles {s : State} :

defense.cnd s ↔ s.pw = 1 ∧ Point.dist s.aPos 0 ≤ 100 ∧ guardTiles ⊆ s.taken

@[simp]

theorem AP.Box.interior₁_subset_interior :

interior₁ ⊆ interior

@[simp]

theorem AP.Box.guardTiles_subset_interior₁ :

guardTiles ⊆ interior₁

@[simp]

theorem AP.Box.guardTiles_subset_interior :

guardTiles ⊆ interior

theorem AP.Box.le_dist_center_of_mem_guardTiles {p : PointZ} (h : p ∈ guardTiles) :

101 ≤ Point.dist p 0

theorem AP.Box.mem_corners_iff_exi {c : Corner} :

c ∈ corners ↔ ∃ n < 4, Corner.rotRight ^[n] corner₀ = c

theorem AP.Box.f_eq_none_of_aPos_dist_le_and_mem_defenses {s : State} {d : Defense} (h₁ : Point.dist s.aPos 0 ≤ 100) (h₂ : d ∈ defenses) :

d.f s = none

theorem AP.Box.f_eq_none_of_aPos_dist_le {s : State} (h : Point.dist s.aPos 0 ≤ 100) :

defense.f s = none

theorem AP.Box.f_st_eq_of_aPos_dist_le {s : State} {d : DStrat} (h : Point.dist s.aPos 0 ≤ 100) :

(defense.st d).f s = d.f s

theorem AP.Box.cnd_defense_eq_cnd :

defense.cnd = Cnd

theorem AP.Box.guardTiles_subset_taken_of_cnd_defense {s : State} (h : defense.cnd s) :

guardTiles ⊆ s.taken

@[simp]

theorem AP.Box.size_interior :

interior.size = 213 ^ 2

@[simp]

theorem AP.Box.size_interior₁ :

interior₁.size = 211 ^ 2

theorem AP.Box.dist_zero_eq_of_f_eq_some {s : State} {p : PointZ} [hs : sys.WF s] (h : defense.f s = some p) (H₁ : s.aPos ∈ interior₁) (H₂ : guardTiles ⊆ s.taken) :

Point.dist p 0 = 106

theorem AP.Box.mem_interior_of_f_eq_some {s : State} {p : PointZ} [hs : sys.WF s] (h : defense.f s = some p) (H₁ : s.aPos ∈ interior₁) (H₂ : guardTiles ⊆ s.taken) :

theorem AP.Box.interior_eq_interiorNC :

interior = interiorNC