Considering only one face of a Rubik's cube: reduce a set of turns to an orientation

Rubik.idr

module Rubik

%default total
%access public export

||| "North", "south", "east" and "west" face orientations
data Orient = N | E | S | W

turnCW : Orient -> Orient
turnCW N = E
turnCW E = S
turnCW S = W
turnCW W = N

turnCCW : Orient -> Orient
turnCCW N = W
turnCCW E = N
turnCCW S = E
turnCCW W = S

turnCW_retracts_turnCCW : (x : Orient) -> turnCW (turnCCW x) = x
turnCW_retracts_turnCCW N = Refl
turnCW_retracts_turnCCW E = Refl
turnCW_retracts_turnCCW S = Refl
turnCW_retracts_turnCCW W = Refl

turnCCW_retracts_turnCW : (x : Orient) -> turnCCW (turnCW x) = x
turnCCW_retracts_turnCW N = Refl
turnCCW_retracts_turnCW E = Refl
turnCCW_retracts_turnCW S = Refl
turnCCW_retracts_turnCW W = Refl

turnCW_forms_ring : (x : Orient) -> turnCW (turnCW (turnCW (turnCW x))) = x
turnCW_forms_ring N = Refl
turnCW_forms_ring E = Refl
turnCW_forms_ring S = Refl
turnCW_forms_ring W = Refl

turnCCW_forms_ring : (x : Orient) -> turnCCW (turnCCW (turnCCW (turnCCW x))) = x
turnCCW_forms_ring N = Refl
turnCCW_forms_ring E = Refl
turnCCW_forms_ring S = Refl
turnCCW_forms_ring W = Refl

||| Clockwise or counterclockwise single turn
data Turn = CW | CCW

turn : Turn -> Orient -> Orient
turn CW = turnCW
turn CCW = turnCCW

||| Turns of one face only, all other faces ignored. Take an input list of
||| turns; reduce it to a 2-bit state.
reduce : List Turn -> Orient
reduce = foldr turn N