From mathcomp Require Import all_ssreflect all_algebra.

(* Example from Chapter 8 of mathcomp book *)

Inductive dir: predArgType :=
| South | North | East | West.

(* dir to an existing ordinal ?? *)
Definition d2o (d: dir): 'I_4 :=
  match d with
  | South => inord 0
  | North => inord 1
  | East => inord 2
  | West => inord 3
  end.

Definition o2d (o: 'I_4): option dir :=
  match val o with
  | 0 => Some South
  | 1 => Some North
  | 2 => Some East
  | 3 => Some West
  | _ => None
  end.

(* d2o and o2d cancel out *)
Lemma pcan_do4: pcancel d2o o2d.
Proof.
  by case; rewrite /o2d /= inordK.
Qed.

Compute (North \in dir).
(* = true : bool *)

Fail Check (North != South).  (* needs EqType *)
Fail Check (#| dir | == 4).   (* needs FinType *)

(* Give structure of ordinals to [dir] *)
Definition dir_eqMixin := PcanEqMixin pcan_do4.
Canonical dir_eqType := EqType dir dir_eqMixin.
Check (North != South).
(* North != South : bool *)

(* [CountType] implies [ChoiceType] by the way.
   Here it's explicitly given though *)
Definition dir_choiceMixin := PcanChoiceMixin pcan_do4.
Canonical dir_choiceType := ChoiceType dir dir_choiceMixin.

Definition dir_countMixin := PcanCountMixin pcan_do4.
Canonical dir_countType := CountType dir dir_countMixin.

Definition dir_finMixin := PcanFinMixin pcan_do4.
Canonical dir_finType := FinType dir dir_finMixin.
Check (#| dir | == 4).
(* #|dir| == 4 : bool *)

Check (North != South) && (North \in dir) && (#| dir | == 4).