FixpointFiniteTypes

    Require Image.
    Require Import List.
    Set Implicit Arguments.
    Fixpoint Fin (n:nat) : Set :=
    match n with
    | O => Empty_set
    | (S m) => (unit+(Fin m))%type
    end.
    Definition FinNew (n:nat) : Fin (S n) := inl (Fin n) tt.
    Definition FinOld (n:nat) (x:Fin n) : Fin (S n) := inr unit x.
    Implicit Arguments FinOld [n].
    Lemma FinO_rect : forall P:Type, Fin O -> P.
    Proof.
    destruct 1.
    Defined.
    Lemma FinSn_rect :
     forall n,
     forall (P:Fin (S n)->Type),
     (forall y:Fin n, P (FinOld y)) ->
     P (FinNew n) ->
     forall x, P x.
    Proof.
    intros n P H0 H1 [[]|]; auto.
    Defined.
    Lemma FinOldOrNew : forall n,
    forall y:Fin (S n),
    {z:Fin n | y=(FinOld z)}+{y=FinNew n}.
    Proof.
    intros n [[]|y]; auto.
    left.
    exists y; auto.
    Defined.
    Lemma FinOldInject : forall n, forall x y:Fin n, (FinOld x)=(FinOld y) -> x=y.
    Proof.
    intros n x y H.
    unfold FinOld in H.
    congruence.
    Qed.
    Hint Resolve FinOldInject : fin.
    Lemma FinDecideEquality : forall n, forall (x y:Fin n), {x=y}+{x<>y}.
    Proof.
    induction n.
    destruct x.
    simpl.
    intros [[]|x] [[]|y]; auto; try (right; discriminate).
    destruct (IHn x y).
    left; intuition; congruence.
    right; intuition; congruence.
    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 P Q H.
    right.
    destruct x.
    intros P Q H.
    destruct (H (FinNew n)).
    left.
    exists (FinNew n); auto.
    destruct (IHn (fun x=>(P (FinOld x)))
                  (fun x=>(Q (FinOld x)))
                  (fun x=> (H (FinOld x)))).
    destruct s.
    left.
    exists (FinOld x); auto.
    right.
    intros [[]|x]; firstorder.
    Defined.
    Definition FinList : forall n, {l:list (Fin n) | forall x, In x l}.
    intros.
    induction n.
    exists (@nil (Fin 0)).
    destruct x.
    destruct IHn.
    exists (cons (FinNew n) (map (@FinOld n) x)).
    intros [[]|y]; simpl; auto.
    right.
    change (In (FinOld y) (map (FinOld (n:=n)) x)).
    apply in_map; auto with *.
    Defined.
    Lemma FinInjectionInjection : forall n m, forall f:Fin (S n) -> Fin (S m), Image.injective _ _ f -> {g:Fin n -> Fin m | Image.injective _ _ g}.
    Proof.
    intros n m f H.
    destruct (FinOldOrNew (f (FinNew n))).
    destruct s.
    exists (fun a:Fin n=>
    match (FinOldOrNew (f (FinOld a))) with
    | inleft p => proj1_sig p
    | inright _ => x
    end).
    intros a b A.
    destruct (FinOldOrNew (f (FinOld a))); try destruct s;
    destruct (FinOldOrNew (f (FinOld b))); try destruct s;
    simpl in A.
    apply FinOldInject.
    apply H.
    congruence.
    assert ((FinOld a)=(FinNew n)).
    apply H.
    congruence.
    discriminate H0.
    assert ((FinOld b)=(FinNew n)).
    apply H.
    congruence.
    discriminate H0.
    apply FinOldInject.
    apply H.
    congruence.
    assert (forall x, {y:Fin m | f (FinOld x) = FinOld y}).
    intros x.
    destruct (FinOldOrNew (f (FinOld x))).
    auto.
    assert ((FinNew n)=(FinOld x)).
    apply H.
    congruence.
    discriminate H0.
    exists (fun x=>(proj1_sig (H0 x))).
    intros a b A.
    destruct (H0 a).
    destruct (H0 b).
    simpl in A.
    apply FinOldInject.
    apply H.
    congruence.
    Defined.
    Lemma FinInjectionLt : forall n m, forall f:Fin n -> Fin m, Image.injective _ _ f -> n <= m.
    Proof.
    induction n; auto with *.
    destruct m.
    intro f.
    destruct (f (FinNew n)).
    intros f H.
    apply Le.le_n_S.
    destruct (FinInjectionInjection H).
    firstorder.
    Qed.