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
6c1e3579
Commit
6c1e3579
authored
Nov 25, 2020
by
Pierre Letouzey
Browse files
partial solution for TD4 (just exo 1 and 2)
parent
8a216021
Changes
1
Hide whitespace changes
Inline
Side-by-side
solutions/td4.v
0 → 100644
View file @
6c1e3579
(
*
TD4
:
solutions
for
exercises
1
and
2
*
)
Require
Import
Arith
List
.
Import
ListNotations
.
Set
Implicit
Arguments
.
(
*
Exercise
1
*
)
Module
RegularList
.
Print
List
.
(
*
our
cons
here
is
just
a
wrapper
around
Coq
'
s
cons
*
)
Definition
cons
:
forall
{
A
}
,
A
->
list
A
->
list
A
:=
fun
{
A
}
a
l
=>
List
.
cons
a
l
.
(
*
or
fun
{
A
}
a
m
=>
a
::
l
*
)
(
*
or
just
directly
@
List
.
cons
.
*
)
(
*
complexity
:
O
(
1
)
*
)
Definition
uncons
:
forall
{
A
}
,
list
A
->
option
(
A
*
list
A
)
:=
fun
{
A
}
l
=>
match
l
with
|
[]
=>
None
|
x
::
l
=>
Some
(
x
,
l
)
end
.
(
*
complexity
:
O
(
1
)
*
)
Definition
nth
:
forall
{
A
}
,
list
A
->
nat
->
option
A
:=
List
.
nth_error
.
(
*
worst
complexity
:
O
(
n
)
where
n
is
the
size
of
the
list
*
)
End
RegularList
.
(
*
Exercise
2
*
)
Module
BList
.
Inductive
tree
A
:=
|
leaf
:
A
->
tree
A
|
node
:
tree
A
->
tree
A
->
tree
A
.
Check
node
(
leaf
1
)
(
leaf
2
).
Check
node
(
node
(
leaf
1
)
(
leaf
2
))
(
leaf
3
).
(
*
Some
unbalanced
tree
we
want
to
avoid
*
)
Fixpoint
depth
{
A
}
(
t
:
tree
A
)
:=
(
*
optimistic
depth
,
supposing
the
tree
to
be
perfect
*
)
match
t
with
|
leaf
_
=>
0
|
node
t
'
_
=>
S
(
depth
t
'
)
end
.
Definition
blist
(
A
:
Type
)
:
Type
:=
list
(
tree
A
).
(
*
or
later
a
version
with
the
size
or
depth
of
tree
coming
along
each
trees
,
to
avoid
recomputing
this
information
all
the
time
.
*
)
Definition
empty_blist
{
A
}
:
blist
A
:=
[].
Definition
size1_blist
{
A
}
(
a
:
A
)
:
blist
A
:=
[
leaf
a
].
Definition
size2_blist
{
A
}
(
a
b
:
A
)
:
blist
A
:=
[
node
(
leaf
a
)
(
leaf
b
)].
(
*
etc
.
The
size
of
the
trees
are
the
binary
decomposition
of
the
total
number
of
elements
in
the
blist
.
Eg
.
7
=
1
+
2
+
4
*
)
(
*
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
}
(
t
:
tree
A
)
(
bl
:
blist
A
)
:
blist
A
:=
match
bl
with
|
[]
=>
[
t
]
|
t
'
::
bl
'
=>
if
depth
t
=?
depth
t
'
then
constree
(
node
t
t
'
)
bl
'
else
t
::
bl
end
.
Definition
cons
{
A
}
(
a
:
A
)
bl
:=
constree
(
leaf
a
)
bl
.
Compute
cons
2
(
cons
3
(
size2_blist
5
7
)).
(
*
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
}
(
t
:
tree
A
)
:
list
A
:=
match
t
with
|
leaf
a
=>
[
a
]
|
node
t
t
'
=>
tree_to_list
t
++
tree_to_list
t
'
end
.
Fixpoint
blist_to_list
{
A
}
(
bl
:
blist
A
)
:=
match
bl
with
|
[]
=>
[]
|
t
::
bl
=>
tree_to_list
t
++
blist_to_list
bl
end
.
(
*
end
of
digression
*
)
(
*
depth
t
<
depth
of
ervery
tree
in
acc
*
)
Fixpoint
unconstree
{
A
}
(
t
:
tree
A
)
(
acc
:
blist
A
)
:
A
*
blist
A
:=
match
t
with
|
leaf
a
=>
(
a
,
acc
)
|
node
t
t
'
=>
unconstree
t
(
t
'
::
acc
)
end
.
Definition
uncons
{
A
}
(
bl
:
blist
A
)
:
option
(
A
*
blist
A
)
:=
match
bl
with
|
[]
=>
None
|
t
::
bl
=>
Some
(
unconstree
t
bl
)
end
.
(
*
O
(
lg
(
n
))
*
)
Check
Nat
.
log2
.
Compute
(
2
^
4
).
Compute
Nat
.
log2
16.
(
*
invariant
:
n
<
size
t
(
which
is
2
^
depth
t
)
*
)
Fixpoint
nthtree
{
A
}
(
t
:
tree
A
)
n
:
option
A
:=
match
t
with
|
leaf
a
=>
Some
a
(
*
normally
here
n
must
be
0
*
)
|
node
t1
t2
=>
let
size_t1
:=
2
^
depth
t1
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
|
t
::
bl
'
=>
let
size_t
:=
2
^
depth
t
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
.
Module
BListWithSize
.
Import
BList
.
(
*
for
BList
.
tree
*
)
Definition
blist
(
A
:
Type
)
:
Type
:=
list
(
nat
*
tree
A
).
(
*
nat
is
here
the
size
of
the
tree
along
it
.
Could
be
the
size
if
you
prefer
.
*
)
(
*
Let
'
s
adapt
all
the
previous
code
to
avoid
recomputing
any
depth
*
)
(
*
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
}
(
t
:
tree
A
)
(
depth
:
nat
)
(
bl
:
blist
A
)
:
blist
A
:=
match
bl
with
|
[]
=>
[(
depth
,
t
)]
|
(
depth
'
,
t
'
)
::
bl
'
=>
if
depth
=?
depth
'
then
constree
(
node
t
t
'
)
(
S
depth
)
bl
'
else
(
depth
,
t
)
::
bl
end
.
Definition
cons
{
A
}
(
a
:
A
)
bl
:=
constree
(
leaf
a
)
0
bl
.
Compute
cons
2
(
cons
3
(
cons
5
(
cons
7
[]))).
(
*
digression
:
from
regular
list
to
blist
and
back
*
)
Fixpoint
list_to_blist
{
A
}
(
l
:
list
A
)
:
blist
A
:=
match
l
with
|
[]
=>
[]
|
x
::
l
=>
cons
x
(
list_to_blist
l
)
end
.
Compute
list_to_blist
[
1
;
2
;
3
;
4
;
5
;
6
;
7
].
Fixpoint
blist_to_list
{
A
}
(
bl
:
blist
A
)
:=
match
bl
with
|
[]
=>
[]
|
(
_
,
t
)
::
bl
=>
tree_to_list
t
++
blist_to_list
bl
end
.
(
*
end
of
digression
*
)
(
*
depth
t
<
depth
of
ervery
tree
in
acc
*
)
Fixpoint
unconstree
{
A
}
(
t
:
tree
A
)
depth
(
acc
:
blist
A
)
:
A
*
blist
A
:=
match
t
with
|
leaf
a
=>
(
a
,
acc
)
|
node
t
t
'
=>
let
depth
'
:=
depth
-
1
in
unconstree
t
depth
'
((
depth
'
,
t
'
)
::
acc
)
end
.
Definition
uncons
{
A
}
(
bl
:
blist
A
)
:
option
(
A
*
blist
A
)
:=
match
bl
with
|
[]
=>
None
|
(
depth
,
t
)
::
bl
=>
Some
(
unconstree
t
depth
bl
)
end
.
(
*
O
(
lg
(
n
))
*
)
(
*
invariant
:
n
<
size
(
which
is
2
^
depth
t
)
*
)
Fixpoint
nthtree
{
A
}
(
t
:
tree
A
)
n
size
:
option
A
:=
match
t
with
|
leaf
a
=>
Some
a
(
*
normally
here
n
must
be
0
*
)
|
node
t1
t2
=>
let
size
'
:=
Nat
.
div2
size
in
if
n
<?
size
'
then
nthtree
t1
n
size
'
else
nthtree
t2
(
n
-
size
'
)
size
'
end
.
Fixpoint
nth
{
A
}
(
bl
:
blist
A
)
n
:
option
A
:=
match
bl
with
|
[]
=>
None
|
(
depth
,
t
)
::
bl
'
=>
let
size_t
:=
2
^
depth
in
if
n
<?
size_t
then
nthtree
t
n
size_t
else
nth
bl
'
(
n
-
size_t
)
end
.
(
*
O
(
lg
(
n
))
*
)
Compute
nth
(
list_to_blist
[
1
;
2
;
3
;
4
;
5
;
6
;
7
])
6.
End
BListWithSize
.
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