Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Contribute to GitLab
Sign in
Toggle navigation
C
cpdt
Project
Project
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
research
cpdt
Commits
5535d6ec
Commit
5535d6ec
authored
16 years ago
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Exercise added at end of MoreDep
parent
56efc518
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
17 additions
and
0 deletions
+17
-0
MoreDep.v
src/MoreDep.v
+17
-0
No files found.
src/MoreDep.v
View file @
5535d6ec
...
...
@@ -1078,3 +1078,20 @@ Eval simpl in matches a_star "a".
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
This diff is collapsed.
Click to expand it.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment