Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Simon Spies
stdpp
Commits
36f903b6
Commit
36f903b6
authored
Jun 21, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
More hlist stuff.
parent
46db392a
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
38 additions
and
7 deletions
+38
7
theories/hlist.v
theories/hlist.v
+38
7
No files found.
theories/hlist.v
View file @
36f903b6
From
stdpp
Require
Import
base
.
From
stdpp
Require
Import
tactics
.
(* Not using [list Type] in order to avoid universe inconsistencies *)
Inductive
tlist
:
=
tnil
:
tlist

tcons
:
Type
→
tlist
→
tlist
.
...
...
@@ 7,22 +7,53 @@ Inductive hlist : tlist → Type :=

hnil
:
hlist
tnil

hcons
{
A
As
}
:
A
→
hlist
As
→
hlist
(
tcons
A
As
).
Fixpoint
tapp
(
As
Bs
:
tlist
)
:
tlist
:
=
match
As
with
tnil
=>
Bs

tcons
A
As
=>
tcons
A
(
tapp
As
Bs
)
end
.
Fixpoint
happ
{
As
Bs
}
(
xs
:
hlist
As
)
(
ys
:
hlist
Bs
)
:
hlist
(
tapp
As
Bs
)
:
=
match
xs
with
hnil
=>
ys

hcons
_
_
x
xs
=>
hcons
x
(
happ
xs
ys
)
end
.
Fixpoint
hhead
{
A
As
}
(
xs
:
hlist
(
tcons
A
As
))
:
A
:
=
match
xs
with
hnil
=>
()

hcons
_
_
x
_
=>
x
end
.
Fixpoint
htail
{
A
As
}
(
xs
:
hlist
(
tcons
A
As
))
:
hlist
As
:
=
match
xs
with
hnil
=>
()

hcons
_
_
_
xs
=>
xs
end
.
Fixpoint
hheads
{
As
Bs
}
:
hlist
(
tapp
As
Bs
)
→
hlist
As
:
=
match
As
with

tnil
=>
λ
_
,
hnil

tcons
A
As
=>
λ
xs
,
hcons
(
hhead
xs
)
(
hheads
(
htail
xs
))
end
.
Fixpoint
htails
{
As
Bs
}
:
hlist
(
tapp
As
Bs
)
→
hlist
Bs
:
=
match
As
with

tnil
=>
id

tcons
A
As
=>
λ
xs
,
htails
(
htail
xs
)
end
.
Fixpoint
himpl
(
As
:
tlist
)
(
B
:
Type
)
:
Type
:
=
match
As
with
tnil
=>
B

tcons
A
As
=>
A
→
himpl
As
B
end
.
Definition
happly
{
As
B
}
(
f
:
himpl
As
B
)
(
xs
:
hlist
As
)
:
B
:
=
Definition
hinit
{
B
}
(
y
:
B
)
:
himpl
tnil
B
:
=
y
.
Definition
hlam
{
A
As
B
}
(
f
:
A
→
himpl
As
B
)
:
himpl
(
tcons
A
As
)
B
:
=
f
.
Arguments
hlam
_
_
_
_
_
/.
Definition
hcurry
{
As
B
}
(
f
:
himpl
As
B
)
(
xs
:
hlist
As
)
:
B
:
=
(
fix
go
As
xs
:
=
match
xs
in
hlist
As
return
himpl
As
B
→
B
with

hnil
=>
λ
f
,
f

hcons
A
As
x
xs
=>
λ
f
,
go
As
xs
(
f
x
)
end
)
_
xs
f
.
Coercion
happly
:
himpl
>>
Funclass
.
Coercion
hcurry
:
himpl
>>
Funclass
.
Fixpoint
huncurry
{
As
B
}
:
(
hlist
As
→
B
)
→
himpl
As
B
:
=
match
As
with

tnil
=>
λ
f
,
f
hnil

tcons
x
xs
=>
λ
f
,
hlam
(
λ
x
,
huncurry
(
f
∘
hcons
x
))
end
.
Lemma
hcurry_uncurry
{
As
B
}
(
f
:
hlist
As
→
B
)
xs
:
huncurry
f
xs
=
f
xs
.
Proof
.
by
induction
xs
as
[
A
As
x
xs
IH
]
;
simpl
;
rewrite
?IH
.
Qed
.
Fixpoint
hcompose
{
As
B
C
}
(
f
:
B
→
C
)
{
struct
As
}
:
himpl
As
B
→
himpl
As
C
:
=
match
As
with

tnil
=>
f

tcons
A
As
=>
λ
g
x
,
hcompose
f
(
g
x
)

tcons
A
As
=>
λ
g
,
hlam
(
λ
x
,
hcompose
f
(
g
x
)
)
end
.
Definition
hinit
{
B
}
(
y
:
B
)
:
himpl
tnil
B
:
=
y
.
Definition
hlam
{
A
As
B
}
(
f
:
A
→
himpl
As
B
)
:
himpl
(
tcons
A
As
)
B
:
=
f
.
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