Lists Projections

(* LIST PROJECTIONS      *)
(* by Venanzio Capretta  *)
(* Coq version 6.2.3     *)

(* We define a projection from lists that uses finite sets.   *)
(* It has the advantage over the projection nth which uses    *)
(* natural numbers, that there is no need for a defaut value. *)

Require Export PolyList.
Require Export Finite_Sets.

Section Finite_Projections.

Variable A : Set.

Fixpoint fin_proj' [l:(list A)] : (m:nat)(gt (length l) m) -> A :=
<[l:(list A)](m:nat)(gt (length l) m) -> A>
Cases l of
    nil => [m][p](False_rec A (lt_n_O m p))
  | (cons a l') => [m : nat]
                   <[m:nat](gt (length (cons a l')) m) -> A>
                   Cases m of
                       O => [p]a
                     | (S m') => [p](fin_proj' l' m' (gt_S_n m' (length l') p))
                   end
end.

Definition fin_proj : (l : (list A))(Finite (length l)) -> A :=
[l][i](fin_proj' l (fin_extr i) (fin_extr_gt i)).

End Finite_Projections.

Syntactic Definition Fin_proj := (fin_proj ?).

25/02/99, 14:36