Projects.Dir

source

inductive Dir :

Type

up : Dir
left : Dir
right : Dir
down : Dir

Instances For

source

@[instance_reducible]

instance instInhabitedDir :

Inhabited Dir

Equations

instInhabitedDir = { default := instInhabitedDir.default }

source

@[instance_reducible]

instance instDecidableEqDir :

DecidableEq Dir

Equations

instDecidableEqDir x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[instance_reducible]

instance instFintypeDir :

Fintype Dir

Equations

instFintypeDir = { elems := { val := ↑Dir.enumList, nodup := Dir.enumList_nodup }, complete := instFintypeDir._proof_1 }

source

def Dir.point :

Dir → PointZ

Equations

Dir.up.point = { x := 0, y := -1 }
Dir.down.point = { x := 0, y := 1 }
Dir.left.point = { x := -1, y := 0 }
Dir.right.point = { x := 1, y := 0 }

Instances For

source

@[simp]

theorem Dir.point_up :

up.point = { x := 0, y := -1 }

source

@[simp]

theorem Dir.point_down :

down.point = { x := 0, y := 1 }

source

@[simp]

theorem Dir.point_left :

left.point = { x := -1, y := 0 }

source

@[simp]

theorem Dir.point_right :

right.point = { x := 1, y := 0 }

source

@[simp]

theorem Dir.point_ne_zero {d : Dir} :

d.point ≠ 0

source

def Dir.hor :

Dir → Prop

Equations

Instances For

source

def Dir.vert :

Dir → Prop

Equations

Instances For

source

@[simp]

theorem Dir.not_hor_up :

¬up.hor

source

@[simp]

theorem Dir.not_hor_down :

¬down.hor

source

@[simp]

theorem Dir.hor_left :

left.hor

source

@[simp]

theorem Dir.hor_right :

right.hor

source

@[simp]

theorem Dir.vert_up :

up.vert

source

@[simp]

theorem Dir.vert_down :

down.vert

source

@[simp]

theorem Dir.not_vert_left :

¬left.vert

source

@[simp]

theorem Dir.not_vert_right :

¬right.vert

source

@[simp]

theorem Dir.not_hor {d : Dir} :

¬d.hor ↔ d.vert

source

@[simp]

theorem Dir.not_vert {d : Dir} :

¬d.vert ↔ d.hor

source

@[instance_reducible]

instance Dir.instDecidableHor {d : Dir} :

Decidable d.hor

Equations

source

@[instance_reducible]

instance Dir.instDecidableVert {d : Dir} :

Decidable d.vert

Equations

source

def Dir.rotRight :

Dir → Dir

Equations

Instances For

source

def Dir.rotLeft :

Dir → Dir

Equations

Instances For

source

def Dir.inv :

Dir → Dir

Equations

Instances For

source

@[instance_reducible]

instance Dir.instInv :

Inv Dir

Equations

Dir.instInv = { inv := Dir.inv }

source

theorem Dir.inv_def {d : Dir} :

d⁻¹ = d.inv

source

@[simp]

theorem Dir.rotRight_up :

up.rotRight = right

source

@[simp]

theorem Dir.rotRight_right :

right.rotRight = down

source

@[simp]

theorem Dir.rotRight_down :

down.rotRight = left

source

@[simp]

theorem Dir.rotRight_left :

left.rotRight = up

source

@[simp]

theorem Dir.rotLeft_up :

up.rotLeft = left

source

@[simp]

theorem Dir.rotLeft_right :

right.rotLeft = up

source

@[simp]

theorem Dir.rotLeft_down :

down.rotLeft = right

source

@[simp]

theorem Dir.rotLeft_left :

left.rotLeft = down

source

@[simp]

theorem Dir.inv_up :

up ⁻¹ = down

source

@[simp]

theorem Dir.inv_right :

right ⁻¹ = left

source

@[simp]

theorem Dir.inv_down :

