Library Equations.Fin

An example development of the fin datatype using equations.

fin n is the type of naturals smaller than n.

Inductive fin : nat -> Set :=
| fz : forall {n}, fin (S n)
| fs : forall {n}, fin n -> fin (S n).
Derive Signature for fin.

NoConfusion For fin.

Derive NoConfusion NoConfusionHom for fin.

We can inject it into nat.

Equations fog {n} (f : fin n) : nat :=
fog (n:=?(S n )) (@fz n) := 0 ;
fog (fs f) := S (fog f).

The injection preserves the number:

Require Import FunctionalInduction.

Lemma fog_inj {n} (f : fin n) : fog f < n.
Proof with auto with arith. intros.
depind f; simp fog...
Qed.

Of course it has an inverse.

Equations gof n : fin (S n) :=
gof O := fz ;
gof (S n) := fs (gof n).

Lemma fog_gof n : fog (gof n) = n.
Proof with auto with arith. intros.
funind (gof n) gofn; simp fog gof...
Qed.

Equations fin_inj_one {n} (f : fin n) : fin (S n) :=
fin_inj_one fz := fz;
fin_inj_one (fs f) := fs (fin_inj_one f).

Inductive le : nat -> nat -> Type :=
| le_O n : 0 <= n
| le_S {n m} : n <= m -> S n <= S m
where "n <= m" := (le n m).
Derive Signature for le.

Equations le_S_inv {n m} (p : S n <= S m) : n <= m :=
le_S_inv (le_S p) := p.

Equations fin_inj {n} {m} (f : fin n) (k : n <= m) : fin m :=
fin_inj fz (le_S p) := fz;
fin_inj (fs f) (le_S p) := fs (fin_inj f p).

Let's do some arithmetic on fin

Won't pass the guardness check which diverges anyway.

Inductive finle : forall (n : nat) (x : fin n) (y : fin n), Prop :=
| leqz : forall {n j}, finle (S n) fz j
| leqs : forall {n i j}, finle n i j -> finle (S n) (fs i) (fs j).

Scheme finle_ind_dep := Induction for finle Sort Prop.

Instance finle_ind_pack n x y : DependentEliminationPackage (finle n x y) :=
{ elim_type := _ ; elim := finle_ind_dep }.

Arguments finle {n}.

Require Vectors.Vector.
Arguments Vector.nil {A}.
Arguments Vector.cons {A} _ {n}.
Notation vnil := Vector.nil.
Notation vcons := Vector.cons.

Equations nth {A} {n} (v : Vector.t A n) (f : fin n) : A :=
nth (vcons a v) fz := a ;
nth (vcons a v) (fs f) := nth v f.

Equations tabulate {A} {n} (f : fin n -> A) : Vector.t A n by struct n :=
tabulate (n:=O) f := vnil ;
tabulate (n:=(S n)) f := vcons (f fz) (tabulate (f ∘ fs)).

Below recursor for fin.

Equations(noind) Below_fin (P : forall n, fin n -> Type) {n} (v : fin n) : Type :=
Below_fin P fz := unit ;
Below_fin P (fs f) := (P _ f * Below_fin P f)%type.

Hint Rewrite Below_fin_equation_2 : Below.

Equations(noeqns noind) below_fin (P : forall n, fin n -> Type)
  (step : forall n (v : fin n), Below_fin P v -> P n v)
  {n} (v : fin n) : Below_fin P v :=
below_fin P step fz := tt ;
below_fin P step (@fs n f) :=
  let bf := below_fin P step f in
    (step n f bf , bf ).

Global Opaque Below_fin.

Definition rec_fin (P : forall n, fin n -> Type) {n} v
  (step : forall n (v : fin n), Below_fin P v -> P n v) : P n v :=
  step n v (below_fin P step v).

Import Equations.Below.

Instance fin_Recursor n : Recursor (fin n) :=
  { rec_type := fun v => forall (P : forall n, fin n -> Type) step, P n v;
    rec := fun v P step => rec_fin P v step }.