coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: Elimination of an inductive object of sort Prop (Re: [Coq-Club] more on vectors)
chronological Thread
- From: Adam Koprowski <adam.koprowski AT gmail.com>
- To: Martijn Vermaat <martijn AT vermaat.name>
- Cc: coq-club <coq-club AT inria.fr>, Dimitri Hendriks <diem AT xs4all.nl>
- Subject: Re: Elimination of an inductive object of sort Prop (Re: [Coq-Club] more on vectors)
- Date: Wed, 28 Apr 2010 16:30:06 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=oksgauY2FLSQ+d6Y9DpE21hGqSkiHRah/Wh7cM63BAFETy5kiXXsBWup91vmbNU/x4 l6E5iVYESm8vfU18f/Peb+x8YF+rrqv/fYk5IdvCSVcpwFUOxmW7lHyzIFwxY7dZHngG 70RxzOVDAOjx16xqmJLWLvBi35IQvevm66NdM=
In the definitions of functions on vectors such as take, drop, and nth,
we would use proofs of 'le' ord 'lt', e.g.:
Definition vtake (n m : nat) : n <= m -> vector m -> vector n.
But unfortunately, we cannot deconstruct the proof of n <= m since it
lives in Prop.
Why would you want to de-construct such a proof? You may want to take a look at the CoLoR library [1], which has a rich set of functions/results on vectors [2].
Best,
Adam
Adam Koprowski [http://adam-koprowski.net]
R&D @ MLstate [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]
- Elimination of an inductive object of sort Prop (Re: [Coq-Club] more on vectors), Martijn Vermaat
- Re: Elimination of an inductive object of sort Prop (Re: [Coq-Club] more on vectors), Adam Koprowski
- Re: Elimination of an inductive object of sort Prop (Re: [Coq-Club] more on vectors), Roman Beslik
- <Possible follow-ups>
- Re: Elimination of an inductive object of sort Prop (Re: [Coq-Club] more on vectors), Adam Chlipala
Archive powered by MhonArc 2.6.16.