# Library InductiveFiniteSets

Require Import Eqdep_dec Image Peano_dec.

Inductive Finite Types

Set Implicit Arguments.

Inductive Fin : nat -> Set :=
| fz : forall n, Fin (S n)
| fs : forall n, Fin n -> Fin (S n).

Derive Inversion FinO_rect with (Fin 0) Sort Type.

Inductive FinSN (n : nat) : Fin (S n) -> Set :=
| isfz : FinSN (fz n)
| isfs : forall i, FinSN (fs i).

Definition finSN (n : nat) (i : Fin (S n)) : FinSN i :=
match i in (Fin k) return match k return Fin k -> Set with
| O => fun _ => unit
| S n' => @FinSN _
end i with
| fz _ => isfz _
| fs _ j => isfs j
end.

Definition FinSn_rect : forall n, forall (P:Fin (S n)->Type),
(forall y:Fin n, P (fs y)) -> P (fz n) -> forall x, P x :=
fun n P H0 H1 x => match (finSN x) in (FinSN e) return (P e) with
| isfz => H1
| isfs i => (H0 i)
end.

Lemma fsInject : forall n, forall x y:Fin n, (fs x)=(fs y) -> x=y.
Proof.
induction x; intro y. destruct (finSN y); trivial.
intro H; try discriminate H.
destruct (finSN y).
intro H; try discriminate H.
intro H; injection H.
intro H0;
rewrite (inj_pair2_eq_dec _ eq_nat_dec (fun n : nat => Fin n) n x i H0);
trivial.
Qed.

Hint Resolve fsInject : fin_scope.

Lemma FinDecideEquality : forall n, forall (x y:Fin n), {x=y}+{x<>y}.
Proof.
induction x. intro y ; destruct (finSN y) ; auto.
try (right; discriminate).
intro y; destruct (finSN y).
right; discriminate.
destruct (IHx i); subst.
left ; trivial.
right; intuition.
Defined.

Lemma FinForallOrExist : forall n (P Q:Fin n->Prop),
(forall x, {P x}+{Q x}) -> {x:Fin n | P x}+{forall x, Q x}.
Proof.
induction n. intros; right; inversion x.
intros P Q H. destruct (H ( fz n)).
left; exists (fz n); auto.
destruct (IHn (fun x=>(P (fs x))) (fun x=>(Q (fs x))) (fun x=> (H (fs x)))).
destruct s. left; exists (fs x); auto.
right. intros x; destruct x using FinSn_rect; auto.
Defined.

Fixpoint eqFin (n :nat) (i : Fin n) {struct i}: Fin n -> bool :=
match i in Fin e return (Fin e -> bool) with
| fz _ => fun j => match (finSN j) with
| isfz => true
| isfs _ => false
end
| fs _ k => fun j => match (finSN j) with
| isfz => false
| isfs k' => eqFin k k'
end
end.

Lemma eqFin_ok : forall n (i j : Fin n), eqFin i j = true -> i = j.
Proof.
induction i; simpl. intros j; destruct (finSN j);
try (intro h; discriminate h); trivial.
intro j; destruct (finSN j); try (intro h; discriminate h).
intro h; rewrite (IHi i0 h); trivial.
Qed.

Fixpoint lefin (n : nat) (i : Fin n) {struct i}: Fin n -> bool :=
match i as e in (Fin n) return (Fin n -> bool) with
| fz _ => fun _ => true
| fs _ i' => fun x =>
match (finSN x) with
| isfs z => lefin i' z
| _ => false
end
end.

Inductive Lefin : forall n, Fin n -> Fin n -> Set :=
| leq : forall n, Lefin (fz n) (fz n)
| lefz : forall n ( i : Fin n) , Lefin (fz n) (fs i)
| lefs : forall n (i j : Fin n), Lefin i j -> Lefin (fs i) (fs j).

Lemma Le_refl : forall n (i : Fin n), Lefin i i.
Proof.
induction i; try apply leq.
exact (lefs IHi).
Qed.

Lemma Le_fs_inj : forall n (i j : Fin n), Lefin (fs i) (fs j) -> Lefin i j.
Proof.
intros n i j H; try inversion H.
rewrite <- (inj_pair2_eq_dec _ eq_nat_dec (fun n : nat => Fin n) n i0 i H1);
rewrite <- (inj_pair2_eq_dec _ eq_nat_dec (fun n : nat => Fin n) n j0 j H2);
trivial.
Qed.

Lemma Le_trans :
forall n (i j k: Fin n), Lefin i j -> Lefin j k -> Lefin i k.
Proof.
induction i. destruct j using FinSn_rect.
destruct k using FinSn_rect. intros.
apply lefz. intros. inversion H0.
destruct k using FinSn_rect.
intros. apply lefz.
intros. apply leq. destruct j using FinSn_rect;
destruct k using FinSn_rect.
intros H H1. exact (lefs (IHi _ _ (Le_fs_inj H) (Le_fs_inj H1)) ).
intros. inversion H0.
intros. inversion H.
intros. inversion H.
Qed.

