Fin is injective

Inductive Fin : nat -> Set :=
| fz : forall n, Fin (S n)
| fs : forall n, Fin n -> Fin (S n).
Implicit Arguments fz [n].
Implicit Arguments fs [n].
(* Fin is the family of finite types
 * Fin n is the type with 'n' distinct elements
 * Fin 0 ~ void
 * Fin 1 ~ unit
 * Fin 2 ~ bool
 *)

Inductive sumdys (A:Prop) (B:Type) : Type :=
| dyleft : A -> sumdys A B
| dyright : B -> sumdys A B.
(* Just because I prefer the Prop case to come first *)

Definition fz_or_fs n (f : Fin (S n)) : sumdys (f = fz) { f' | f = fs f' }.
intros; set (P n :=
  match n return Fin n -> Set with
    | O => fun _ => unit
    | S n => fun f => sumdys (f = fz) { f' | f = fs f' }
  end).

change (P (S n) f);
  destruct f;
    [ left; reflexivity |
      right; exists f; reflexivity ].
Defined.
Implicit Arguments fz_or_fs [n].

Lemma no_fin0 : Fin 0 -> forall P, P.
  intros f; refine
    match f in Fin n' return
      match n' with
        | O => forall P, P
        | S _ => True
      end
      with
      | fz _ => I
      | fs _ _ => I
    end.
Qed.

(* Destruct a fin down one level *)
Ltac fin_case f :=
  destruct (fz_or_fs f);
    match goal with
      | eq : f = fz |- _ =>
        try (rewrite eq in *; clear eq)
      | Ex : { f' | f = fs f' } |- _ =>
        destruct Ex;
          match goal with
            | eq : f = fs ?f' |- _ =>
              try (rewrite eq in *; clear eq)
          end end.

