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
proglmfi
Commits
f6f06d74
Commit
f6f06d74
authored
Dec 02, 2020
by
Pierre Letouzey
Browse files
some solutions for TD5
parent
445c32ce
Changes
1
Hide whitespace changes
Inline
Sidebyside
solutions/td5.v
0 → 100644
View file @
f6f06d74
(
*
TD5
*
)
Require
Import
Arith
List
Bool
NArith
.
Import
ListNotations
.
Set
Implicit
Arguments
.
(
*
Exercise
1
:
Exercise
2
of
TD4
,
this
time
with
dependent
types
expressing
that
trees
are
necessarily
perfect
*
)
Module
BList_DepType
.
(
*
See
seance5

english
.
v
for
explanations
*
)
Inductive
fulltree
(
A
:
Type
)
:
nat
>
Type
:=

FLeaf
:
A
>
fulltree
A
0

FNode
n
:
fulltree
A
n
>
fulltree
A
n
>
fulltree
A
(
S
n
).
Arguments
FLeaf
{
A
}
.
Arguments
FNode
{
A
}
{
n
}
.
Definition
blist
(
A
:
Type
)
:=
list
{
n
&
fulltree
A
n
}
.
Definition
empty_blist
{
A
}
:
blist
A
:=
[].
Definition
size1_blist
{
A
}
(
a
:
A
)
:
blist
A
:=
[
existT
_
_
(
FLeaf
a
)].
Definition
size2_blist
{
A
}
(
a
b
:
A
)
:
blist
A
:=
[
existT
_
_
(
FNode
(
FLeaf
a
)
(
FLeaf
b
))].
(
*
A
comparison
returning
(
dis
)
equality
proofs
in
addition
to
the
yes
/
no
answer
*
)
Check
Nat
.
eq_dec
.
(
*
For
instance
:
match
Nat
.
eq_dec
n
m
with

left
p
=>
(
*
here
(
p
:
n
=
m
)
*
)
...

right
_
=>
(
*
here
n
<>
m
*
)
...
end
*
)
(
*
Just
like
Vcast
(
see
seance
4
)
*
)
Definition
treecast
{
A
}
{
n
}
{
m
}
(
v
:
fulltree
A
n
)(
h
:
n
=
m
)
:
fulltree
A
m
:=
match
h
with

eq_refl
=>
v
end
.
(
*
Important
auxiliary
function
:
putting
a
tree
on
the
left
of
a
bl
.
*
)
(
*
invariant
:
depth
t
<=
depth
of
leftmost
tree
in
the
bl
*
)
Fixpoint
constree
{
A
}
{
n
:
nat
}
(
t
:
fulltree
A
n
)
(
bl
:
blist
A
)
:
blist
A
:=
match
bl
with

[]
=>
[
existT
_
n
t
]

(
existT
_
m
t
'
)
::
bl
'
=>
match
Nat
.
eq_dec
n
m
with

left
p
=>
constree
(
FNode
(
treecast
t
p
)
t
'
)
bl
'

right
_
=>
(
existT
_
n
t
)
::
bl
end
end
.
Definition
cons
{
A
}
(
a
:
A
)
bl
:=
constree
(
FLeaf
a
)
bl
.
Compute
cons
2
(
cons
3
(
size2_blist
5
7
)).
(
*
Unlike
with
Vcast
in
seance
4
,
this
computes
ok
since
Nat
.
eq_dec
returns
a
proof
that
isn
'
t
opaque
...
*
)
(
*
digression
:
from
regular
list
to
blist
and
back
*
)
Fixpoint
list_to_blist
{
A
}
(
l
:
list
A
)
:
blist
A
:=
match
l
with

[]
=>
empty_blist

x
::
l
=>
cons
x
(
list_to_blist
l
)
end
.
Compute
list_to_blist
[
1
;
2
;
3
;
4
;
5
;
6
;
7
].
Fixpoint
tree_to_list
{
A
}
{
n
}
(
t
:
fulltree
A
n
)
:
list
A
:=
match
t
with

FLeaf
a
=>
[
a
]

FNode
t
t
'
=>
tree_to_list
t
++
tree_to_list
t
'
end
.
Fixpoint
blist_to_list
{
A
}
(
bl
:
blist
A
)
:=
match
bl
with

[]
=>
[]

(
existT
_
_
t
)
::
bl
=>
tree_to_list
t
++
blist_to_list
bl
end
.
(
*
end
of
digression
*
)
(
*
depth
t
<
depth
of
every
tree
in
acc
*
)
Fixpoint
unconstree
{
A
}
{
n
}
(
t
:
fulltree
A
n
)
(
acc
:
blist
A
)
:
A
*
blist
A
:=
match
t
with

FLeaf
a
=>
(
a
,
acc
)

FNode
t
t
'
=>
unconstree
t
((
existT
_
_
t
'
)
::
acc
)
end
.
Definition
uncons
{
A
}
(
bl
:
blist
A
)
:
option
(
A
*
blist
A
)
:=
match
bl
with

