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
434eb027
Commit
434eb027
authored
Aug 05, 2015
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Touch-ups in 8.4
parent
da4a8431
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
10 additions
and
8 deletions
+10
-8
Makefile
Makefile
+4
-2
cpdt.tex
latex/cpdt.tex
+1
-1
Equality.v
src/Equality.v
+2
-2
InductiveTypes.v
src/InductiveTypes.v
+1
-1
StackMachine.v
src/StackMachine.v
+2
-2
No files found.
Makefile
View file @
434eb027
...
@@ -28,8 +28,10 @@ clean:: Makefile.coq
...
@@ -28,8 +28,10 @@ clean:: Makefile.coq
doc
:
latex/cpdt.pdf html
doc
:
latex/cpdt.pdf html
COQDOC
=
coqdoc
-R
.
Cpdt
latex/%.v.tex
:
Makefile src/%.v src/%.glob
latex/%.v.tex
:
Makefile src/%.v src/%.glob
cd
src
;
coqdoc
--interpolate
--latex
--body-only
-s
\
cd
src
;
$(COQDOC)
--interpolate
--latex
--body-only
-s
\
$*
.v
-o
../latex/
$*
.v.tex
$*
.v
-o
../latex/
$*
.v.tex
latex/cpdt.pdf
:
latex/cpdt.tex $(TEX) latex/cpdt.bib
latex/cpdt.pdf
:
latex/cpdt.tex $(TEX) latex/cpdt.bib
...
@@ -40,7 +42,7 @@ latex/%.pdf: latex/%.tex latex/cpdt.bib
...
@@ -40,7 +42,7 @@ latex/%.pdf: latex/%.tex latex/cpdt.bib
html
:
Makefile $(VS) src/toc.html
html
:
Makefile $(VS) src/toc.html
mkdir
-p
html
mkdir
-p
html
cd
src
;
coqdoc
--interpolate
--no-externals
$(VS_DOC)
\
cd
src
;
$(COQDOC)
--interpolate
--no-externals
$(VS_DOC)
\
-d
../html
-d
../html
cp
src/toc.html html/
cp
src/toc.html html/
...
...
latex/cpdt.tex
View file @
434eb027
...
@@ -27,7 +27,7 @@ A print version of this book is available from the MIT Press. For more informat
...
@@ -27,7 +27,7 @@ A print version of this book is available from the MIT Press. For more informat
\mbox
{}
\vfill
\mbox
{}
\vfill
\begin{center}
\begin{center}
Copyright Adam Chlipala 2008-2013.
Copyright Adam Chlipala 2008-2013
, 2015
.
This work is licensed under a
This work is licensed under a
...
...
src/Equality.v
View file @
434eb027
...
@@ -833,7 +833,7 @@ eq_ind_r
...
@@ -833,7 +833,7 @@ eq_ind_r
P
x
->
forall
y
:
A
,
y
=
x
->
P
y
P
x
->
forall
y
:
A
,
y
=
x
->
P
y
]]
]]
The
corresponding
lemma
used
for
[
JMeq
]
in
the
proof
of
[
pair_cong
]
is
defined
internally
by
[
rewrite
as
needed
,
but
its
type
happens
to
be
the
following
.
*
)
The
corresponding
lemma
used
for
[
JMeq
]
in
the
proof
of
[
pair_cong
]
is
defined
internally
by
[
rewrite
]
as
needed
,
but
its
type
happens
to
be
the
following
.
*
)
(
**
%
\
vspace
{-
.15
in
}%
[[
(
**
%
\
vspace
{-
.15
in
}%
[[
internal_JMeq_rew_r
internal_JMeq_rew_r
...
@@ -843,7 +843,7 @@ internal_JMeq_rew_r
...
@@ -843,7 +843,7 @@ internal_JMeq_rew_r
The
key
difference
is
that
,
where
the
[
eq
]
lemma
is
parameterized
on
a
predicate
of
type
[
A
->
Prop
]
,
the
[
JMeq
]
lemma
is
parameterized
on
a
predicate
of
type
more
like
[
forall
A
:
Type
,
A
->
Prop
]
.
To
apply
[
eq_ind_r
]
with
a
proof
of
[
x
=
y
]
,
it
is
only
necessary
to
rearrange
the
goal
into
an
application
of
a
[
fun
]
abstraction
to
[
y
]
.
In
contrast
,
to
apply
the
alternative
principle
,
it
is
necessary
to
rearrange
the
goal
to
an
application
of
a
[
fun
]
abstraction
to
both
[
y
]
and
_
its
type_
.
In
other
words
,
the
predicate
must
be
_
polymorphic_
in
[
y
]
'
s
type
;
any
type
must
make
sense
,
from
a
type
-
checking
standpoint
.
There
may
be
cases
where
the
former
rearrangement
is
easy
to
do
in
a
type
-
correct
way
,
but
the
second
rearrangement
done
%
\
%
naive
%{}%
ly
leads
to
a
type
error
.
The
key
difference
is
that
,
where
the
[
eq
]
lemma
is
parameterized
on
a
predicate
of
type
[
A
->
Prop
]
,
the
[
JMeq
]
lemma
is
parameterized
on
a
predicate
of
type
more
like
[
forall
A
:
Type
,
A
->
Prop
]
.
To
apply
[
eq_ind_r
]
with
a
proof
of
[
x
=
y
]
,
it
is
only
necessary
to
rearrange
the
goal
into
an
application
of
a
[
fun
]
abstraction
to
[
y
]
.
In
contrast
,
to
apply
the
alternative
principle
,
it
is
necessary
to
rearrange
the
goal
to
an
application
of
a
[
fun
]
abstraction
to
both
[
y
]
and
_
its
type_
.
In
other
words
,
the
predicate
must
be
_
polymorphic_
in
[
y
]
'
s
type
;
any
type
must
make
sense
,
from
a
type
-
checking
standpoint
.
There
may
be
cases
where
the
former
rearrangement
is
easy
to
do
in
a
type
-
correct
way
,
but
the
second
rearrangement
done
%
\
%
naive
%{}%
ly
leads
to
a
type
error
.
When
[
rewrite
]
cannot
figure
out
how
to
apply
the
alternative
principle
for
[
x
==
y
]
where
[
x
]
and
[
y
]
have
the
same
type
,
the
tactic
can
instead
use
a
n
alternate
theorem
,
which
is
easy
to
prove
as
a
composition
of
[
eq_ind_r
]
and
[
JMeq_eq
]
.
*
)
When
[
rewrite
]
cannot
figure
out
how
to
apply
the
alternative
principle
for
[
x
==
y
]
where
[
x
]
and
[
y
]
have
the
same
type
,
the
tactic
can
instead
use
a
different
theorem
,
which
is
easy
to
prove
as
a
composition
of
[
eq_ind_r
]
and
[
JMeq_eq
]
.
*
)
Check
JMeq_ind_r
.
Check
JMeq_ind_r
.
(
**
%
\
vspace
{-
.15
in
}%
[[
(
**
%
\
vspace
{-
.15
in
}%
[[
...
...
src/InductiveTypes.v
View file @
434eb027
...
@@ -1116,7 +1116,7 @@ Theorem ntsize_ntsplice : forall tr1 tr2 : nat_tree, ntsize (ntsplice tr1 tr2)
...
@@ -1116,7 +1116,7 @@ Theorem ntsize_ntsplice : forall tr1 tr2 : nat_tree, ntsize (ntsplice tr1 tr2)
(** We can go further in automating the proof by exploiting the hint mechanism.%\index{Vernacular commands!Hint Extern}% *)
(** We can go further in automating the proof by exploiting the hint mechanism.%\index{Vernacular commands!Hint Extern}% *)
Restart.
Restart.
Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) =>
Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) =>
destruct LS; crush.
destruct LS; crush.
induction tr1 using nat_tree_ind'; crush.
induction tr1 using nat_tree_ind'; crush.
...
...
src/StackMachine.v
View file @
434eb027
...
@@ -12,9 +12,9 @@
...
@@ -12,9 +12,9 @@
(
**
I
will
start
off
by
jumping
right
in
to
a
fully
worked
set
of
examples
,
building
certified
compilers
from
increasingly
complicated
source
languages
to
stack
machines
.
We
will
meet
a
few
useful
tactics
and
see
how
they
can
be
used
in
manual
proofs
,
and
we
will
also
see
how
easily
these
proofs
can
be
automated
instead
.
This
chapter
is
not
meant
to
give
full
explanations
of
the
features
that
are
employed
.
Rather
,
it
is
meant
more
as
an
advertisement
of
what
is
possible
.
Later
chapters
will
introduce
all
of
the
concepts
in
bottom
-
up
fashion
.
In
other
words
,
it
is
expected
that
most
readers
will
not
understand
what
exactly
is
going
on
here
,
but
I
hope
this
demo
will
whet
your
appetite
for
the
remaining
chapters
!
(
**
I
will
start
off
by
jumping
right
in
to
a
fully
worked
set
of
examples
,
building
certified
compilers
from
increasingly
complicated
source
languages
to
stack
machines
.
We
will
meet
a
few
useful
tactics
and
see
how
they
can
be
used
in
manual
proofs
,
and
we
will
also
see
how
easily
these
proofs
can
be
automated
instead
.
This
chapter
is
not
meant
to
give
full
explanations
of
the
features
that
are
employed
.
Rather
,
it
is
meant
more
as
an
advertisement
of
what
is
possible
.
Later
chapters
will
introduce
all
of
the
concepts
in
bottom
-
up
fashion
.
In
other
words
,
it
is
expected
that
most
readers
will
not
understand
what
exactly
is
going
on
here
,
but
I
hope
this
demo
will
whet
your
appetite
for
the
remaining
chapters
!
As
always
,
you
can
step
through
the
source
file
<<
StackMachine
.
v
>>
for
this
chapter
interactively
in
Proof
General
.
Alternatively
,
to
get
a
feel
for
the
whole
lifecycle
of
creating
a
Coq
development
,
you
can
enter
the
pieces
of
source
code
in
this
chapter
in
a
new
<<.
v
>>
file
in
an
Emacs
buffer
.
If
you
do
the
latter
,
include
these
t
wo
lines
at
the
start
of
the
file
.
*
)
As
always
,
you
can
step
through
the
source
file
<<
StackMachine
.
v
>>
for
this
chapter
interactively
in
Proof
General
.
Alternatively
,
to
get
a
feel
for
the
whole
lifecycle
of
creating
a
Coq
development
,
you
can
enter
the
pieces
of
source
code
in
this
chapter
in
a
new
<<.
v
>>
file
in
an
Emacs
buffer
.
If
you
do
the
latter
,
include
these
t
hree
lines
at
the
start
of
the
file
.
*
)
Require
Import
Bool
Arith
List
CpdtTactics
.
Require
Import
Bool
Arith
List
Cpdt
.
Cpdt
Tactics
.
Set
Implicit
Arguments
.
Set
Implicit
Arguments
.
Set
Asymmetric
Patterns
.
Set
Asymmetric
Patterns
.
...
...
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