# Library CoLoR.Util.Nat.BoundNat

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2014-12-11
• Leo Ducas, 2007-08-06
Type of natural numbers strictly smaller that some bound.

Set Implicit Arguments.

Definition N n := sig (gt n).

Definition N_ n := @exist nat (gt n).

Definition N_val {n} (x : N n) : nat := proj1_sig x.

Coercion N_val : N >-> nat.

Definition N_prf {n} (x : N n) : x < n := proj2_sig x.

Coercion N_prf : N >-> lt.

Definition zero {n} : N (S n).

Definition any_of_N0 {B : Type} : N 0 -> B.

Lemma inj_N_val n : injective (@N_val n).

Lemma N_eq {n} : forall x y : N n, N_val x = N_val y <-> x = y.

Lemma N_eq_dec {n} : forall x y : N n, {x=y}+{~x=y}.

List n-1; ..; 0 of the n first natural numbers starting from 0 in reverse order.

Fixpoint nats_decr_lt n :=
match n with
| 0 => nil
| S n' => n' :: nats_decr_lt n'
end.

Definition nats_incr_lt n := rev' (nats_decr_lt n).

Lemma In_nats_decr_lt : forall n x, x < n <-> In x (nats_decr_lt n).

Lemma length_nats_decr_lt n : length (nats_decr_lt n) = n.

List @N_ n (n-1) _; ..; @N_ n 0 _ of all the elements of N n in reverse order.

Section list_N.

Variable n : nat.

Lemma L_ k : S k < n -> k < n.

Fixpoint L_aux k :=
match k as k return k<n -> list (N n) with
| 0 => fun h => N_ h :: nil
| S k' => fun h => N_ h :: L_aux k' (L_ h)
end.

Lemma length_L_aux : forall k (hk : k<n), length (L_aux hk) = S k.

Lemma nth_L_aux x :
forall k (h : k<n) i, i <= k -> N_val (nth i (L_aux h) x) = k - i.

Lemma In_L_aux_elim x k (h : k<n) :
In x (L_aux h) -> exists i, N_val x = k - i.

Lemma In_L_aux :
forall k (h : k<n) i (p : i<n), i <= k -> In (N_ p) (L_aux h).

End list_N.

Definition L n :=
match n return list (N n) with
| 0 => nil
| S n' => L_aux (le_n (S n'))
end.

Lemma nth_L n x i : i < n -> N_val (nth i (L n) x) = pred n - i.

Lemma In_L n i (p : i<n) : In (N_ p) (L n).

Lemma In_L_elim n x : In x (L n) -> exists i, N_val x = n - i.

Lemma length_L n : length (L n) = n.

Lemma nodup_L_aux {n} : forall k (hk : k < n), nodup (L_aux hk).

Lemma nodup_L n : nodup (L n).

Functions between N m and N n.

Lemma N_inj_le m n (f : N m -> N n) : injective f -> m <= n.

Lemma N_bij_eq m n (f : N m -> N n) : bijective f -> m = n.

Vector @N_ n (n-1) _; ..; @N_ n 0 _ of all the elements of N n in reverse order.

Section vec_N.

Variable n : nat.

Fixpoint V_aux k :=
match k as k return k<n -> vector (N n) (S k) with
| 0 => fun h => Vcons (N_ h) Vnil
| S k' => fun h => Vcons (N_ h) (V_aux k' (L_ h))
end.

Lemma Vnth_V_aux :
forall k (h : k<n) i (hi : i < S k), N_val (Vnth (V_aux h) hi) = k - i.

Lemma Vin_V_aux_elim x k (h : k<n) :
Vin x (V_aux h) -> exists i, N_val x = k - i.

Lemma Vin_V_aux :
forall k (h : k<n) i (p : i<n), i <= k -> Vin (N_ p) (V_aux h).

End vec_N.

Definition V n :=
match n return vector (N n) n with
| 0 => Vnil
| S n' => V_aux (le_n (S n'))
end.

Lemma Vnth_V n i (hi : i < n) : N_val (Vnth (V n) hi) = pred n - i.

Lemma Vin_V n i (p : i<n) : Vin (N_ p) (V n).

Lemma Vin_V_elim n x : Vin x (V n) -> exists i, N_val x = n - i.

Multiplicity and sorting properties.

Lemma map_N_val_L_aux n :
forall k (hk : k<n), map N_val (L_aux hk) = nats_decr_lt (S k).

Lemma map_N_val_L n : map N_val (L n) = nats_decr_lt n.

Lemma lelistA_map_N_val n R (a : N n) :
forall l, lelistA (Rof R N_val) a l -> lelistA R a (map N_val l).

Lemma sort_map_N_val n R :
forall l : list (N n), sort (Rof R N_val) l -> sort R (map N_val l).

Lemma multiplicity_nats_decr_lt i :
forall n, multiplicity (list_contents eq_nat_dec (nats_decr_lt n)) i
= if lt_ge_dec i n then 1 else 0.

Lemma multiplicity_L_aux n (i : N n) : forall k (kn : k < n),
multiplicity (list_contents N_eq_dec (L_aux kn)) i
= if le_dec i k then 1 else 0.

Lemma multiplicity_L n (i : N n) :
multiplicity (list_contents N_eq_dec (L n)) i = 1.

Lemma multiplicity_map_N_val n i (hi : i<n) :
forall l, multiplicity (list_contents eq_nat_dec (map N_val l)) i
= multiplicity (list_contents N_eq_dec l) (N_ hi).

Lemma multiplicity_map_N_val_notin n i (hi : i>=n) : forall l : list (N n),
multiplicity (list_contents eq_nat_dec (map N_val l)) i = 0.

Given n:nat, a predicate Pr : N n -> Prop and a function P that can check whether Pr i is true, check_seq Pr P checks whether Pr i is true for all i strictly smaller than n.

Section Check_seq_aux.

Variables (n : nat) (Pr : N n -> Prop) (P : forall i : N n, option (Pr i)).

Program Fixpoint check_seq_aux p (H : forall i : N n, N_val i < p -> Pr i)
{measure (n - p)} : option (forall i : N n, Pr i) :=
match le_lt_dec n p with
| left _ => Some _
| right cmp =>
match P (N_ cmp) with
| None => None
| Some _ => @check_seq_aux (S p) _ _
end
end.

End Check_seq_aux.

Program Definition check_seq (n : nat) (Pr : N n -> Prop)
(P : forall (i : N n), option (Pr i)) : option (forall (i : N n), Pr i)
:= check_seq_aux _ P (p:=0) _.