Projects.AP.Symmetry.Rotation

source

def AP.rotRight :

sys.Symmetry

Equations

AP.rotRight = AP.mkSym { toFun := fun (p : PointZ) => { x := -p.y, y := p.x }, invFun := fun (p : PointZ) => { x := p.y, y := -p.x }, left_inv := AP.rotRight._proof_1, right_inv := AP.rotRight._proof_2 }

Instances For

source

theorem AP.rotRight.cnd_initial_fs_iff {s : State} :

sys.Initial (rotRight.fs s) ↔ sys.Initial s

source

theorem AP.rotRight.cnd_tr_eq {s : State} {p : PointZ} :

sys.tr s p = Option.map (⇑rotRight.fs') (sys.tr (rotRight.fs s) (rotRight.ft p))

source

@[simp]

instance AP.instWFStatePointZRotRight :

rotRight.WF

source

def AP.rotLeft :

sys.Symmetry

Equations

AP.rotLeft = AP.rotRight ⁻¹

Instances For

source

@[simp]

instance AP.instWFStatePointZRotLeft :

rotLeft.WF

source

def AP.rot180 :

sys.Symmetry

Equations

AP.rot180 = AP.rotRight ^ 2

Instances For

source

@[simp]

instance AP.instWFStatePointZRot180 :

rot180.WF

source

@[simp]

theorem AP.rotRight_mul_rotRight :

rotRight * rotRight = rot180

source

@[simp]

theorem AP.rotRight_mul_rotLeft :

rotRight * rotLeft = 1

source

@[simp]

theorem AP.rotLeft_mul_rotRight :

rotLeft * rotRight = 1

source

theorem AP.inv_rot180 :

rot180 ⁻¹ = rot180

source

instance AP.instSelfInverseStatePointZRot180 :

rot180.SelfInverse

source

@[simp]

theorem AP.rotLeft_mul_rotLeft :

rotLeft * rotLeft = rot180

source

@[simp]

theorem AP.rotRight_pow_two :

rotRight ^ 2 = rot180

source

@[simp]

theorem AP.rotLeft_pow_two :

rotLeft ^ 2 = rot180

source

@[simp]

theorem AP.rotRight_pow_three :

rotRight ^ 3 = rotLeft

source

@[simp]

theorem AP.rotLeft_pow_three :

rotLeft ^ 3 = rotRight

source

@[simp]

theorem AP.rot180_mul_rot180 :

rot180 * rot180 = 1

source

@[simp]

theorem AP.rot180_pow_two :

rot180 ^ 2 = 1

source

@[simp]

theorem AP.rotRight_pow_four :

rotRight ^ 4 = 1

source

@[simp]

theorem AP.rotLeft_pow_four :

rotLeft ^ 4 = 1

source

@[simp]

theorem AP.inv_rotRight :

rotRight ⁻¹ = rotLeft

source

@[simp]

theorem AP.inv_rotLeft :

rotLeft ⁻¹ = rotRight

source

@[simp]

instance AP.instBasicSymRotRight :

BasicSym rotRight

source

@[simp]

instance AP.instBasicSymRotLeft :

BasicSym rotLeft

source

@[simp]

instance AP.instBasicSymRot180 :

BasicSym rot180

source

@[simp]

theorem AP.rotRight_ft_x {p : PointZ} :

(rotRight.ft p).x = -p.y

source

@[simp]

theorem AP.rotRight_ft_y {p : PointZ} :

(rotRight.ft p).y = p.x

source

@[simp]

theorem AP.rotRight_ft'_x {p : PointZ} :

(rotRight.ft' p).x = p.y

source

@[simp]

theorem AP.rotRight_ft'_y {p : PointZ} :

(rotRight.ft' p).y = -p.x

source

@[simp]

theorem AP.rotLeft_ft_x {p : PointZ} :

(rotLeft.ft p).x = p.y

source

@[simp]

theorem AP.rotLeft_ft_y {p : PointZ} :

(rotLeft.ft p).y = -p.x

source

@[simp]

theorem AP.rotLeft_ft'_x {p : PointZ} :

(rotLeft.ft' p).x = -p.y

source

@[simp]

theorem AP.rotLeft_ft'_y {p : PointZ} :

(rotLeft.ft' p).y = p.x

source

@[simp]

theorem AP.rot180_ft_x {p : PointZ} :

(rot180.ft p).x = -p.x

source

@[simp]

theorem AP.rot180_ft_y {p : PointZ} :

(rot180.ft p).y = -p.y

source

@[simp]

theorem AP.rot180_ft'_x {p : PointZ} :

(rot180.ft' p).x = -p.x

source

@[simp]

theorem AP.rot180_ft'_y {p : PointZ} :

(rot180.ft' p).y = -p.y

source

@[simp]

theorem AP.rotRight_dist_rotRight {p₁ p₂ : PointZ} :

Point.dist (rotRight.ft p₁) (rotRight.ft p₂) = Point.dist p₁ p₂

source

@[simp]

theorem AP.rotRight_dist_rotRight' {p₁ p₂ : PointZ} :

Point.dist (rotRight.ft' p₁) (rotRight.ft' p₂) = Point.dist p₁ p₂

source

@[simp]

theorem AP.rotLeft_dist_rotLeft {p₁ p₂ : PointZ} :

Point.dist (rotLeft.ft p₁) (rotLeft.ft p₂) = Point.dist p₁ p₂

source

@[simp]

theorem AP.rotLeft_dist_rotLeft' {p₁ p₂ : PointZ} :

Point.dist (rotLeft.ft' p₁) (rotLeft.ft' p₂) = Point.dist p₁ p₂

source

@[simp]

theorem AP.rot180_dist_rot180 {p₁ p₂ : PointZ} :

Point.dist (rot180.ft p₁) (rot180.ft p₂) = Point.dist p₁ p₂

source

@[simp]

theorem AP.rot180_dist_rot180' {p₁ p₂ : PointZ} :

Point.dist (rot180.ft' p₁) (rot180.ft' p₂) = Point.dist p₁ p₂

source

@[simp]

theorem AP.rotRight_ft_mk {x y : ℤ} :

rotRight.ft { x := x, y := y } = { x := -y, y := x }

source

@[simp]

theorem AP.rotRight_ft'_mk {x y : ℤ} :

rotRight.ft' { x := x, y := y } = { x := y, y := -x }

source

@[simp]

theorem AP.rotLeft_ft_mk {x y : ℤ} :

rotLeft.ft { x := x, y := y } = { x := y, y := -x }

source

@[simp]

theorem AP.rotLeft_ft'_mk {x y : ℤ} :

rotLeft.ft' { x := x, y := y } = { x := -y, y := x }

source

@[simp]

theorem AP.rot180_ft_mk {x y : ℤ} :

rot180.ft { x := x, y := y } = { x := -x, y := -y }

source

@[simp]

theorem AP.rotRight_mul_rot180 :

rotRight * rot180 = rotLeft

source

@[simp]

theorem AP.rot180_mul_rotRight :

rot180 * rotRight = rotLeft

source

@[simp]

theorem AP.rotLeft_mul_rot180 :

rotLeft * rot180 = rotRight

source

@[simp]

theorem AP.rot180_mul_rotLeft :

rot180 * rotLeft = rotRight