Writing a decision procedure for equality on fins

feq_dec.v

Inductive fin : nat -> Set :=
| F1 : forall {n : nat}, fin (S n)
| FS : forall {n : nat}, fin n -> fin (S n).

Definition C {m : nat} (x : fin (S m)) :=
  { x' | x = FS x' } + { x = F1 }.

Definition case {m : nat} (x : fin (S m)) : C x :=
match x in fin (S n) return { x' | x = FS x' } + { x = F1 } with
  | F1    => inright eq_refl
  | FS x' => inleft (exist _ x' eq_refl)
end.

Definition finpred {m : nat} (x : fin m) : option (fin (pred m)) :=
match x with
  | F1    => None
  | FS x' => Some x'
end.

Definition P {m : nat} (x y : fin m) := {x = y} + {x <> y}.

Fixpoint feq_dec {m : nat} (x y : fin m) : P x y.
refine (
match m return forall (x y : fin m), P x y with
  | O    => _
  | S m' => fun x y =>
  match (case x, case y) with
    | (inright eqx            , inright eqy)             => left _
    | (inleft (exist _ x' eqx), inright eqy)             => right _
    | (inright eqx            , inleft (exist _ y' eqy)) => right _
    | (inleft (exist _ x' eqx), inleft (exist _ y' eqy)) =>
    match feq_dec _ x' y' with
      | left eqx'y'   => left _
      | right neqx'y' => right _
    end
  end
end x y); simpl in *; subst.
- inversion 0.
- reflexivity.
- intro Heq; apply neqx'y'.
  assert (Heq' : Some x' = Some y') by exact (f_equal finpred Heq).
  inversion Heq'; reflexivity.
- inversion 1.
- inversion 1.
- reflexivity.
Defined.

Compute (@feq_dec 5 (FS F1) (FS F1)).