Set Implicit Arguments. Inductive bnat: nat -> Set := | bO n: bnat (S n) | bS n: bnat n -> bnat (S n). Fixpoint to_nat n (b: bnat n): nat := match b with | bO _ => 0 | bS _ x => S (to_nat x) end. Section alt_rect. Variables (P: forall n: nat, bnat (S n) -> Type) (Pz: forall p, P (bO p)) (Ps: forall n (b: bnat (S n)), P b -> P (bS b)). Let R (n: nat): bnat n -> Type := match n with | O => fun _ => False | S _ => @P _ end. Fixpoint RS (n : nat): forall (b : bnat n), R b -> R (bS b) := match n return forall (b : bnat n), R b -> R (bS b) with | O => fun x f => False_rect _ f | S n' => fun x f => Ps f end. Definition bnat_Srect (n: nat) (nb: bnat (S n)): P nb := bnat_rect R Pz RS nb. End alt_rect. Lemma bnat_cases n (x: bnat (S n)): { p | x = bS p } + { x = bO n }. revert n x. apply bnat_Srect; [right | left; exists b]; reflexivity. Defined. Lemma bnat_0: bnat 0 -> False. Proof with auto. cut (forall n, bnat n -> n <> 0%nat). intros H H0. apply (H _ H0)... induction 1; intro; discriminate. Qed. Require Import List list_util. Definition bnat_bound n (b: bnat n): nat := n. Definition pred n (b: bnat n): option (bnat (Peano.pred (bnat_bound b))) := match b return option (bnat (Peano.pred (bnat_bound b))) with | bO _ => None | bS x y => Some y end. Require Import util. Lemma eq_bS_inv n (x y: bnat n): bS x = bS y -> x = y. Proof with auto. intros. apply option_eq_inv. replace (Some x) with (pred (bS x))... replace (Some y) with (pred (bS y))... rewrite H... Qed. Require Import EquivDec. Instance bnat_eq_dec n: EqDec (bnat n) eq. induction n. repeat intro. elimtype False. apply (bnat_0 x). repeat intro. destruct (bnat_cases x) as [[x' e] | e]; destruct (bnat_cases y) as [[y' e'] | e']; subst. destruct (IHn x' y'); [left | right]. rewrite e. reflexivity. exact (fun H => c (eq_bS_inv H)). right. discriminate. right. discriminate. left. reflexivity. Defined. Definition all_bnats := fix F (n: nat): list (bnat n) := match n with | O => nil | S m => bO m :: map (@bS m) (F m) end. Instance bnats n: ExhaustiveList (bnat n) := { exhaustive_list := all_bnats n }. Proof with auto. dependent induction n; intro x. elimtype False. apply bnat_0... destruct (bnat_cases x) as [[p e] | e]; subst; [right | left]... Defined. Lemma NoDup_bnats n: NoDup (bnats n). Proof with auto. induction n. apply NoDup_nil. simpl. apply NoDup_cons... intro. destruct (fst (in_map_iff (@bS n) (all_bnats n) (bO n)) H). destruct H0. discriminate. apply NoDup_map... intros. apply eq_bS_inv... Qed.