## Saturday, 11 October 2008

### eq_fin_dec via NoConfusion

`Require Import JMeq.Infix "==" := JMeq (at level 30).Notation "X =/= Y" := (X == Y -> False) (at level 30).Inductive Fin : nat -> Set :=| fz n : Fin (S n)| fs n : Fin n -> Fin (S n).Fixpoint Fin_NoConfusion (P : Type) (n : nat) (f f' : Fin n) {struct f} :=  match f, f' with    | fz _, fz _ => P -> P    | fs _ f, fs _ f' => (f == f' -> P) -> P    | _, _ => P  end.Definition Fin_noConfusion P n (f f' : Fin n) : f == f' -> Fin_NoConfusion P n f f'.intros P n f f' Eq.elim Eq.elim f;  simpl; intros; tauto.Defined.Definition fs_injective (P : Type) (n : nat) (f f' : Fin n)  : (f == f' -> P) -> (fs n f == fs n f' -> P)  := fun m Eq =>    Fin_noConfusion P (S n) (fs n f) (fs n f') Eq m.Definition fz_fs_clash (P : Type) (n : nat) (f : Fin n)  : fz n == fs n f -> P  := fun Eq =>    Fin_noConfusion P (S n) (fz n) (fs n f) Eq.Definition eq_fin_dec n : forall f f' : Fin n, {f == f'} + {f =/= f'}.refine (fix eq_fin_dec n (f f' : Fin n) {struct f'} : {f == f'} + {f =/= f'} :=  match f in Fin n, f' in Fin n' return n = n' -> {f == f'} + {f =/= f'} with    | fz _, fz _ => _    | fs _ _, fz _ => _    | fz _, fs _ _ => _    | fs _ _, fs _ _ => _  end (refl_equal _));intro Eq; injection Eq; clear Eq; intro Eq.left; rewrite Eq; reflexivity.right; rewrite Eq; intro; exact (fz_fs_clash False _ _ H).right; rewrite <- Eq; intro; exact (fz_fs_clash False _ _ (sym_JMeq H)).clear f f' n; subst n0.destruct (eq_fin_dec n1 f0 f1).left; elim j; reflexivity.right; intro; apply f; exact (fs_injective _ _ _ _ (fun Eq => Eq) H).Defined.`