[]
=>
None

(
existT
_
_
t
)
::
bl
=>
Some
(
unconstree
t
bl
)
end
.
(
*
O
(
lg
(
n
))
*
)
(
*
invariant
:
n
<
size
t
(
which
is
2
^
depth
t
)
*
)
Fixpoint
nthtree
{
A
}
{
d
}
(
t
:
fulltree
A
d
)
n
:
option
A
:=
match
t
with

FLeaf
a
=>
Some
a
(
*
normally
here
n
must
be
0
*
)

FNode
t1
t2
=>
let
size_t1
:=
2
^
(
pred
d
)
in
if
n
<?
size_t1
then
nthtree
t1
n
else
nthtree
t2
(
n

size_t1
)
end
.
Fixpoint
nth
{
A
}
(
bl
:
blist
A
)
n
:
option
A
:=
match
bl
with

[]
=>
None

(
existT
_
d
t
)
::
bl
'
=>
let
size_t
:=
2
^
d
in
if
n
<?
size_t
then
nthtree
t
n
else
nth
bl
'
(
n

size_t
)
end
.
(
*
O
(
lg
(
n
))
*
)
Compute
nth
(
list_to_blist
[
1
;
2
;
3
;
4
;
5
;
6
;
7
])
6.
End
BList_DepType
.
(
*
Exercise
2
:
perfect_depth
via
error
monad
*
)
Inductive
tree
A
:=

leaf
:
A
>
tree
A

node
:
tree
A
>
tree
A
>
tree
A
.
Definition
option_bind
{
A
B
}
(
o
:
option
A
)
(
f
:
A
>
option
B
)
:
option
B
:=
match
o
with

Some
x
=>
f
x

None
=>
None
end
.
Infix
">>="
:=
option_bind
(
at
level
20
,
left
associativity
).
Fixpoint
perfect_depth
{
A
}
(
t
:
tree
A
)
:
option
nat
:=
match
t
with

leaf
_
=>
Some
0

node
g
d
=>
perfect_depth
g
>>=
fun
dg
=>
perfect_depth
d
>>=
fun
dd
=>
if
dg
=?
dd
then
Some
(
S
dg
)
else
None
end
.
(
*
Exercise
3
*
)
(
*
first
attempt
,
with
List
.
flat_map
,
and
hence
no
elimination
of
redundant
results
.
*
)
Definition
listbind
{
A
B
}
(
l
:
list
A
)
(
f
:
A
>
list
B
)
:=
List
.
flat_map
f
l
.
Print
flat_map
.
Infix
">>="
:=
listbind
(
at
level
20
,
left
associativity
).
Definition
next_score
n
:=
[
n
+
3
;
n
+
5
;
n
+
7
].
Fixpoint
next_scores
k
l
:=
match
k
with

O
=>
l

S
k
'
=>
next_scores
k
'
l
>>=
next_score
end
.
Compute
next_scores
5
[
0
].
(
*
Looots
of
redundancies
*
)
(
*
Compute
next_scores
10
[
0
]
(
*
Stack
overflow
during
display
...
*
)
*
)
Compute
let
l
:=
next_scores
10
[
0
]
in
N
.
of_nat
(
length
l
).
(
*
59049
elements
!
*
)
(
*
Better
,
without
redundancies
(
but
just
for
list
nat
)
*
)
Fixpoint
listmerge
l1
l2
(
*
for
strictly
sorted
lists
of
numbers
*
)
:=
match
l1
with

[]
=>
l2

x1
::
l1
'
=>
(
fix
listmerge_l1
l2
:=
match
l2
with

[]
=>
l1

x2
::
l2
'
=>
match
Nat
.
compare
x1
x2
with

Lt
=>
x1
::
listmerge
l1
'
l2

Eq
=>
x1
::
listmerge
l1
'
l2
'

Gt
=>
x2
::
listmerge_l1
l2
'
end
end
)
l2
end
.
Compute
listmerge
[
1
;
2
;
4
]
[
2
;
3
;
5
].
(
*
Same
as
flat_map
,
but
here
all
lists
are
supposed
to
be
strictly
sorted
,
and
we
merge
them
instead
of
++
*
)
Fixpoint
listbind2
(
l
:
list
nat
)
(
f
:
nat
>
list
nat
)
:=
match
l
with

[]
=>
[]

a
::
l
'
=>
listmerge
(
f
a
)
(
listbind2
l
'
f
)
end
.
Infix
">>="
:=
listbind2
(
at
level
20
,
left
associativity
).
Fixpoint
next_scores_v2
k
l
:=
match
k
with

O
=>
l

