Add an OrderedType for fin

Util.v

(* this file should be pasted at the bottom of core/Util.v *)

Require Import OrderedType.

Fixpoint fin_to_nat {n : nat} : fin n -> nat :=
  match n with
  | 0 => fun x : fin 0 => match x with end
  | S n' => fun x : fin (S n') => 
             match x with 
             | None => 0
             | Some y => S (fin_to_nat y)
             end
  end.

Definition fin_lt {n : nat} (a b : fin n) : Prop := lt (fin_to_nat a) (fin_to_nat b).

Lemma fin_lt_Some_elim : 
  forall n (a b : fin n), @fin_lt (S n) (Some a) (Some b) -> fin_lt a b.
Proof.
  intros.
  unfold fin_lt. simpl.
  intuition.
Qed.

Lemma fin_lt_Some_intro : 
  forall n (a b : fin n), fin_lt a b -> @fin_lt (S n) (Some a) (Some b).
Proof.
  intros.
  unfold fin_lt. simpl.
  intuition.
Qed.

Lemma None_lt_Some : 
  forall n (x : fin n), 
    @fin_lt (S n) None (Some x).
Proof.
  unfold fin_lt. simpl. auto with *.
Qed.

Lemma fin_lt_trans : forall n (x y z : fin n), 
    fin_lt x y -> fin_lt y z -> fin_lt x z.
Proof.
  induction n; intros.
  - destruct x.
  - destruct x, y, z; simpl in *; 
    repeat match goal with
    | [ H : fin_lt (Some _) (Some _) |- _ ] => apply fin_lt_Some_elim in H
    | [ |- fin_lt (Some _) (Some _) ] => apply fin_lt_Some_intro
    end; eauto using None_lt_Some; solve_by_inversion.
Qed.

Lemma fin_lt_not_eq : forall n (x y : fin n), fin_lt x y -> x <> y.
Proof.
  induction n; intros.
  - destruct x.
  - destruct x, y; 
    repeat match goal with
    | [ H : fin_lt (Some _) (Some _) |- _ ] => apply fin_lt_Some_elim in H
    | [ |- fin_lt (Some _) (Some _) ] => apply fin_lt_Some_intro
    end; try congruence.
    + specialize (IHn f f0). concludes. congruence.
    + solve_by_inversion.
Qed.

Fixpoint fin_compare (n : nat) : forall (x y : fin n), Compare fin_lt eq x y :=
  match n with
  | 0 => fun x y : fin 0 => match x with end
  | S n' => fun x y : fin (S n') => 
             match x, y with
             | Some x', Some y' => 
               match fin_compare n' x' y' with
               | LT pf => LT (fin_lt_Some_intro _ _ _ pf)
               | EQ pf => EQ (f_equal _ pf)
               | GT pf => GT (fin_lt_Some_intro _ _ _ pf)
               end
             | Some x', None => GT (None_lt_Some n' x')
             | None, Some y' => LT (None_lt_Some n' y')
             | None, None => EQ eq_refl
             end
  end.

Module Type NatValue.
  Parameter n : nat.
End NatValue.
  
Module fin_OT (N : NatValue) <: OrderedType.
  Definition t := fin N.n.
  Definition eq : t -> t -> Prop := eq.
  Definition lt : t -> t -> Prop := fin_lt.
  
 Definition eq_refl : forall x : t, eq x x := @eq_refl _.
 Definition eq_sym : forall x y: t, eq x y -> eq y x := @eq_sym _.
 Definition eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z := @eq_trans _.
 
 Definition lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z := fin_lt_trans N.n.
 Definition lt_not_eq : forall x y : t, lt x y -> ~ eq x y := fin_lt_not_eq N.n.
 
 Definition compare : forall x y : t, Compare lt eq x y := fin_compare N.n.
 Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y} := fin_eq_dec N.n.
End fin_OT.