(** Numbers up to @n@ **)
Require Coq.Lists.List.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Tactics.EqDep.
Require Import ExtLib.Tactics.Injection.

Set Implicit Arguments.
Set Strict Implicit.
Set Asymmetric Patterns.

(** `fin n` corresponds to "naturals less than `n`",
 ** i.e. a finite set of size n
 **)
Inductive fin : nat -> Type :=
| F0 : forall {n}, fin (S n)
| FS : forall {n}, fin n -> fin (S n).

Fixpoint fin_all (n : nat) : list (fin n) :=
  match n as n return list (fin n) with
    | 0 => nil
    | S n => @F0 n :: List.map (@FS _) (fin_all n)
  end%list.

Theorem fin_all_In : forall {n} (f : fin n),
  List.In f (fin_all n).
Proof.
(* Goal: forall (n : nat) (f : fin n), @List.In (fin n) f (fin_all n) *)
  induction n; intros.
(* Goal: @List.In (fin O) f (fin_all O) *)
(* Goal: @List.In (fin (S n)) f (fin_all (S n)) *)
  inversion f.
(* Goal: @List.In (fin (S n)) f (fin_all (S n)) *)
  remember (S n). destruct f.
(* Goal: @List.In (fin (S n0)) (@F0 n0) (fin_all (S n0)) *)
(* Goal: @List.In (fin (S n0)) (@FS n0 f) (fin_all (S n0)) *)
  simpl; firstorder.
(* Goal: @List.In (fin (S n0)) (@FS n0 f) (fin_all (S n0)) *)
  inversion Heqn0. subst.
(* Goal: forall y : fin (S n), iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@F0 n) y) true) (@eq (fin (S n)) (@F0 n) y) *)
(* Goal: forall y : fin (S n), iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) y) true) (@eq (fin (S n)) (@FS n x) y) *)
  simpl. right. apply List.in_map. auto.
Qed.

Theorem fin_case : forall n (f : fin (S n)),
  f = F0 \/ exists f', f = FS f'.
Proof.
(* Goal: forall _ : @List.In (fin (S n)) f (fin_all (S n)), or (@eq (fin (S n)) f (@F0 n)) (@ex (fin n) (fun f' : fin n => @eq (fin (S n)) f (@FS n f'))) *)
  intros. generalize (fin_all_In f). intros.
(* Goal: @List.In (fin n) f (fin_all n) *)
  destruct H; auto.
(* Goal: or (@eq (fin (S n)) f (@F0 n)) (@ex (fin n) (fun f' : fin n => @eq (fin (S n)) f (@FS n f'))) *)
  eapply List.in_map_iff in H. right. destruct H.
(* Goal: @ex (fin n) (fun f' : fin n => @eq (fin (S n)) f (@FS n f')) *)
  exists x. intuition.
Qed.

Definition fin0_elim (f : fin 0) : forall T, T :=
  match f in fin n return match n with
                            | 0 => forall T, T
                            | _ => unit
                          end with
    | F0 _ => tt
    | FS _ _ => tt
  end.

Fixpoint pf_lt (n m : nat) : Prop :=
  match n , m with
    | 0 , S _ => True
    | S n , S m => pf_lt n m
    | _ , _ => False
  end.

Fixpoint make (m n : nat) {struct m} : pf_lt n m -> fin m :=
  match n as n , m as m return pf_lt n m -> fin m with
    | 0 , 0 => @False_rect _
    | 0 , S n => fun _ => F0
    | S n , 0 => @False_rect _
    | S n , S m => fun pf => FS (make m n pf)
  end.

Notation "'##' n" := (@make _ n I) (at level 0).

Global Instance Injective_FS {n : nat} (a b : fin n)
  : Injective (FS a = FS b).
(* Goal: Injective (@eq (fin (S n)) (@FS n a) (@FS n b)) *)
refine {| result := a = b |}.
(* Goal: forall _ : @eq (fin (S n)) (@FS n a) (@FS n b), @eq (fin n) a b *)
abstract (intro ; inversion H ; eapply inj_pair2 in H1 ; assumption).
Defined.