S
k
'
=>
next_scores_v2
k
'
l
>>=
next_score
end
.
Compute
next_scores_v2
10
[
0
].
(
*
[
30
;
32
;
34
;
36
;
38
;
40
;
42
;
44
;
46
;
48
;
50
;
52
;
54
;
56
;
58
;
60
;
62
;
64
;
66
;
68
;
70
]
*
)
Compute
length
(
next_scores_v2
10
[
0
]).
(
*
21
unique
answers
instead
of
59049
!
*
)
(
*
End
of
3.1
:
what
about
scoring
at
most
10
times
?
We
just
keep
the
current
score
a
in
addition
to
[
next_score
a
]
*
)
Fixpoint
next_scores_large
k
l
:=
match
k
with

O
=>
l

S
k
'
=>
next_scores_large
k
'
l
>>=
fun
a
=>
a
::
next_score
a
end
.
Compute
next_scores_large
10
[
0
].
(
*
[
0
;
3
;
5
;
6
;
7
;
8
;
9
;
10
;
11
;
12
;
13
;
14
;
15
;
16
;
17
;
18
;
19
;
20
;
21
;
22
;
23
;
24
;
25
;
26
;
27
;
28
;
29
;
30
;
31
;
32
;
33
;
34
;
35
;
36
;
37
;
38
;
39
;
40
;
41
;
42
;
43
;
44
;
45
;
46
;
47
;
48
;
49
;
50
;
51
;
52
;
53
;
54
;
55
;
56
;
57
;
58
;
59
;
60
;
61
;
62
;
63
;
64
;
66
;
68
;
70
]
*
)
(
*
Exercise
3.2
*
)
(
*
Back
to
unsorted
list
bind
(
since
listbind2
was
only
for
list
nat
)
*
)
Infix
">>="
:=
listbind
(
at
level
20
,
left
associativity
).
Compute
List
.
seq
1
100.
(
*
1
to
100
*
)
(
*
A
first
naive
attemp
,
generating
all
combinations
for
a
,
b
and
c
*
)
Definition
pytha
n
:=
let
nums
:=
List
.
seq
1
n
in
nums
>>=
fun
a
=>
nums
>>=
fun
b
=>
nums
>>=
fun
c
=>
if
a
*
a
+
b
*
b
=?
c
*
c
then
[(
a
,
b
,
c
)]
else
[].
(
*
Quite
slow
...
*
)
Time
Compute
pytha
40.
(
*
4
sec
,
then
11
s
here
for
50
,
then
+
∞
for
100
*
)
(
*
Three
possible
improvements
:

Deduce
c
from
a
and
b
,
thanks
to
Nat
.
sqrt
(
but
be
careful
to
check
whether
c
is
<=
n
in
this
case
)

Consider
only
b
for
which
a
<
b

As
usual
,
switch
to
N
instead
of
nat
will
greatly
speed
up
all
arithmetical
computations
.
Moreover
,
a
function
N
.
sqrtrem
directly
give
use
the
remainder
left
after
computing
the
rounded
square
root
.
*
)
Definition
pytha_opt
n
:=
(
List
.
seq
1
n
)
>>=
fun
a
=>
(
List
.
seq
(
a
+
1
)
(
n

a
))
>>=
fun
b
=>
let
c
:=
Nat
.
sqrt
(
a
*
a
+
b
*
b
)
in
if
(
c
<=?
n
)
&&
(
a
*
a
+
b
*
b
=?
c
*
c
)
then
[(
a
,
b
,
c
)]
else
[].
Compute
pytha_opt
100.
(
*
3
s
,
even
with
nat
*
)
Fixpoint
seqN
a
n
:=
match
n
with

0
=>
[]

S
n
=>
a
::
(
seqN
(
N
.
succ
a
)
n
)
end
.
Definition
pythaN
n
:=
(
seqN
1
%
N
n
)
>>=
fun
a
=>
(
seqN
(
a
+
1
)
%
N
(
n

N
.
to_nat
a
))
>>=
fun
b
=>
let
(
c
,
rem
)
:=
N
.
sqrtrem
(
a
*
a
+
b
*
b
)
in
if
(
rem
=?
0
)
%
N
&&
(
c
<=?
N
.
of_nat
n
)
%
N
then
[(
a
,
b
,
c
)]
else
[].
Compute
pythaN
100.
(
*
0
s
*
)
(
**
Exercise
3.3
*
)
Definition
closeby
n
m
:=
(
n
=?
S
m
)

(
S
n
=?
m
).
(
*
A
not

so

nice
solution
.
Any
better
proposal
?
*
)
Definition
L_R_B_P
:=
let
positions
:=
[
1
;
2
;
3
;
4
]
in
positions
>>=
fun
L
=>
positions
>>=
fun
R
=>
if
negb
(
closeby
L
R
)
then
[]
else
positions
>>=
fun
B
=>
if
(
B
=?
R
)

(
B
=?
L
)
then
[]
else
positions
>>=
fun
P
=>
if
(
closeby
P
L
)
&&
(
negb
(
P
=?
R
))
&&
(
negb
(
P
=?
B
))
then
[(
L
,
R
,
B
,
P
)]
else
[].
Compute
L_R_B_P
.
(
*
4
solutions
*
)
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