# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223488520 14400
# Node ID bc12662ae89543cd324e28b2cb90001c01615650
# Parent  070f4de923112bfaa03ceaa01de3c5f849c4984b
Exercise added at end of MoreDep

diff -r 070f4de92311 -r bc12662ae895 src/MoreDep.v
--- a/src/MoreDep.v	Wed Oct 08 10:01:26 2008 -0400
+++ b/src/MoreDep.v	Wed Oct 08 13:55:20 2008 -0400
@@ -1078,3 +1078,20 @@
 Eval simpl in matches a_star "b".
 Eval simpl in matches a_star "aa".
 (* end hide *)
+
+
+(** * Exercises *)
+
+(** %\begin{enumerate}%#<ol>#
+
+%\item%#<li># Define a kind of dependently-typed lists, where a list's type index gives a lower bound on how many of its elements satisfy a particular predicate.  In particular, for an arbitrary set [A] and a predicate [P] over it:
+%\begin{enumerate}%#<ol>#
+  %\item%#<li># Define a type [plist : nat -> Set].  Each [plist n] should be a list of [A]s, where it is guaranteed that at least [n] distinct elements satisfy [P].  There is wide latitude in choosing how to encode this.  You should try to avoid using subset types or any other mechanism based on annotating non-dependent types with propositions after-the-fact.#</li>#
+  %\item%#<li># Define a version of list concatenation that works on [plist]s.  The type of this new function should express as much information as possible about the outpit [plist].#</li>#
+  %\item%#<li># Define a function [plistOut] for translating [plist]s to normal [list]s.#</li>#
+  %\item%#<li># Define a function [plistIn] for translating [list]s to [plist]s.  The type of [plistIn] should make it clear that the best bound on [P]-matching elements is chosen.  You may assume that you are given a dependently-typed function for deciding instances of [P].#</li>#
+  %\item%#<li># Prove that, for any list [ls], [plistOut (plistIn ls) = ls].  This should be the only part of the exercise where you use tactic-based proving.#</li>#
+  %\item%#<li># Define a function [grab : forall n (ls : plist (S n)), sig P].  That is, when given a [plist] guaranteed to contain at least one element satisfying [P], [grab] produces such an element.  [sig] is the type family of sigma types, and [sig P] is extensionally equivalent to [{x : A | P x}], though the latter form uses an eta-expansion of [P] instead of [P] itself as the predicate.#</li>#
+#</ol>#%\end{enumerate}% #</li>#
+   
+#</ol>#%\end{enumerate}% *)
\ No newline at end of file