Library BoundedNat.bounded_nat

Author: Jean-François Monin, Verimag, Université Grenoble Alpes

Similar to finite_set from itp13 with

odd/F1 renamed as even/FO
the parameter is the cardinal
definition of addition (to be used in even_bounded_nat)

Require Import Utf8.

Bounded natural numbers

The type t n represents a finite set of cardinal n, whose elements are numbered from FO to FS (... (FS FO)

Inductive t : nat → Set :=
    | FO {n} : t (S n)
    | FS {n} : t n → t (S n).

Fixpoint forget {n} (i : t n) : nat :=
  match i with
  | FO ⇒ O
  | FS i ⇒ S (forget i)
  end.

Small inversion.

Here we have no shape for 0 and 2 shapes for (S n)

Inductive shape_O : t 0 → Set :=.

Inductive shape_S (n : nat) : t (S n) → Set :=
    | shape_S_F0 : shape_S n FO
    | shape_S_FS : ∀ i : t n , shape_S n (FS i).

Definition t_inv {n} (i : t n) :
    match n with
    | O ⇒ shape_O
    | S n ⇒ shape_S n
    end i.
Proof. destruct i; constructor. Defined.

Generic use

Section sec_example.
  Variable P : ∀ n, t n → Prop.
  Lemma case_t_S n :
    P (S n) FO → (∀ i, P (S n) (FS i)) →
    ∀ (i : t (S n)), P (S n) i.
  Proof.
    intros P0 PS i.

Here destruct i and inversion i don't work.

    destruct (t_inv i) as [ | i]; cbn.
    - exact P0.
    - apply PS.
  Qed.
End sec_example.

Addition

An administrative lifting function (lift1) is needed.

Definition t_n_Sm {n m} (i: t (S (m + n))) : t (m + S n).
  rewrite <- plus_n_Sm; exact i.
Defined.

Fixpoint lift1 m {n} (i : t n) : t (m + n) :=
  match i in t n return t (m + n) with
  | FO ⇒ t_n_Sm FO
  | FS i ⇒ t_n_Sm (FS (lift1 m i))
  end.

Fixpoint Fplus {n m : nat} (i : t n) (j : t m) : t (n + m) :=
  match i with
  | @FO n ⇒ lift1 (S n) j
  | FS i ⇒ FS (Fplus i j)
  end.