Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Data Structures

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Data Structures


chronological Thread 
  • From: Adam Koprowski <adam.koprowski AT gmail.com>
  • To: Dimitris Vekris <dvekris AT hotmail.com>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Data Structures
  • Date: Mon, 16 Mar 2009 11:42:32 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=qL3eItrCL4fpjQV+FO7hj6O5IxmxoJfZJS6GP4kq9i2NBfGNxp9/tVtC8QSSCUKM9t ZU/i2TgIcTvHLUSy/2OTRt6BJ8rchLCNfzgistvFrVdSRP6JJyks0gIPtipoTU4Jw+2q kk9yl5uESvIYEzLOjuPbId18KsNGibB+QiZhw=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

   Dear Dimitris,

I would also like to get rid of Variable dummy, which expresses nothing in my proof and is a pain in the ass for me when it comes to proving lemmas that are associated with Data.
  To get rid of dummy you can consider switching from lists to vectors. Types of vectors carry the information on its length so you can get n'th element of a vector without providing a default value (instead you will need to prove that the index you are using is within the vector). Using vectors can be a bit painful at the beginning due to type dependencies but you may consider using a library, such as CoLoR, which provides numerous functions operating on vectors making your life much easier.

What I am searching for is a way to express this property inside "list Data".
  As for building the property into list, if I understand you correctly, what would you say about this:

Inductive data_prop (m : nat) : nat -> Set :=
| dp_nil : data_prop m 0
| dp_cons : forall el, func el < m -> data_prop m 0 -> data_prop m 0
| dp_consX : forall el i, func el = m -> data_prop m i -> data_prop m (S i).

  'data_prop m l' gives you a list with your property with parameters 'm' and 'l'.

   Cheers,
   Adam

--
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================



Archive powered by MhonArc 2.6.16.

Top of Page