Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Pierre Letouzey
prog-lmfi
Commits
157fd6a8
Commit
157fd6a8
authored
Nov 18, 2020
by
Pierre Letouzey
Browse files
solutions for TD3
parent
89f2e7cb
Changes
4
Hide whitespace changes
Inline
Side-by-side
correc
tions/td1.v
→
solu
tions/td1.v
View file @
157fd6a8
File moved
correc
tions/td2.v
→
solu
tions/td2.v
View file @
157fd6a8
File moved
solutions/td3.v
0 → 100644
View file @
157fd6a8
Require
Import
Bool
Arith
List
.
Import
ListNotations
.
Set
Implicit
Arguments
.
(
*
EXERCISE
1
:
classical
functions
on
lists
*
)
(
*
The
inductive
definition
of
lists
,
once
again
:
*
)
Print
list
.
(
*
Syntax
about
lists
,
provided
by
module
ListNotations
imported
above
*
)
Check
[].
(
*
is
equivalent
to
:
nil
*
)
About
"::"
.
(
*
is
equivalent
to
:
cons
*
)
Check
1
::
[].
Check
[
1
;
2
;
3
].
(
*
is
equivalent
to
*
)
Check
1
::
(
2
::
(
3
::
[])).
(
*
A
first
function
on
lists
:
length
*
)
Fixpoint
length
{
A
}
(
l
:
list
A
)
:=
match
l
with
|
[]
=>
0
|
x
::
q
=>
S
(
length
q
)
end
.
Check
@
length
.
Compute
length
[
1
;
2
;
3
].
Compute
length
[
true
;
false
;
false
].
Check
[[
1
;
2
];[
3
];[];[
5
;
6
]].
(
*
Set
Printing
All
.
(
*
If
you
want
to
see
all
the
implicit
arguments
*
)
*
)
Check
length
[[
1
;
2
];[
3
];[];[
5
;
6
]].
Compute
length
[[
1
;
2
];[
3
];[];[
5
;
6
]].
(
*
Concatenation
*
)
Fixpoint
app
{
A
}
(
l1
l2
:
list
A
)
:=
match
l1
with
|
[]
=>
l2
|
x1
::
q1
=>
x1
::
app
q1
l2
end
.
Check
app
[
1
;
2
;
3
]
[
4
;
5
].
(
*
Using
Coq
standard
definition
of
app
:
*
)
Check
[
1
;
2
;
3
]
++
[
4
;
5
].
(
*
Reverse
(
in
the
"slow"
definition
,
i
.
e
.
quadratic
complexity
)
*
)
Fixpoint
rev
{
A
}
(
l
:
list
A
)
:=
match
l
with
|
[]
=>
[]
|
x
::
q
=>
rev
q
++
[
x
]
end
.
(
*
rev
[
1
;
2
;
3
;
4
]
=
rev
[
1
;
2
;
3
]
++
[
4
]
=
(
rev
[
1
;
2
])
++
[
3
])
++
[
4
]
=
(
rev
[
1
])
++
[
2
])
++
[
3
])
++
[
4
]
=
([]
++
[
1
])
++
[
2
])
++
[
3
])
++
[
4
]
cost
0
cost
1
cost
2
cost
3
total
cost
proportional
to
(
n
*
(
n
+
1
)
/
2
)
when
n
is
length
l
i
.
e
.
quadratic
*
)
(
*
Efficient
reverse
:
we
define
first
an
auxiliary
function
called
rev_app
,
which
is
almost
app
,
but
with
the
left
list
being
reversed
.
*
)
Fixpoint
rev_app
{
A
}
(
l1
l2
:
list
A
)
:=
match
l1
with
|
[]
=>
l2
|
x1
::
q1
=>
rev_app
q1
(
x1
::
l2
)
end
.
Compute
rev_app
[
1
;
2
;
3
]
[
4
;
5
].
(
*
And
then
:
*
)
Definition
fast_rev
{
A
}
(
l
:
list
A
)
:=
rev_app
l
[].
Compute
fast_rev
[
1
;
2
;
3
].
(
*
linear
in
the
size
of
l
*
)
(
*
map
and
filter
:
pretty
straightforward
*
)
Fixpoint
map
{
A
B
}
(
f
:
A
->
B
)
l
:=
match
l
with
|
[]
=>
[]
|
x
::
q
=>
f
x
::
map
f
q
end
.
Fixpoint
filter
{
A
}
(
f
:
A
->
bool
)
l
:=
match
l
with
|
[]
=>
[]
|
x
::
q
=>
if
f
x
then
x
::
filter
f
q
else
filter
f
q
end
.
(
*
fold
*
)
Compute
fold_right
Nat
.
add
0
[
1
;
2
;
3
].
(
*
sums
all
the
numbers
*
)
Compute
fold_left
Nat
.
add
[
1
;
2
;
3
]
0.
(
*
the
same
...
*
)
Check
fold_right
.
(
*
forall
A
B
:
Type
,
(
B
->
A
->
A
)
->
A
->
list
B
->
A
*
)
(
*
fold_right
f
a
[
x1
;
x2
;
x3
]
=
(
f
x1
(
f
x2
(
f
x3
a
))).
*
)
Fixpoint
fold_right
{
A
B
}
(
f
:
B
->
A
->
A
)
a
l
:=
match
l
with
|
[]
=>
a
|
x
::
q
=>
f
x
(
fold_right
f
a
q
)
end
.
Check
fold_left
.
(
*
:
forall
A
B
:
Type
,
(
A
->
B
->
A
)
->
list
B
->
A
->
A
*
)
(
*
fold_left
f
[
x1
;
x2
;
x3
]
a
=
f
(
f
(
f
a
x1
)
x2
)
x3
.
*
)
Fixpoint
fold_left
{
A
B
}
(
f
:
A
->
B
->
A
)
l
a
:=
match
l
with
|
[]
=>
a
|
x
::
q
=>
fold_left
f
q
(
f
a
x
)
end
.
(
*
Let
'
s
use
folds
to
rebuild
a
list
*
)
Compute
fold_right
(
fun
x
l
=>
x
::
l
)
[]
[
1
;
2
;
3
].
Compute
fold_left
(
fun
l
x
=>
x
::
l
)
[
1
;
2
;
3
]
[].
(
*
seq
*
)
Fixpoint
seq
start
len
:=
match
len
with
|
0
=>
[]
|
S
len
'
=>
start
::
seq
(
S
start
)
len
'
end
.
(
*
head
with
the
option
type
*
)
Definition
head
{
A
}
(
l
:
list
A
)
:
option
A
:=
match
l
with
|
[]
=>
None
|
x
::
q
=>
Some
x
end
.
Compute
head
[
1
;
2
;
3
].
(
*
head
with
a
default
answer
in
the
case
of
empty
list
*
)
Definition
head_dft
{
A
}
(
l
:
list
A
)
(
dft
:
A
)
:
A
:=
match
l
with
|
[]
=>
dft
|
x
::
q
=>
x
end
.
Compute
head_dft
[
1
;
2
;
3
]
0.
(
*
other
approaches
:
-
conditions
ensuring
that
the
list
isn
'
t
empty
(
proof
-
carrying
code
,
quite
complex
)
-
switch
from
list
to
a
vector
(
list
of
a
given
size
)
head
:
vector
A
(
S
n
)
->
A
(
dependent
-
type
programming
)
*
)
Fixpoint
last
{
A
}
(
l
:
list
A
)
:
option
A
:=
match
l
with
|
[]
=>
None
|
[
a
]
=>
Some
a
|
_
::
l
=>
last
l
end
.
Compute
last
[
1
;
2
;
3
].
Fixpoint
nth
{
A
}
n
(
l
:
list
A
)
(
dft
:
A
)
:=
match
n
,
l
with
|
_
,
[]
=>
dft
|
O
,
x
::
_
=>
x
|
S
n
,
_
::
q
=>
nth
n
q
dft
end
.
(
*
Left
as
exercise
:
last
with
default
value
or
nth
with
option
*
)
(
*
EXERCISE
2
:
executable
predicates
*
)
Fixpoint
forallb
{
A
}
(
f
:
A
->
bool
)
l
:=
match
l
with
|
[]
=>
true
|
x
::
q
=>
f
x
&&
forallb
f
q
(
*
or
more
lazy
:
if
f
x
then
forallb
f
q
else
false
*
)
end
.
Fixpoint
increasing
l
:=
match
l
with
|
[]
=>
true
|
[
x
]
=>
true
|
x
::
((
y
::
_
)
as
q
)
=>
(
x
<?
y
)
&&
increasing
q
end
.
(
**
As
shown
in
live
during
the
video
-
session
:
be
careful
not
to
forget
the
(
)
around
y
::
_
!!
*
)
(
*
Or
in
two
steps
(
longer
but
more
basic
hence
more
robust
)
*
)
Fixpoint
larger_than
x
l
:=
match
l
with
|
[]
=>
true
|
y
::
q
=>
(
x
<?
y
)
&&
larger_than
y
q
end
.
Definition
increasing_v2
l
:=
match
l
with
|
[]
=>
true
|
x
::
q
=>
larger_than
x
q
end
.
(
*
Or
more
generic
:
*
)
Fixpoint
forallb_successive
{
A
}
(
f
:
A
->
A
->
bool
)
l
:=
match
l
with
|
[]
=>
true
|
[
x
]
=>
true
|
x
::
((
y
::
_
)
as
q
)
=>
f
x
y
&&
forallb_successive
f
q
end
.
Definition
increasing
'
:=
forallb_successive
Nat
.
ltb
.
(
*
where
Nat
.
ltb
is
the
function
behind
the
<?
test
*
)
Compute
increasing
[
1
;
2
;
3
;
4
].
Compute
increasing
[
1
;
2
;
2
].
Definition
delta
k
:=
forallb_successive
(
fun
a
b
=>
a
+
k
<=?
b
).
Compute
delta
1
[
1
;
2
;
3
;
4
].
(
**
Exercise
3
:
Mergesort
*
)
(
*
First
,
a
solution
by
computing
first
the
desired
size
*
)
Fixpoint
split_at
{
A
}
(
l
:
list
A
)
n
:=
match
l
,
n
with
|
[],
_
=>
([],
[])
|
_
,
0
=>
([],
l
)
|
x
::
q
,
S
n
'
=>
let
'
(
l1
,
l2
)
:=
split_at
q
n
'
in
(
x
::
l1
,
l2
)
end
.
Definition
split
{
A
}
(
l
:
list
A
)
:=
split_at
l
(
length
l
/
2
).
Compute
split
[
1
;
2
;
3
;
4
;
5
].
(
*
Second
a
solution
that
just
alternates
*
)
Fixpoint
split
'
{
A
}
(
l
:
list
A
)
:=
match
l
with
|
[]
=>
([],
[])
|
x
::
q
=>
let
(
l1
,
l2
)
:=
split
'
q
in
(
x
::
l2
,
l1
)
end
.
Compute
split
'
[
1
;
2
;
3
;
4
;
5
].
(
*
Merge
:
*
)
Fixpoint
merge
(
l
:
list
nat
)
:
list
nat
->
list
nat
:=
match
l
with
|
[]
=>
fun
s
=>
s
|
a
::
l
'
=>
fix
merge_l
s
:=
match
s
with
|
[]
=>
l
|
b
::
s
'
=>
if
a
<?
b
then
a
::
(
merge
l
'
s
)
else
b
::
merge_l
s
'
end
end
.
Compute
merge
[
1
;
3
;
4
;
5
]
[
2
;
3
;
5
;
7
].
(
*
Mergesort
*
)
Fixpoint
mergesort_counter
l
n
:=
match
n
with
|
O
=>
l
|
S
n
=>
match
l
with
|
[]
=>
[]
(
*
be
careful
not
to
forget
"little"
cases
,
otherwise
you
may
"loop"
(
or
rather
exhaust
the
counter
n
)
*
)
|
[
x
]
=>
[
x
]
|
_
=>
let
(
l1
,
l2
)
:=
split
'
l
in
merge
(
mergesort_counter
l1
n
)
(
mergesort_counter
l2
n
)
end
end
.
Definition
mergesort
l
:=
mergesort_counter
l
(
length
l
).
Compute
mergesort
[
1
;
7
;
2
;
3
;
10
;
0
;
3
].
(
**
Exercise
4
:
Powerset
*
)
Fixpoint
powerset
{
A
}
(
l
:
list
A
)
:
list
(
list
A
)
:=
match
l
with
|
[]
=>
[[]]
|
x
::
q
=>
let
ll
:=
powerset
q
in
ll
++
(
map
(
fun
l
=>
x
::
l
)
ll
)
(
*
or
:
map
(
cons
x
)
ll
*
)
end
.
Compute
powerset
[
1
;
2
;
3
].
td3-english.md
View file @
157fd6a8
...
...
@@ -15,7 +15,7 @@ Import ListNotations.
Program the following functions, without using the corresponding functions from the Coq standard library :
-
`length`
-
concatenate (
`app`
in Coq, infix
e
notation
`++`
)
-
concatenate (
`app`
in Coq, infix notation
`++`
)
-
`rev`
(for reverse, a.k.a mirror)
-
`map : forall {A B}, (A->B)-> list A -> list B`
-
`filter : forall {A}, (A->bool) -> list A -> list A`
...
...
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