Projects.AP.Defense.Corner.Rotation

source

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

Corner

Equations

c.rotRight = { dir := c.dir.rotRight, offset := AP.rotRight.ft c.offset }

Instances For

source

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

Corner

Equations

c.rotLeft = { dir := c.dir.rotLeft, offset := AP.rotLeft.ft c.offset }

Instances For

source

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

Corner

Equations

c.rot180 = { dir := c.dir⁻¹, offset := AP.rot180.ft c.offset }

Instances For

source

@[simp]

theorem AP.Corner.rotRight_mk {dir : Dir} {offset : PointZ} :

{ dir := dir, offset := offset }.rotRight = { dir := dir.rotRight, offset := rotRight.ft offset }

source

@[simp]

theorem AP.Corner.rotLeft_mk {dir : Dir} {offset : PointZ} :

{ dir := dir, offset := offset }.rotLeft = { dir := dir.rotLeft, offset := rotLeft.ft offset }

source

@[simp]

theorem AP.Corner.rot180_mk {dir : Dir} {offset : PointZ} :

{ dir := dir, offset := offset }.rot180 = { dir := dir⁻¹, offset := rot180.ft offset }

source

@[simp]

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

c.rotRight.edge₁ = c.edge₂

source

@[simp]

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

c.rotLeft.edge₂ = c.edge₁

source

theorem AP.Corner.false_of_f_edge₁_rotLeft_rotRight_eq_some {c : Corner} {s : State} {p₁ p₂ : PointZ} [h : c.SquareGe 6] (h₁ : c.rotLeft.edge₁.defense.f s = some p₁) (h₂ : c.rotRight.edge₁.defense.f s = some p₂) :

False

source

theorem AP.Corner.false_of_f_edge₂_rotLeft_rotRight_eq_some {c : Corner} {s : State} {p₁ p₂ : PointZ} [h : c.SquareGe 6] (h₁ : c.rotLeft.edge₂.defense.f s = some p₁) (h₂ : c.rotRight.edge₂.defense.f s = some p₂) :

False

source

theorem AP.Corner.compatible_rotRight {c : Corner} [h : c.SquareGe 6] :

c.defense.Compatible c.rotRight.defense

source

@[simp]

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

c.rotRight.rotRight = c.rot180

source

@[simp]

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

c.rotLeft.rotLeft = c.rot180

source

@[simp]

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

c.rotRight.rotLeft = c

source

@[simp]

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

c.rotLeft.rotRight = c

source

@[simp]

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

c.rot180.edge₁ = c.edge₁.rot180

source

@[simp]

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

c.rot180.edge₂ = c.edge₂.rot180

source

@[simp]

instance AP.Corner.instSquareRotRight {c : Corner} [h : c.Square] :

c.rotRight.Square

source

@[simp]

instance AP.Corner.instSquareRotLeft {c : Corner} [h : c.Square] :

c.rotLeft.Square

source

@[simp]

instance AP.Corner.instSquareRot180 {c : Corner} [h : c.Square] :

c.rot180.Square

source

@[simp]

instance AP.Corner.instSquareGeRotRight {c : Corner} {d : ℤ} [h : c.SquareGe d] :

c.rotRight.SquareGe d

source

@[simp]

instance AP.Corner.instSquareGeRotLeft {c : Corner} {d : ℤ} [h : c.SquareGe d] :

c.rotLeft.SquareGe d

source

@[simp]

instance AP.Corner.instSquareGeRot180 {c : Corner} {d : ℤ} [h : c.SquareGe d] :

c.rot180.SquareGe d

source

theorem AP.Corner.compatible_rotLeft {c : Corner} [h : c.SquareGe 6] :

c.defense.Compatible c.rotLeft.defense

source

@[simp]

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

c.rotLeft.edge₁ = c.edge₁.rotLeft

source

@[simp]

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

c.rotRight.edge₂ = c.edge₂.rotRight

source

theorem AP.Corner.edge₁_rotRight' {c : Corner} :

c.rotRight.edge₁ = c.edge₁.rotRight

source

theorem AP.Corner.edge₂_rotLeft' {c : Corner} :

c.rotLeft.edge₂ = c.edge₂.rotLeft

source

@[simp]

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

c.rotRight.rot180 = c.rotLeft

source

theorem AP.Corner.cnd'_of_cnd {c : Corner} {s : State} (h : c.cnd s) :

c.cnd' s

source

theorem AP.Corner.cnd'_of_cnd_defense {c : Corner} {s : State} (h : c.defense.cnd s) :

c.cnd' s

source

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

Prop

Equations

c.RotCnd s = ∀ (n : ℕ), (AP.Corner.rotRight ^[n] c).defense.cnd s

Instances For

source

theorem AP.Corner.compatible'_rot180 {c : Corner} [h : c.SquareGe 6] :

Defense.Compatible' c.RotCnd c.defense c.rot180.defense

source

@[simp]

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

c.rot180.rotRight = c.rotLeft

source

@[simp]

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

c.rot180.rotLeft = c.rotRight

source

@[simp]

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

c.rotLeft.rot180 = c.rotRight

source

@[simp]

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

c.rot180.rot180 = c

source

@[simp]

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

c.rotRight.RotCnd = c.RotCnd

source

theorem AP.Corner.iter_rotRight_eq_mod_4 {n : ℕ} :

Corner.rotRight ^[n] = Corner.rotRight ^[n % 4]

source

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

c.RotCnd = fun (s : State) => c.defense.cnd s ∧ c.rotRight.defense.cnd s ∧ c.rot180.defense.cnd s ∧ c.rotLeft.defense.cnd s