Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Contribute to GitLab
Sign in
Toggle navigation
C
cpdt
Project
Project
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
research
cpdt
Commits
a0c1af6f
Commit
a0c1af6f
authored
Mar 28, 2012
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
One more example of avoiding axioms (getNat)
parent
e0fa0633
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
152 additions
and
2 deletions
+152
-2
Universes.v
src/Universes.v
+152
-2
No files found.
src/Universes.v
View file @
a0c1af6f
(
*
Copyright
(
c
)
2009
-
201
1
,
Adam
Chlipala
(
*
Copyright
(
c
)
2009
-
201
2
,
Adam
Chlipala
*
*
*
This
work
is
licensed
under
a
*
This
work
is
licensed
under
a
*
Creative
Commons
Attribution
-
Noncommercial
-
No
Derivative
Works
3.0
*
Creative
Commons
Attribution
-
Noncommercial
-
No
Derivative
Works
3.0
...
@@ -8,6 +8,8 @@
...
@@ -8,6 +8,8 @@
*
)
*
)
(
*
begin
hide
*
)
(
*
begin
hide
*
)
Require
Import
List
.
Require
Import
DepList
CpdtTactics
.
Require
Import
DepList
CpdtTactics
.
Set
Implicit
Arguments
.
Set
Implicit
Arguments
.
...
@@ -1016,4 +1018,152 @@ Print Assumptions proj1_again.
...
@@ -1016,4 +1018,152 @@ Print Assumptions proj1_again.
Closed
under
the
global
context
Closed
under
the
global
context
>>
>>
This
example
illustrates
again
how
some
of
the
same
design
patterns
we
learned
for
dependently
typed
programming
can
be
used
fruitfully
in
theorem
statements
.
*
)
This
example
illustrates
again
how
some
of
the
same
design
patterns
we
learned
for
dependently
typed
programming
can
be
used
fruitfully
in
theorem
statements
.
%
\
medskip
%
To
close
the
chapter
,
we
consider
one
final
way
to
avoid
dependence
on
axioms
.
Often
this
task
is
equivalent
to
writing
definitions
such
that
they
%
\
emph
{%
#
<
i
>
#
compute
#
</
i
>
#
%}%.
That
is
,
we
want
Coq
'
s
normal
reduction
to
be
able
to
run
certain
programs
to
completion
.
Here
is
a
simple
example
where
such
computation
can
get
stuck
.
In
proving
properties
of
such
functions
,
we
would
need
to
apply
axioms
like
%
\
index
{
axiom
K
}%
K
manually
to
make
progress
.
Imagine
we
are
working
with
%
\
index
{
deep
embedding
}%
deeply
embedded
syntax
of
some
programming
language
,
where
each
term
is
considered
to
be
in
the
scope
of
a
number
of
free
variables
that
hold
normal
Coq
values
.
To
enforce
proper
typing
,
we
will
need
to
model
a
Coq
typing
environment
somehow
.
One
natural
choice
is
as
a
list
of
types
,
where
variable
number
[
i
]
will
be
treated
as
a
reference
to
the
[
i
]
th
element
of
the
list
.
*
)
Section
withTypes
.
Variable
types
:
list
Set
.
(
**
To
give
the
semantics
of
terms
,
we
will
need
to
represent
value
environments
,
which
assign
each
variable
a
term
of
the
proper
type
.
*
)
Variable
values
:
hlist
(
fun
x
:
Set
=>
x
)
types
.
(
**
Now
imagine
that
we
are
writing
some
procedure
that
operates
on
a
distinguished
variable
of
type
[
nat
]
.
A
hypothesis
formalizes
this
assumption
,
using
the
standard
library
function
[
nth_error
]
for
looking
up
list
elements
by
position
.
*
)
Variable
natIndex
:
nat
.
Variable
natIndex_ok
:
nth_error
types
natIndex
=
Some
nat
.
(
**
It
is
not
hard
to
use
this
hypothesis
to
write
a
function
for
extracting
the
[
nat
]
value
in
position
[
natIndex
]
of
[
values
]
,
starting
with
two
helpful
lemmas
,
each
of
which
we
finish
with
[
Defined
]
to
mark
the
lemma
as
transparent
,
so
that
its
definition
may
be
expanded
during
evaluation
.
*
)
Lemma
nth_error_nil
:
forall
A
n
x
,
nth_error
(
@
nil
A
)
n
=
Some
x
->
False
.
destruct
n
;
simpl
;
unfold
error
;
congruence
.
Defined
.
Implicit
Arguments
nth_error_nil
[
A
n
x
]
.
Lemma
Some_inj
:
forall
A
(
x
y
:
A
)
,
Some
x
=
Some
y
->
x
=
y
.
congruence
.
Defined
.
Fixpoint
getNat
(
types
'
:
list
Set
)
(
values
'
:
hlist
(
fun
x
:
Set
=>
x
)
types
'
)
(
natIndex
:
nat
)
:
(
nth_error
types
'
natIndex
=
Some
nat
)
->
nat
:=
match
values
'
with
|
HNil
=>
fun
pf
=>
match
nth_error_nil
pf
with
end
|
HCons
t
ts
x
values
''
=>
match
natIndex
return
nth_error
(
t
::
ts
)
natIndex
=
Some
nat
->
nat
with
|
O
=>
fun
pf
=>
match
Some_inj
pf
in
_
=
T
return
T
with
|
refl_equal
=>
x
end
|
S
natIndex
'
=>
getNat
values
''
natIndex
'
end
end
.
End
withTypes
.
(
**
The
problem
becomes
apparent
when
we
experiment
with
running
[
getNat
]
on
a
concrete
[
types
]
list
.
*
)
Definition
myTypes
:=
unit
::
nat
::
bool
::
nil
.
Definition
myValues
:
hlist
(
fun
x
:
Set
=>
x
)
myTypes
:=
tt
:::
3
:::
false
:::
HNil
.
Definition
myNatIndex
:=
1.
Theorem
myNatIndex_ok
:
nth_error
myTypes
myNatIndex
=
Some
nat
.
reflexivity
.
Defined
.
Eval
compute
in
getNat
myValues
myNatIndex
myNatIndex_ok
.
(
**
%
\
vspace
{-
.15
in
}%
[[
=
3
]]
We
have
not
hit
the
problem
yet
,
since
we
proceeded
with
a
concrete
equality
proof
for
[
myNatIndex_ok
]
.
However
,
consider
a
case
where
we
want
to
reason
about
the
behavior
of
[
getNat
]
%
\
emph
{%
#
<
i
>
#
independently
#
</
i
>
#
%}%
of
a
specific
proof
.
*
)
Theorem
getNat_is_reasonable
:
forall
pf
,
getNat
myValues
myNatIndex
pf
=
3.
intro
;
compute
.
(
**
<<
1
subgoal
>>
%
\
vspace
{-
.3
in
}%
[[
pf
:
nth_error
myTypes
myNatIndex
=
Some
nat
============================
match
match
pf
in
(
_
=
y
)
return
(
nat
=
match
y
with
|
Some
H
=>
H
|
None
=>
nat
end
)
with
|
eq_refl
=>
eq_refl
end
in
(
_
=
T
)
return
T
with
|
eq_refl
=>
3
end
=
3
]]
Since
the
details
of
the
equality
proof
[
pf
]
are
not
known
,
computation
can
proceed
no
further
.
A
rewrite
with
axiom
K
would
allow
us
to
make
progress
,
but
we
can
rethink
the
definitions
a
bit
to
avoid
depending
on
axioms
.
*
)
Abort
.
(
**
Here
is
a
definition
of
a
function
that
turns
out
to
be
useful
,
though
no
doubt
its
purpose
will
be
mysterious
for
now
.
A
call
[
update
ls
n
x
]
overwrites
the
[
n
]
th
position
of
the
list
[
ls
]
with
the
value
[
x
]
,
padding
the
end
of
the
list
with
extra
[
x
]
values
as
needed
to
ensure
sufficient
length
.
*
)
Fixpoint
copies
A
(
x
:
A
)
(
n
:
nat
)
:
list
A
:=
match
n
with
|
O
=>
nil
|
S
n
'
=>
x
::
copies
x
n
'
end
.
Fixpoint
update
A
(
ls
:
list
A
)
(
n
:
nat
)
(
x
:
A
)
:
list
A
:=
match
ls
with
|
nil
=>
copies
x
n
++
x
::
nil
|
y
::
ls
'
=>
match
n
with
|
O
=>
x
::
ls
'
|
S
n
'
=>
y
::
update
ls
'
n
'
x
end
end
.
(
**
Now
let
us
revisit
the
definition
of
[
getNat
]
.
*
)
Section
withTypes
'
.
Variable
types
:
list
Set
.
Variable
natIndex
:
nat
.
(
**
Here
is
the
trick
:
instead
of
asserting
properties
about
the
list
[
types
]
,
we
build
a
%
``
%
#
"#new#"
#
%
''
%
list
that
is
%
\
emph
{%
#
<
i
>
#
guaranteed
by
construction
#
</
i
>
#
%}%
to
have
those
properties
.
*
)
Definition
types
'
:=
update
types
natIndex
nat
.
Variable
values
:
hlist
(
fun
x
:
Set
=>
x
)
types
'
.
(
**
Now
a
bit
of
dependent
pattern
matching
helps
us
rewrite
[
getNat
]
in
a
way
that
avoids
any
use
of
equality
proofs
.
*
)
Fixpoint
getNat
'
(
types
''
:
list
Set
)
(
natIndex
:
nat
)
:
hlist
(
fun
x
:
Set
=>
x
)
(
update
types
''
natIndex
nat
)
->
nat
:=
match
types
''
with
|
nil
=>
fun
vs
=>
hhd
vs
|
t
::
types0
=>
match
natIndex
return
hlist
(
fun
x
:
Set
=>
x
)
(
update
(
t
::
types0
)
natIndex
nat
)
->
nat
with
|
O
=>
fun
vs
=>
hhd
vs
|
S
natIndex
'
=>
fun
vs
=>
getNat
'
types0
natIndex
'
(
htl
vs
)
end
end
.
End
withTypes
'
.
(
**
Now
the
surprise
comes
in
how
easy
it
is
to
%
\
emph
{%
#
<
i
>
#
use
#
</
i
>
#
%}%
[
getNat
'
]
.
While
typing
works
by
modification
of
a
types
list
,
we
can
choose
parameters
so
that
the
modification
has
no
effect
.
*
)
Theorem
getNat_is_reasonable
:
getNat
'
myTypes
myNatIndex
myValues
=
3.
reflexivity
.
Qed
.
(
**
The
same
parameters
as
before
work
without
alteration
,
and
we
avoid
use
of
axioms
.
*
)
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