## Wednesday, 17 September 2008

### 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.`