Library CoLoR.Util.Nat.BoundNat

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2014-12-11
  • Adam Koprowski, 2009-04-24
  • 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) _.