Fixpoint fin_eq_dec {n} (x : fin n) {struct x} : fin n -> bool :=
  match x in fin n' return fin n' -> bool with
    | F0 _ => fun y => match y with
                         | F0 _ => true
                         | _ => false
                       end
    | FS n' x' => fun y : fin (S n') =>
      match y in fin n'' return (match n'' with
                                   | 0 => unit
                                   | S n'' => fin n''
                                 end -> bool) -> bool with
        | F0 _ => fun _ => false
        | FS _ y' => fun f => f y'
      end (fun y => fin_eq_dec x' y)
    end.

Global Instance RelDec_fin_eq (n : nat) : RelDec (@eq (fin n)) :=
{ rel_dec := fin_eq_dec }.

Global Instance RelDec_Correct_fin_eq (n : nat)
  : RelDec_Correct (RelDec_fin_eq n).
Proof.
(* Goal: @RelDec_Correct (fin n) (@eq (fin n)) (RelDec_fin_eq n) *)
  constructor.
(* Goal: forall y : fin (S n), iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@F0 n) y) true) (@eq (fin (S n)) (@F0 n) y) *)
(* Goal: forall y : fin (S n), iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) y) true) (@eq (fin (S n)) (@FS n x) y) *)
  induction x. simpl.
(* Goal: @List.In (fin (S n0)) (@FS n0 f) (fin_all (S n0)) *)
  intro. destruct (fin_case y) ; subst.
(* Goal: iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@F0 n) (@F0 n)) true) (@eq (fin (S n)) (@F0 n) (@F0 n)) *)
(* Goal: iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@F0 n) y) true) (@eq (fin (S n)) (@F0 n) y) *)
(* Goal: forall y : fin (S n), iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) y) true) (@eq (fin (S n)) (@FS n x) y) *)
  intuition.
(* Goal: @List.In (fin (S n0)) (@FS n0 f) (fin_all (S n0)) *)
  destruct H ; subst.
(* Goal: iff (@eq bool false true) (@eq (fin (S n)) (@FS n x) (@F0 n)) *)
(* Goal: iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) y) true) (@eq (fin (S n)) (@FS n x) y) *)
  intuition ; try congruence. 
(* Goal: iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) y) true) (@eq (fin (S n)) (@FS n x) y) *)
(*  inversion H.*)
(* Goal: forall y : fin (S n), iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@F0 n) y) true) (@eq (fin (S n)) (@F0 n) y) *)
(* Goal: forall y : fin (S n), iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) y) true) (@eq (fin (S n)) (@FS n x) y) *)
  intro ; destruct (fin_case y) ; subst ; simpl.
(* Goal: iff (@eq bool false true) (@eq (fin (S n)) (@FS n x) (@F0 n)) *)
(* Goal: iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) y) true) (@eq (fin (S n)) (@FS n x) y) *)
  intuition ; try congruence.
(* Goal: iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) y) true) (@eq (fin (S n)) (@FS n x) y) *)
  inversion H.
(* Goal: @List.In (fin (S n0)) (@FS n0 f) (fin_all (S n0)) *)
  destruct H ; subst.
(* Goal: forall y : fin (S n), iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@F0 n) y) true) (@eq (fin (S n)) (@F0 n) y) *)
(* Goal: forall y : fin (S n), iff (@eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) y) true) (@eq (fin (S n)) (@FS n x) y) *)
  split ; intro.
(* Goal: @List.In (fin n) f (fin_all n) *)
  f_equal ; eauto.
(* Goal: @eq (fin n) x x1 *)
(* Goal: @eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) (@FS n x1)) true *)
  eapply IHx.
(* Goal: @eq bool (@rel_dec (fin n) (@eq (fin n)) (RelDec_fin_eq n) x x1) true *)
(* Goal: @eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x) (@FS n x1)) true *)
  eapply H.
(* Goal: @List.In (fin (S n0)) (@FS n0 f) (fin_all (S n0)) *)
  inv_all ; subst.
(* Goal: @eq bool (@rel_dec (fin (S n)) (@eq (fin (S n))) (RelDec_fin_eq (S n)) (@FS n x0) (@FS n x0)) true *)
  apply IHx. reflexivity.
Qed.