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.

FixpointFiniteTypes (last edited 07-12-2007 20:37:50 by localhost)

Cocorico!WikiLicense