Mercurial > cpdt > repo
comparison src/MoreDep.v @ 102:d829cc24faee
Add a darn newline
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 08 Oct 2008 14:18:35 -0400 |
| parents | bc12662ae895 |
| children | 22f111d5cda2 |
comparison
equal
deleted
inserted
replaced
| 101:bc12662ae895 | 102:d829cc24faee |
|---|---|
| 1085 (** %\begin{enumerate}%#<ol># | 1085 (** %\begin{enumerate}%#<ol># |
| 1086 | 1086 |
| 1087 %\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: | 1087 %\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: |
| 1088 %\begin{enumerate}%#<ol># | 1088 %\begin{enumerate}%#<ol># |
| 1089 %\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># | 1089 %\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># |
| 1090 %\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># | 1090 %\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 output [plist].#</li># |
| 1091 %\item%#<li># Define a function [plistOut] for translating [plist]s to normal [list]s.#</li># | 1091 %\item%#<li># Define a function [plistOut] for translating [plist]s to normal [list]s.#</li># |
| 1092 %\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># | 1092 %\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># |
| 1093 %\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># | 1093 %\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># |
| 1094 %\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># | 1094 %\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># |
| 1095 #</ol>#%\end{enumerate}% #</li># | 1095 #</ol>#%\end{enumerate}% #</li># |