(* Smash a Fin to bits *)
Ltac destruct_fin f :=
  destruct (fz_or_fs f);
    match goal with
      | eq : f = fz |- _ =>
        try (rewrite eq in *; clear eq)
      | Ex : { f' | f = fs f' } |- _ =>
        destruct Ex;
          match goal with
            | eq : f = fs ?f' |- _ =>
              try (rewrite eq in *; clear eq);
                match type of f' with
                  | Fin 0 => apply (no_fin0 f')
                  | Fin (S _) => destruct_fin f'
                end end end.

Lemma one_fin1 : forall f : Fin 1, f = fz.
  intro f; destruct_fin f; reflexivity.
Qed.

Lemma two_fin2 : forall f : Fin 2, f = fz \/ f = fs fz.
  intro f; destruct_fin f; auto.
Qed.

Definition squish n : Fin (S (S n)) -> Fin (S n) :=
  fun f => match fz_or_fs f with
             | dyleft _ => fz
             | dyright (exist f _) => f
           end.
Implicit Arguments squish [n].
(* squish pushes down on the Fin *)

Fixpoint bump n (f : Fin n) : Fin (S n) :=
  match f with
    | fz _ => fz
    | fs _ f => fs (bump _ f)
  end.
Implicit Arguments bump [n].
(* bump lifts the family a Fin resides in *)

Fixpoint scum n : Fin (S n) :=
  match n with
    | O => fz
    | S n => fs (scum n)
  end.
Implicit Arguments scum [n].
(* scum always floats at the top *)


Lemma fs_injective n (x y : Fin n) : fs x = fs y -> x = y.
  intros; destruct n.
  apply (no_fin0 x).
  change (squish (fs x) = squish (fs y)); congruence.
Qed.
Implicit Arguments fs_injective [n x y].

Lemma bump_isn't_scum n (f : Fin n) : bump f <> scum.
  induction f.
  discriminate.
  contradict IHf.
  simpl in IHf; rewrite (fs_injective IHf).
  reflexivity.
Qed.

Lemma bump_injection n : forall u v : Fin n, bump u = bump v -> u = v.
  intros; induction n.
  apply (no_fin0 u).
  fin_case u; fin_case v.
  reflexivity.
  discriminate.
  discriminate.
  rewrite (IHn _ _ (fs_injective H)).
  reflexivity.
Qed.

Definition fin_eq_dec n (x y : Fin n) : {x = y} + {x <> y}.
intros; induction n.
apply (no_fin0 x).
fin_case x; fin_case y.
left; reflexivity.
right; discriminate.
right; discriminate.
destruct (IHn x0 x1).
left; congruence.
right; contradict n0; pose (fs_injective n0); congruence.
Defined.
Implicit Arguments fin_eq_dec [n].


(* thinning a Fin either lifts it or leaves it where it was,
 * depending on if it was above or below the wedge.
 *)
Definition thin n (wedge : Fin (S n)) : Fin n -> Fin (S n).
induction n.
refine (fun _ e => no_fin0 e _).
refine (fun wedge e =>
  match fz_or_fs wedge with
    | dyleft _ => fs e
    | dyright (exist wedge' _) =>
      match fz_or_fs e with
        | dyleft _ => fz
        | dyright (exist e' _) => fs (IHn wedge' e')
      end
  end).
Defined.

(* thickening a Fin squashes down around a pivot, this is
 * a partial inverse of thin, which will be proven soon.
 *)
Definition thicken n (wedge e : Fin (S n)) : option (Fin n).
induction n.
refine (fun _ _ => None).
refine (fun wedge e =>
  match fz_or_fs wedge with
    | dyleft _ =>
      match fz_or_fs e with
        | dyleft _ => None
        | dyright (exist e' _) => Some e'
      end
    | dyright (exist wedge' _) =>
      match fz_or_fs e with
        | dyleft _ => Some fz
        | dyright (exist e' _) =>
          match IHn wedge' e' with
            | Some e' => Some (fs e')
            | None => None
          end
      end
  end).
Defined.

Theorem thin_injective n o x y : thin n o x = thin n o y -> x = y.
  intros; induction n.
  apply (no_fin0 x).
  fin_case x; fin_case y.
  reflexivity.
  fin_case o; inversion H.
  fin_case o; inversion H.
  destruct n.
  apply (no_fin0 x0).
  fin_case o; rewrite (IHn fz x0 x1); try reflexivity; simpl.
  rewrite (fs_injective H); reflexivity.
  rewrite (IHn _ _ _ (fs_injective H)); reflexivity.
Qed.

Theorem thin_mutate n o e : thin n o e <> o.
  intros; induction n.
  apply (no_fin0 e).
  fin_case o.
  discriminate.
  fin_case e.
  discriminate.
  pose (IHn x x0).
  simpl; contradict n0.
  exact (fs_injective n0).
Qed.

Theorem thin_image n o e : o <> e -> exists e', thin n o e' = e.
  intros; induction n.
  destruct_fin o; destruct_fin e.
  absurd (@fz 1 = fz); auto.
  fin_case o.
  fin_case e.
  absurd (@fz 1 = fz); auto.
  exists x; reflexivity.
  fin_case e.
  exists fz; reflexivity.
  destruct (IHn x x0).
  contradict H; congruence.
  exists (fs x1); simpl; congruence.
Qed.

Theorem thicken_inversion n o e r : thicken n o e = r ->
  (e = o /\ r = None) + { e' | e = thin n o e' /\ r = Some e' }.
  intros; induction n.
  destruct_fin o; destruct_fin e; left; auto.
  fin_case o.
  
  fin_case e.
  left; auto.
  right; exists x; auto.
  
  fin_case e.
  right; exists fz; auto.
  
  destruct r.
  simpl in H.
  case_eq (thicken n x x0).
  intros f' eq.
  rewrite eq in *.
  injection H; clear H; intro H; rewrite <- H in *; clear H.
  destruct (IHn _ _ _ eq).
  destruct a.
  inversion H0.
  destruct s.
  destruct a.
  injection H0; clear H0; intro H0; rewrite <- H0 in *; clear H0.
  right; exists (fs f'); intuition.
  simpl; congruence.
  intro eq; rewrite eq in H; inversion H.
  
  left; intuition.
  destruct (IHn x x0 None).
  simpl in H.
  destruct (thicken n x x0); auto.
  inversion H.
  destruct a; congruence.
  destruct s.
  destruct a.
  inversion H1.
Qed.
(* Why is the proof long? *)


Definition thicken' n (wedge e : Fin (S n)) : wedge <> e -> Fin n.
intros.
pose (thicken n wedge e).
destruct (thicken_inversion n wedge e o (refl_equal _)).
destruct a; absurd (wedge = e); auto.
destruct s.
exact x.
Defined.

Lemma thick_and_thin n o e ne : e = thin n o (thicken' n o e ne).
  intros; unfold thicken'.
  set (k := thicken_inversion _ _ _ (thicken n o e) (refl_equal _)).
  destruct k.
  elimtype False; destruct a; absurd (e = o); auto.
  destruct s.
  destruct a.
  assumption.
Qed.



Require Import List.

Inductive AllDifferent A : list A -> Prop :=
| nil'  :
  AllDifferent A nil
| cons' : forall x xs,
  AllDifferent A xs -> ~In x xs -> AllDifferent A (x :: xs).
Implicit Arguments AllDifferent [A].

Lemma AllDifferent_injection A B (f : A -> B) x : (forall u v, f u = f v -> u = v) -> AllDifferent x -> AllDifferent (map f x).
  intros; induction x; simpl.
  apply nil'.
  apply cons'; inversion H0.
  apply IHx; assumption.
  contradict H4.
  destruct (in_map_iff f x (f a)).
  destruct (H5 H4).
  destruct H7.
  rewrite <- (H _ _ H7).
  assumption.
Qed.


Lemma In_P_reduce X (P : X -> Prop) o xs :
  (forall x : X, In x (o :: xs) -> P x) ->
   forall x : X, In x xs -> P x.
  intros.
  apply H.
  right.
  assumption.
Qed.

Definition map' X Y (P : X -> Prop) (f : forall x : X, P x -> Y) :
  forall xs : list X, (forall x, In x xs -> P x) -> list Y.
fix 5.
intros X Y P f xs P'.
destruct xs.
exact nil.
refine (f x (P' _ _) :: map' _ _ _ f xs (In_P_reduce _ _ _ _ P')).
left; reflexivity.
Defined.

Theorem map'_length X Y P f xs O : length xs = length (map' X Y P f xs O).
  intros; induction xs.
  reflexivity.
  simpl; rewrite (IHxs (In_P_reduce _ _ _ _ O)).
  reflexivity.
Qed.


Lemma thicken_In_inj n o a x H H' :
  In (thicken' n o a H)
     (map' _ _ (fun e => o <> e) (thicken' n o) x H') ->
  In a x.
  intros; induction x.
  inversion H0.
  simpl in H0.
  destruct H0.
  left.
  rewrite (thick_and_thin _ o a H).
  rewrite (thick_and_thin _ o a0 (H' a0 (or_introl (In a0 x) (refl_equal a0)))).
  rewrite H0.
  reflexivity.
  right.
  eapply IHx.
  apply H0.
Qed.

Lemma saturation n : forall x : list (Fin n),
  AllDifferent x -> length x = n -> forall f, In f x.
  intros; induction n.
  apply (no_fin0 f).
  destruct x.
  inversion H0.
  destruct (fin_eq_dec f f0).
  left; congruence.
  right.
  injection H0; clear H0; intro H0.
  inversion H.
  clear H1 H2 x0 xs.
  
  assert (forall e, In e x -> f0 <> e).
  intros; contradict H4; congruence.
  pose (map' _ _ _ (thicken' _ f0) x H1).
  
  Lemma AllDifferent_map'_thicken' n o x (H : (forall e, In e x -> o <> e)) :
    AllDifferent x ->
    (AllDifferent
      (map' _ _
        (fun e => o <> e)
        (thicken' n o) x
        H)).
    intros; induction x.
    apply nil'.
    simpl; apply cons'; inversion H0.
    apply IHx; assumption.
    contradict H4.
    eapply thicken_In_inj.
    apply H4.
  Qed.
  pose (AllDifferent_map'_thicken' _ _ _ H1 H3).
  
  assert (length l = n).
  rewrite <- H0.
  rewrite (map'_length _ _ _ (thicken' n f0) x H1).
  reflexivity.
  
  pose (IHn _ a H2).
  pose (i (thicken' _ f f0 n0)).
  assert (f0 <> f).
  auto.
  pose (thicken_In_inj _ f0 f x H5 H1).
  apply i1.
  apply i.
Qed.

Definition Cardinality : nat -> Set -> Prop :=
  fun n A => exists l : list A, length l = n /\ AllDifferent l.

Theorem pigeonhole_principle m : ~ Cardinality (S m) (Fin m).
  unfold Cardinality.
  intros; intro.
  destruct H; destruct H.
  destruct x.
  inversion H.
  case (In_dec (@fin_eq_dec _) f x); inversion H0.
  contradiction.
  injection H; intro H'.
  pose (saturation _ x H3 H' f).
  contradiction.
Qed.

Theorem Cardinality_n_Fin_n n : Cardinality n (Fin n).
  induction n.
  
  exists nil; split; [ reflexivity | apply nil'].
  
  destruct IHn.
  destruct H.
  exists (scum :: map (@bump _) x); split.
  
  simpl.
  rewrite map_length.
  congruence.
  
  apply cons'.
  apply AllDifferent_injection.
  apply bump_injection.
  assumption.
  clear H H0.
  induction x.
  auto.
  contradict IHx.
  inversion IHx.
  absurd (bump a = scum); auto.
  apply bump_isn't_scum.
  apply H.
Qed.

Theorem not_gt_Cardinality_n_Fin_m n m : n > m -> ~Cardinality n (Fin m).
  intros.
  
  Lemma lt_diff n m : n > m -> exists d, n = S d + m.
    unfold gt; unfold lt.
    intros n m H; induction H.
    exists 0; reflexivity.
    destruct IHle.
    exists (S x).
    rewrite H0.
    reflexivity.
  Qed.
  destruct (lt_diff n m); auto.
  rewrite H0; clear H0 H n.
  induction x.
  
  exact (pigeonhole_principle m).
  
  contradict IHx.
  destruct IHx.
  destruct H.
  inversion H0.
  rewrite <- H1 in H; inversion H.
  exists xs; split; auto.
  rewrite <- H3 in H; injection H.
  auto.
Qed.
(* Another triumph of the pigeonhole principle *)

Require Import Arith.
Theorem fin_different n m : n <> m -> Fin n <> Fin m.
  intros n m ne; intro H.
  destruct (not_eq _ _ ne);
    [ pose (Cardinality_n_Fin_n m) as p; rewrite <- H in p |
      pose (Cardinality_n_Fin_n n) as p; rewrite    H in p ];
    eapply not_gt_Cardinality_n_Fin_m;
      try apply p; auto with arith.
Qed.

Theorem fin_injective n m : Fin n = Fin m -> n = m.
  intros; destruct (eq_nat_dec n m).
  assumption.
  pose (fin_different _ _ n0); contradiction.
Qed.