coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
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)
=====================================================
- [Coq-Club] Data Structures, Dimitris Vekris
- Re: [Coq-Club] Data Structures, Edsko de Vries
- Re: [Coq-Club] Data Structures, Adam Koprowski
- Re: [Coq-Club] Data Structures,
dimitrisg7
- Re: [Coq-Club] Data Structures,
muad
- Re: [Coq-Club] Data Structures,
dimitrisg7
- Re: [Coq-Club] Data Structures, Edsko de Vries
- Re: [Coq-Club] Data Structures,
Adam Koprowski
- Re: [Coq-Club] Data Structures, Edsko de Vries
- Re: [Coq-Club] Data Structures, Adam Chlipala
- Re: [Coq-Club] Data Structures,
muad
- Re: [Coq-Club] Data Structures, dimitrisg7
- Re: [Coq-Club] Data Structures, Frederic Blanqui
- Re: [Coq-Club] Data Structures,
dimitrisg7
- Re: [Coq-Club] Data Structures,
muad
- Re: [Coq-Club] Data Structures,
dimitrisg7
Archive powered by MhonArc 2.6.16.