structure AP.Edge : Type

• dir : Dir
• offset : ℤ

theorem AP.Edge.ext_iff {x y : Edge} : x = y ↔ x.dir = y.dir ∧ x.offset = y.offset

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

@[instance_reducible]

instance AP.instInhabitedEdge : Inhabited Edge

Equations

• AP.instInhabitedEdge = { default := AP.instInhabitedEdge.default }

def AP.instDecidableEqEdge.decEq (x✝ x✝¹ : Edge) : Decidable (x✝ = x✝¹)

Equations

• AP.instDecidableEqEdge.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 ⋯

@[instance_reducible]

instance AP.instDecidableEqEdge : DecidableEq Edge

Equations

• AP.instDecidableEqEdge = AP.instDecidableEqEdge.decEq

def AP.Edge.hor (e : Edge) : Prop

Equations

• e.hor = e.dir.vert

def AP.Edge.vert (e : Edge) : Prop

Equations

• e.vert = e.dir.hor

@[instance_reducible]

instance AP.Edge.instDecidableHor {e : Edge} : Decidable e.hor

Equations

• AP.Edge.instDecidableHor = id inferInstance

@[instance_reducible]

instance AP.Edge.instDecidableVert {e : Edge} : Decidable e.vert

Equations

• AP.Edge.instDecidableVert = id inferInstance

def AP.Edge.memPoints (e : Edge) (p : PointZ) : Bool

Equations

• e.memPoints p = match e.dir with | Dir.up => decide (p.y ≤ e.offset) | Dir.right => decide (e.offset ≤ p.x) | Dir.down => decide (e.offset ≤ p.y) | Dir.left => decide (p.x ≤ e.offset)

def AP.Edge.points (e : Edge) : Set PointZ

Equations

• e.points = {p : PointZ | e.memPoints p = true}

def AP.Edge.dist (e : Edge) (p : PointZ) : ℤ

Equations

• e.dist p = match e.dir with | Dir.up => p.y - e.offset | Dir.down => e.offset - p.y | Dir.left => p.x - e.offset | Dir.right => e.offset - p.x

def AP.Edge.getBorderPoint (e : Edge) (p : PointZ) (d : ℤ) : PointZ

Equations

• e.getBorderPoint p d = match e.dir with | Dir.up => { x := p.x - d, y := e.offset } | Dir.down => { x := p.x + d, y := e.offset } | Dir.left => { x := e.offset, y := p.y + d } | Dir.right => { x := e.offset, y := p.y - d }

def AP.Edge.getBorderPoint₀ (e : Edge) (p : PointZ) : PointZ

Equations

• e.getBorderPoint₀ p = e.getBorderPoint p 0

def AP.Edge.getBorderPoints (e : Edge) (p : PointZ) (d : ℕ) : List PointZ

Equations

• e.getBorderPoints p d = [e.getBorderPoint p (-↑d), e.getBorderPoint p ↑d]

def AP.Edge.ptsArr (e : Edge) (s : State) (start : ℤ) (len : ℕ) : Array Bool

Equations

• e.ptsArr s start len = { toList := List.map (fun (i : ℤ) => decide (e.getBorderPoint s.aPos (start + i) ∈ s.taken)) do let a ← List.range len pure ↑a }

def AP.Edge.cndMp : Map ℤ (List (Array Bool))

Equations

• AP.Edge.cndMp = Map.ofList (List.map (fun (x : ℤ × List String) => match x with | (d, xs) => (fun (x : List (Array Bool)) => (d, x)) (List.map (fun (s : String) => { toList := List.map (fun (x : Char) => '1' == x) s.toList }) xs)) [(1, ["0011100"]), (2, ["0101100", "0011010"]), (3, ["1010010", "1001100", "0110010", "0100110", "0100101", "0011001"]), (4, ["0100100", "0100010", "0011000", "0010010", "0001100"]), (5, ["0010000", "0001000", "0000100"])])

def AP.Edge.cnd (d : ℤ) (f : ℕ → Bool) : Bool

Equations

• AP.Edge.cnd d f = match Map.get? d AP.Edge.cndMp with | none => true | some xs => xs.any fun (arr : Array Bool) => decide (∀ (i : Fin 7), arr[i]? = some true → f ↑i = true)

def AP.Edge.f₅ (f : ℕ → Bool) (n : Option ℕ) : ℕ

Equations

• AP.Edge.f₅ f (some n_2) = n_2
• AP.Edge.f₅ f none = (List.find? (fun (x : ℕ) => !f x) (List.range 7)).getD 0

def AP.Edge.f₄ (d : ℤ) (f : ℕ → Bool) : ℕ

Equations

• AP.Edge.f₄ d f = AP.Edge.f₅ f (List.find? (fun (i : ℕ) => AP.Edge.cnd d fun (k : ℕ) => if (k == i) = true then true else f k) (List.range 7))

def AP.Edge.f₃ (d : ℤ) (f : ℕ → Bool) : Option ℕ

Equations

• AP.Edge.f₃ d f = if (decide (d ≤ 0) || decide (6 ≤ d) || AP.Edge.cnd d f) = true then none else some (AP.Edge.f₄ d f)

def AP.Edge.f₂ (d : ℤ) (arr : Array Bool) (offset : ℕ) : Option ℕ

Equations

• AP.Edge.f₂ d arr offset = AP.Edge.f₃ d fun (i : ℕ) => arr[offset + i]?.getD false

def AP.Edge.f₁ (e : Edge) (s : State) : Option PointZ

Equations

• e.f₁ s = do let i ← AP.Edge.f₂ (e.dist s.aPos) (e.ptsArr s (-3) 7) 0 pure (e.getBorderPoint s.aPos (↑i - 3))

def AP.Edge.f (e : Edge) (s : State) : Option PointZ

Equations

• e.f s = do let p ← e.f₁ s guard (p ≠ s.aPos) guard (p ∉ s.taken) pure p

def AP.Edge.defense (e : Edge) : Defense

Equations

• e.defense = { cnd := fun (s : AP.State) => s.pw = 1 ∧ 6 ≤ e.dist s.aPos, ps := e.points, f := e.f }

def AP.Edge.edge₀ : Edge

Equations

• AP.Edge.edge₀ = { dir := Dir.down, offset := 0 }