Permalink
Find file
Fetching contributors…
Cannot retrieve contributors at this time
114 lines (93 sloc) 2.65 KB
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.