The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Note that [n] can be larger than the length of the lists, in which case [nth] will return the default element and hence you will need an assumption [rel dA dB] in [nth_dep]. Otherwise I don't see why would it not be possible to prove your lemma. Do you have some specific problems?

  If indexing elements plays important role in your development I suggest you consider switching from lists to vectors: then no default elements are needed as all indexes are always within range. 
  If you decide to do that I also suggest writing some generic operations on your datatypes (instead of inductive definitions in the spirit of your test). For instance here you will need a function checking that a property holds point-wise for two vectors of equal lengths. If interested you'll find such function ready for you in the CoLoR library: see [Vforall2n] at http://color.inria.fr/doc/CoLoR.Util.Vector.VecUtil.html#S.Vforall2_sec.

   Cheers,
    Adam

On Sun, Apr 26, 2009 at 13:24, dimitrisg7 <dvekris AT hotmail.com> wrote:

Hello to everyone!

Is it possible to get the nth object (of type rel (nth ...) (nth ...)) in
the following inductive definition (I do not think that I can) or should I
make some changes in my definitions?

Section testing.
Set Implicit Arguments.

Variable A : Type.
Variable dA : A.
Variable B : Type.
Variable dB : B.
Variable rel: A -> B -> Type.

Inductive test : list A -> list B -> Type :=
| constr1 : test nil nil
| constr2 : forall a b al bl, rel a b -> test al bl -> test (a::al)(b::bl).

Definition nth_dep n al bl (t : test al bl) : rel(nth n al dA)(nth n bl dB).
Proof.
(* get nth object *)
Admitted.

End testing.

-----
Never say never.
--
View this message in context: http://www.nabble.com/Nth---dependent-types.-tp23241301p23241301.html
Sent from the Coq mailing list archive at Nabble.com.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================