Lemma Le_ind_bool : forall n (i j : Fin n), Lefin i j -> lefin i j = true.
Proof.
induction i. destruct j using FinSn_rect; simpl; auto.
destruct j using FinSn_rect; simpl; auto.
intros. exact (IHi _ (Le_fs_inj H)).
intros. inversion H.
Qed.

Lemma fin_0_empty: (Fin 0) -> False.
Proof.
intro i; inversion i.
Qed.

Fixpoint foo n (i : Fin n) :=
match i with
| fz _ => 0
| fs _ i => S (foo i)
end.

Fixpoint nat_finite (n:nat) k : k<n -> Fin n :=
match n return ( k<n -> Fin n) with
O => fun (h:k<O) =>
match (lt_n_O k h) return (Fin 0) with end
| (S n') => match k return (k<(S n') -> Fin (S n')) with
O => fun _ => (fz n')
| (S k') => fun h:S k' < S n' =>
fs (nat_finite (lt_S_n _ _ h))
end
end.

Implicit Arguments nat_finite [n].

Lemma nat_finite_id:
forall (n k:nat)(h:k<n), (foo (nat_finite k h)) = k.
Proof.
induction n.
intros k h; destruct (lt_n_O k h).
induction k; auto.
exact (fun h => f_equal S (IHn k (lt_S_n k n h))).
Qed.

Fixpoint finite_lt_n (n : nat) (i : Fin n) {struct i}: (foo i) < n :=
match i as e in Fin m return (foo e) < m with
| fz x => lt_O_Sn x
| fs _ j => lt_n_S (foo j) _ (finite_lt_n j)
end.

Definition finite_le_n (n : nat) (i : Fin n) :=
lt_le_weak _ _ (finite_lt_n i).

Lemma finite_nat_id_general:
forall (n:nat)(i:Fin n)(h:(foo i)<n), (nat_finite (foo i) h) = i.
Proof.
induction i; auto;
try (intro h; simpl; rewrite IHi; auto).
Qed.

Lemma finite_nat_id:
forall (n:nat)(i:Fin n), (nat_finite (foo i) (finite_lt_n i)) = i.
Proof.
intros; apply finite_nat_id_general; auto.
Qed.

Require Import Arith.

Definition FinFn (H : forall n, Fin n -> Fin n) :=
fun n m => match le_lt_dec n m with
| left _ => 0
| right l => foo (H _ (nat_finite m l))
end.

Definition FinFn1 (f : nat -> nat) (H : forall n, Fin (f n) -> Fin n) :=
fun n m => match le_lt_dec (f n) m with
| left _ => 0
| right l => foo (H _ (nat_finite m l))
end.

Definition FinFnEx
(f : nat -> nat) (H : forall n, Fin (f n) -> Fin n) :
forall n, {k | k < f n} -> Fin n :=
fun n ex => let (_, l) := ex in H n (nat_finite _ l).

Definition FinFn_inv (H : nat -> nat -> nat) : forall n, Fin n -> Fin n :=
fun n i => match le_lt_dec n (H n (foo i)) with
| left _ => i
| right l => nat_finite (H n (foo i)) l
end .

Lemma foo_not_le : forall n (i : Fin n), ~ n <= foo i.
induction i; simpl; auto with arith.
Qed.

Lemma FinFn_l (H : forall n, Fin n -> Fin n) :
forall n (i : Fin n), FinFn_inv (FinFn H) i = H n i .
Proof.
unfold FinFn_inv; unfold FinFn; simpl; intros.
destruct (le_lt_dec n (foo i)); simpl.
case (foo_not_le i l).
rewrite (finite_nat_id_general i l).
destruct (le_lt_dec n (foo (H n i)) ).
case (foo_not_le (H n i) l0 ).
apply (finite_nat_id_general (H n i) l0 ).
Qed.

Lemma FinFn_l1 (H : nat -> nat -> nat) :
forall n m, m < n -> H n m < n -> FinFn (FinFn_inv H) n m = H n m .
Proof.
unfold FinFn; unfold FinFn_inv; intros.
destruct (le_lt_dec n m) as [ l | r ].
case (le_not_lt _ _ l H0).
rewrite (nat_finite_id r).
destruct (le_lt_dec n (H n m ));
[case (le_not_lt _ _ l H1) | apply (nat_finite_id l)].
Qed.

Lemma FinFn_eq_ok : forall (h h1 : forall n, Fin n -> Fin n), h = h1 ->
FinFn h = FinFn h1.
Proof.
intros h h1 H; destruct H; trivial.
Qed.

Lemma FinFn_inv_eq_ok : forall (h h1 : nat -> nat -> nat), h = h1 ->
FinFn_inv h = FinFn_inv h1.
Proof.
intros h h1 H; destruct H; trivial.
Qed.