down ⁻¹ = up

source

@[simp]

theorem Dir.inv_left :

left ⁻¹ = right

source

@[simp]

theorem Dir.rotRight_rotRight {d : Dir} :

d.rotRight.rotRight = d⁻¹

source

@[simp]

theorem Dir.rotLeft_rotLeft {d : Dir} :

d.rotLeft.rotLeft = d.inv

source

@[simp]

theorem Dir.rotLeft_rotRight {d : Dir} :

d.rotLeft.rotRight = d

source

@[simp]

theorem Dir.rotRight_rotLeft {d : Dir} :

d.rotRight.rotLeft = d

source

@[simp]

theorem Dir.rotLeft_inv {d : Dir} :

d.rotLeft⁻¹ = d.rotRight

source

@[simp]

theorem Dir.rotRIght_inv {d : Dir} :

d.rotRight⁻¹ = d.rotLeft

source

@[simp]

theorem Dir.inv_rotLeft {d : Dir} :

d⁻¹.rotLeft = d.rotRight

source

@[simp]

theorem Dir.inv_rotRIght {d : Dir} :

d⁻¹.rotRight = d.rotLeft

source

@[simp]

theorem Dir.inv_inv {d : Dir} :

d⁻¹ ⁻¹ = d

source

theorem Dir.hor_iff {d : Dir} :

d.hor ↔ d = left ∨ d = right

source

theorem Dir.vert_iff {d : Dir} :

d.vert ↔ d = up ∨ d = down

source

def Point.coord' {α : Type u_1} (p : Point α) (d : Dir) :

α

Equations

Instances For

source

def Point.coord {α : Type u_1} [ha : Neg α] (p : Point α) (d : Dir) :

α

Equations

Instances For

source

@[simp]

theorem Point.coord'_up {α : Type u_1} {p : Point α} :

p.coord' Dir.up = p.y

source

@[simp]

theorem Point.coord'_down {α : Type u_1} {p : Point α} :

p.coord' Dir.down = p.y

source

@[simp]

theorem Point.coord'_left {α : Type u_1} {p : Point α} :

p.coord' Dir.left = p.x

source

@[simp]

theorem Point.coord'_right {α : Type u_1} {p : Point α} :

p.coord' Dir.right = p.x

source

@[simp]

theorem Point.coord_up {α : Type u_1} {p : Point α} [ha : Neg α] :

p.coord Dir.up = -p.y

source

@[simp]

theorem Point.coord_down {α : Type u_1} {p : Point α} [ha : Neg α] :

p.coord Dir.down = p.y

source

@[simp]

theorem Point.coord_left {α : Type u_1} {p : Point α} [ha : Neg α] :

p.coord Dir.left = -p.x

source

@[simp]

theorem Point.coord_right {α : Type u_1} {p : Point α} [ha : Neg α] :

p.coord Dir.right = p.x

source

@[simp]

theorem Dir.hor_rotRight {d : Dir} :

d.rotRight.hor = d.vert

source

@[simp]

theorem Dir.vert_rotRight {d : Dir} :

d.rotRight.vert = d.hor

source

@[simp]

theorem Dir.hor_rotLeft {d : Dir} :

d.rotLeft.hor = d.vert

source

@[simp]

theorem Dir.vert_rotLeft {d : Dir} :

d.rotLeft.vert = d.hor

source

@[simp]

theorem Dir.hor_inv {d : Dir} :

d⁻¹.hor = d.hor

source

@[simp]

theorem Dir.vert_inv {d : Dir} :

d⁻¹.vert = d.vert

source

def Dir.univList :

List Dir

Equations

Dir.univList = [Dir.up , Dir.left , Dir.right , Dir.down ]

Instances For

source

@[simp]

theorem Dir.nodup_univList :

univList.Nodup

source

@[simp]

theorem Dir.mem_univList {d : Dir} :

d ∈ univList