Documentation

Projects.AP.Defense.Corner.Basic

structure AP.Corner :

dir : Dir
offset : PointZ

Instances For

theorem AP.Corner.ext_iff {x y : Corner} :

x = y ↔ x.dir = y.dir ∧ x.offset = y.offset

theorem AP.Corner.ext {x y : Corner} (dir : x.dir = y.dir) (offset : x.offset = y.offset) :

x = y

@[instance_reducible]

instance AP.instInhabitedCorner :

Inhabited Corner

Equations

AP.instInhabitedCorner = { default := AP.instInhabitedCorner.default }

def AP.instDecidableEqCorner.decEq (x✝ x✝¹ : Corner) :

Decidable (x✝ = x✝¹)

Equations

AP.instDecidableEqCorner.decEq { dir := a, offset := a_1 } { dir := b, offset := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

@[instance_reducible]

instance AP.instDecidableEqCorner :

DecidableEq Corner

Equations

AP.instDecidableEqCorner = AP.instDecidableEqCorner.decEq

def AP.Corner.edge (dir : Dir) (offset : PointZ) :

Equations

AP.Corner.edge dir offset = { dir := dir, offset := Point.coord' offset dir }

Instances For

def AP.Corner.edge₁ (c : Corner) :

Equations

c.edge₁ = AP.Corner.edge c.dir c.offset

Instances For

def AP.Corner.edge₂ (c : Corner) :

Equations

c.edge₂ = AP.Corner.edge c.dir.rotRight c.offset

Instances For

def AP.Corner.points (c : Corner) :

Equations

c.points = c.edge₁.points ∪ c.edge₂.points

Instances For

def AP.Corner.memPoints (c : Corner) (p : PointZ) :

Equations

c.memPoints { x := cx, y := cy } = match c.offset with | { x := cx_1, y := cy_1 } => match c.dir with | Dir.up => decide (cy ≤ cy_1 ∨ cx_1 ≤ cx) | Dir.right => decide (cx_1 ≤ cx ∨ cy_1 ≤ cy) | Dir.down => decide (cy_1 ≤ cy ∨ cx ≤ cx_1) | Dir.left => decide (cx ≤ cx_1 ∨ cy ≤ cy_1)

Instances For

theorem AP.Corner.mem_points_iff_memPoints {c : Corner} {p : PointZ} :

p ∈ c.points ↔ c.memPoints p = true

@[instance_reducible]

instance AP.Corner.instDecidableMemPointZSetPoints {c : Corner} {p : PointZ} :

Decidable (p ∈ c.points)

Equations

AP.Corner.instDecidableMemPointZSetPoints = decidable_of_bool (c.memPoints p) ⋯

@[simp]

theorem AP.Corner.memPoints_eq {c : Corner} {p : PointZ} :

c.memPoints p = decide (p ∈ c.points)

def AP.Corner.dist (c : Corner) (p : PointZ) :

Equations

c.dist p = min (c.edge₁.dist p) (c.edge₂.dist p)

Instances For

def AP.Corner.cnd' (c : Corner) (s : State) :

Equations

c.cnd' s = ∀ (p : PointZ), have d₁ := c.edge₁.dist p; have d₂ := c.edge₂.dist p; 1 ≤ d₁ → d₁ ≤ 5 → 1 ≤ d₂ → d₂ ≤ 5 → p ∈ s.taken

Instances For

def AP.Corner.cnd (c : Corner) (s : State) :

Equations

c.cnd s = (s.pw = 1 ∧ 6 ≤ c.dist s.aPos ∧ c.cnd' s)

Instances For

def AP.Corner.f (c : Corner) (s : State) :

Equations

c.f s = (c.edge₁.defense.f s <|> c.edge₂.defense.f s)

Instances For

def AP.Corner.defense (c : Corner) :

Equations

c.defense = { cnd := c.cnd, ps := c.points, f := c.f }

Instances For

theorem AP.Corner.cnd_defense_edge₁ {c : Corner} {s : State} (h : c.cnd s) :

c.edge₁.defense.cnd s

theorem AP.Corner.cnd_defense_edge₂ {c : Corner} {s : State} (h : c.cnd s) :

c.edge₂.defense.cnd s

@[simp]

theorem AP.Corner.ps_defense {c : Corner} :

c.defense.ps = c.points

@[simp]

theorem AP.Corner.f_defense {c : Corner} :

c.defense.f = c.f

theorem AP.Corner.edge₁_hor_iff {c : Corner} :

c.edge₁.dir.hor ↔ c.edge₂.dir.vert

theorem AP.Corner.edge₂_hor_iff {c : Corner} :

c.edge₂.dir.hor ↔ c.edge₁.dir.vert

theorem AP.Corner.edge₁_vert_iff {c : Corner} :

c.edge₁.dir.vert ↔ c.edge₂.dir.hor

theorem AP.Corner.edge₂_vert_iff {c : Corner} :

c.edge₂.dir.vert ↔ c.edge₁.dir.hor

theorem AP.Corner.cnd'_of_reachable {c : Corner} {s s' : State} [hs : sys.WF s] (h₁ : sys.Reachable s s') (h₂ : c.cnd' s) :

c.cnd' s'

theorem AP.Corner.f_edge₂_eq_none_of_f_edge₁_eq_some {c : Corner} {s : State} {p : PointZ} [hs : sys.WF s] (H : c.cnd' s) (h : c.edge₁.defense.f s = some p) :

c.edge₂.defense.f s = none

theorem AP.Corner.f_edge₁_eq_none_of_f_edge₂_eq_some {c : Corner} {s : State} {p : PointZ} [hs : sys.WF s] (H : c.cnd' s) (h : c.edge₂.defense.f s = some p) :

c.edge₁.defense.f s = none

@[simp]

theorem AP.Corner.validTr_defense {c : Corner} :

c.defense.ValidTr

theorem AP.Corner.wf_defense {c : Corner} :

@[simp]

instance AP.Corner.instWFDefense {c : Corner} :

theorem AP.Corner.of_f_eq_some {c : Corner} {s : State} {p : PointZ} (h : c.defense.f s = some p) :

c.edge₁.defense.f s = some p ∨ c.edge₂.defense.f s = some p

theorem AP.Corner.f_eq_some_iff_of_cnd' {c : Corner} {s : State} {p : PointZ} [hs : sys.WF s] (h : c.cnd' s) :

c.defense.f s = some p ↔ c.edge₁.defense.f s = some p ∨ c.edge₂.defense.f s = some p

class AP.Corner.Square (c : Corner) :

h : c.edge₁.dist 0 = c.edge₂.dist 0

Instances

class AP.Corner.SquareEx (c : Corner) (d : ℤ) extends c.Square :

h : c.edge₁.dist 0 = c.edge₂.dist 0
h₁ : c.edge₁.dist 0 = d

Instances

class AP.Corner.SquareLe (c : Corner) (d : ℤ) extends c.Square :

h : c.edge₁.dist 0 = c.edge₂.dist 0
h₁ : c.edge₁.dist 0 ≤ d

Instances

class AP.Corner.SquareGe (c : Corner) (d : ℤ) extends c.Square :

h : c.edge₁.dist 0 = c.edge₂.dist 0
h₁ : d ≤ c.edge₁.dist 0

Instances

theorem AP.Corner.square_iff {c : Corner} :

c.Square ↔ c.edge₁.dist 0 = c.edge₂.dist 0

theorem AP.Corner.square_iff_offset_x_eq {c : Corner} :

c.Square ↔ c.offset.x = c.offset.y * if c.dir.vert then -1 else 1

@[simp]

theorem AP.Corner.rotRight_edge₁ {c : Corner} [h : c.Square] :

c.edge₁.rotRight = c.edge₂

@[simp]

theorem AP.Corner.rotLeft_edge₂ {c : Corner} [h : c.Square] :

c.edge₂.rotLeft = c.edge₁

@[simp]

theorem AP.Corner.edge₁_dist_of_squareEx {c : Corner} {d : ℤ} [h : c.SquareEx d] :

c.edge₁.dist 0 = d

@[simp]

theorem AP.Corner.edge₁_dist_of_squareLe {c : Corner} {d : ℤ} [h : c.SquareLe d] :

c.edge₁.dist 0 ≤ d

@[simp]

theorem AP.Corner.edge₁_dist_of_squareGe {c : Corner} {d : ℤ} [h : c.SquareGe d] :

d ≤ c.edge₁.dist 0

@[simp]

theorem AP.Corner.edge₂_dist_of_squareEx {c : Corner} {d : ℤ} [h : c.SquareEx d] :

c.edge₂.dist 0 = d

@[simp]

theorem AP.Corner.edge₂_dist_of_squareLe {c : Corner} {d : ℤ} [h : c.SquareLe d] :

c.edge₂.dist 0 ≤ d

@[simp]

theorem AP.Corner.edge₂_dist_of_squareGe {c : Corner} {d : ℤ} [h : c.SquareGe d] :

d ≤ c.edge₂.dist 0

theorem AP.Corner.false_of_edge₁_edge₂_eq_some {c : Corner} {s : State} {p₁ p₂ : PointZ} [hs : sys.WF s] (H : c.cnd' s) (h₁ : c.edge₁.defense.f s = some p₁) (h₂ : c.edge₂.defense.f s = some p₂) :