Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
David Swasey
coq-stdpp
Commits
af633db2
Commit
af633db2
authored
Jun 06, 2014
by
Robbert Krebbers
Browse files
Small stream library.
parent
ab930b45
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/streams.v
0 → 100644
View file @
af633db2
(* Copyright (c) 2012-2014, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require
Export
tactics
.
CoInductive
stream
(
A
:
Type
)
:
Type
:
=
scons
:
A
→
stream
A
→
stream
A
.
Arguments
scons
{
_
}
_
_
.
Delimit
Scope
stream_scope
with
stream
.
Bind
Scope
stream_scope
with
stream
.
Open
Scope
stream_scope
.
Infix
":.:"
:
=
scons
(
at
level
60
,
right
associativity
)
:
stream_scope
.
Definition
shead
{
A
}
(
s
:
stream
A
)
:
A
:
=
match
s
with
x
:
.
:
_
=>
x
end
.
Definition
stail
{
A
}
(
s
:
stream
A
)
:
stream
A
:
=
match
s
with
_
:
.
:
s
=>
s
end
.
CoInductive
stream_equiv'
{
A
}
(
s1
s2
:
stream
A
)
:
Prop
:
=
scons_equiv'
:
shead
s1
=
shead
s2
→
stream_equiv'
(
stail
s1
)
(
stail
s2
)
→
stream_equiv'
s1
s2
.
Instance
stream_equiv
{
A
}
:
Equiv
(
stream
A
)
:
=
stream_equiv'
.
Reserved
Infix
"!.!"
(
at
level
20
).
Fixpoint
slookup
{
A
}
(
i
:
nat
)
(
s
:
stream
A
)
:
A
:
=
match
i
with
O
=>
shead
s
|
S
i
=>
stail
s
!.!
i
end
where
"s !.! i"
:
=
(
slookup
i
s
).
Section
stream_properties
.
Context
{
A
:
Type
}.
Implicit
Types
x
y
:
A
.
Implicit
Types
s
t
:
stream
A
.
Lemma
scons_equiv
s1
s2
:
shead
s1
=
shead
s2
→
stail
s1
≡
stail
s2
→
s1
≡
s2
.
Proof
.
by
constructor
.
Qed
.
Global
Instance
equal_equivalence
:
Equivalence
(@
equiv
(
stream
A
)
_
).
Proof
.
split
.
*
now
cofix
;
intros
[??]
;
constructor
.
*
now
cofix
;
intros
??
[??]
;
constructor
.
*
cofix
;
intros
???
[??]
[??]
;
constructor
;
etransitivity
;
eauto
.
Qed
.
Global
Instance
scons_proper
x
:
Proper
((
≡
)
==>
(
≡
))
(
scons
x
).
Proof
.
by
constructor
.
Qed
.
Global
Instance
shead_proper
:
Proper
((
≡
)
==>
(=))
(@
shead
A
).
Proof
.
by
intros
??
[??].
Qed
.
Global
Instance
stail_proper
:
Proper
((
≡
)
==>
(
≡
))
(@
stail
A
).
Proof
.
by
intros
??
[??].
Qed
.
Global
Instance
slookup_proper
:
Proper
((
≡
)
==>
eq
)
(@
slookup
A
i
).
Proof
.
by
induction
i
as
[|
i
IH
]
;
intros
s1
s2
Hs
;
simpl
;
rewrite
Hs
.
Qed
.
End
stream_properties
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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