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
38ff4812
Commit
38ff4812
authored
7 years ago
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Plain Diff
Merge
parents
e138476d
a74d3620
Changes
7
Show whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
20 additions
and
16 deletions
+20
-16
cpdt.tex
latex/cpdt.tex
+1
-1
GeneralRec.v
src/GeneralRec.v
+2
-8
Intro.v
src/Intro.v
+2
-2
Match.v
src/Match.v
+1
-1
Reflection.v
src/Reflection.v
+3
-3
Universes.v
src/Universes.v
+3
-1
updates.rss
staging/updates.rss
+8
-0
No files found.
latex/cpdt.tex
View file @
38ff4812
...
@@ -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, 2015.
Copyright Adam Chlipala 2008-2013, 2015
, 2017
.
This work is licensed under a
This work is licensed under a
...
...
This diff is collapsed.
Click to expand it.
src/GeneralRec.v
View file @
38ff4812
...
@@ -822,10 +822,7 @@ Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
...
@@ -822,10 +822,7 @@ Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
match
goal
with
match
goal
with
|
[
H
:
Bnd
_
_
=
Bnd
_
_
|-
_
]
=>
injection
H
;
clear
H
;
intros
;
try
subst
|
[
H
:
Bnd
_
_
=
Bnd
_
_
|-
_
]
=>
injection
H
;
clear
H
;
intros
;
try
subst
end
.
end
.
move
H3
after
A
.
try
subst
B
.
(
*
This
line
expected
to
fail
in
Coq
8.4
and
succeed
in
Coq
8.6
.
*
)
generalize
dependent
B0
.
do
2
intro
.
subst
.
crush
.
crush
.
inversion
H
;
clear
H
;
crush
.
inversion
H
;
clear
H
;
crush
.
eauto
.
eauto
.
...
@@ -839,10 +836,7 @@ Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
...
@@ -839,10 +836,7 @@ Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
match
goal
with
match
goal
with
|
[
H
:
Bnd
_
_
=
Bnd
_
_
|-
_
]
=>
injection
H
;
clear
H
;
intros
;
try
subst
|
[
H
:
Bnd
_
_
=
Bnd
_
_
|-
_
]
=>
injection
H
;
clear
H
;
intros
;
try
subst
end
.
end
.
move
H3
after
B
.
try
subst
A
.
(
*
Same
as
above
*
)
generalize
dependent
B0
.
do
2
intro
.
subst
.
crush
.
crush
.
inversion
H0
;
clear
H0
;
crush
.
inversion
H0
;
clear
H0
;
crush
.
eauto
.
eauto
.
...
...
This diff is collapsed.
Click to expand it.
src/Intro.v
View file @
38ff4812
(
*
Copyright
(
c
)
2008
-
2013
,
2015
,
Adam
Chlipala
(
*
Copyright
(
c
)
2008
-
2013
,
2015
,
2017
,
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
...
@@ -186,7 +186,7 @@ Some readers have asked about the pragmatics of using this tactic library in the
...
@@ -186,7 +186,7 @@ Some readers have asked about the pragmatics of using this tactic library in the
(
**
**
Installation
and
Emacs
Set
-
Up
*
)
(
**
**
Installation
and
Emacs
Set
-
Up
*
)
(
**
(
**
At
the
start
of
the
next
chapter
,
I
assume
that
you
have
installed
Coq
and
Proof
General
.
The
code
in
this
book
is
tested
with
Coq
versions
8.4
pl
5
and
8.5
beta2
.
Though
parts
may
work
with
other
versions
,
it
is
expected
that
the
book
source
will
fail
to
build
with
_
earlier_
versions
.
At
the
start
of
the
next
chapter
,
I
assume
that
you
have
installed
Coq
and
Proof
General
.
The
code
in
this
book
is
tested
with
Coq
versions
8.4
pl
6
,
8.5
pl3
,
and
8.6
.
Though
parts
may
work
with
other
versions
,
it
is
expected
that
the
book
source
will
fail
to
build
with
_
earlier_
versions
.
%
\
index
{
Proof
General
|
(
}%
To
set
up
your
Proof
General
environment
to
process
the
source
to
the
next
chapter
,
a
few
simple
steps
are
required
.
%
\
index
{
Proof
General
|
(
}%
To
set
up
your
Proof
General
environment
to
process
the
source
to
the
next
chapter
,
a
few
simple
steps
are
required
.
...
...
This diff is collapsed.
Click to expand it.
src/Match.v
View file @
38ff4812
...
@@ -444,7 +444,7 @@ Ltac map T f :=
...
@@ -444,7 +444,7 @@ Ltac map T f :=
Sometimes
we
need
to
employ
the
opposite
direction
of
"nonterminal escape,"
when
we
want
to
pass
a
complicated
tactic
expression
as
an
argument
to
another
tactic
,
as
we
might
want
to
do
in
invoking
%
\
coqdocvar
{%
#
<
tt
>
#
map
#
</
tt
>
#
%}%.
*
)
Sometimes
we
need
to
employ
the
opposite
direction
of
"nonterminal escape,"
when
we
want
to
pass
a
complicated
tactic
expression
as
an
argument
to
another
tactic
,
as
we
might
want
to
do
in
invoking
%
\
coqdocvar
{%
#
<
tt
>
#
map
#
</
tt
>
#
%}%.
*
)
Goal
False
.
Goal
False
.
let
ls
:=
map
(
nat
*
nat
)
%
type
ltac
:
(
fun
x
=>
constr
:
(
x
,
x
))
(
1
::
2
::
3
::
nil
)
in
let
ls
:=
map
(
nat
*
nat
)
%
type
ltac
:
(
fun
x
=>
constr
:
(
(
x
,
x
)
))
(
1
::
2
::
3
::
nil
)
in
pose
ls
.
pose
ls
.
(
**
[[
(
**
[[
l
:=
(
1
,
1
)
::
(
2
,
2
)
::
(
3
,
3
)
::
nil
:
list
(
nat
*
nat
)
l
:=
(
1
,
1
)
::
(
2
,
2
)
::
(
3
,
3
)
::
nil
:
list
(
nat
*
nat
)
...
...
This diff is collapsed.
Click to expand it.
src/Reflection.v
View file @
38ff4812
...
@@ -673,7 +673,7 @@ Ltac addToList x xs :=
...
@@ -673,7 +673,7 @@ Ltac addToList x xs :=
let
b
:=
inList
x
xs
in
let
b
:=
inList
x
xs
in
match
b
with
match
b
with
|
true
=>
xs
|
true
=>
xs
|
false
=>
constr
:
(
x
,
xs
)
|
false
=>
constr
:
(
(
x
,
xs
)
)
end
.
end
.
(
**
Now
we
can
write
our
recursive
function
to
calculate
the
list
of
variable
values
we
will
want
to
use
to
represent
a
term
.
*
)
(
**
Now
we
can
write
our
recursive
function
to
calculate
the
list
of
variable
values
we
will
want
to
use
to
represent
a
term
.
*
)
...
@@ -718,8 +718,8 @@ Inductive formula' : Set :=
...
@@ -718,8 +718,8 @@ Inductive formula' : Set :=
Ltac
reifyTerm
xs
e
:=
Ltac
reifyTerm
xs
e
:=
match
e
with
match
e
with
|
True
=>
constr
:
Truth
'
|
True
=>
Truth
'
|
False
=>
constr
:
Falsehood
'
|
False
=>
Falsehood
'
|
?
e1
/
\
?
e2
=>
|
?
e1
/
\
?
e2
=>
let
p1
:=
reifyTerm
xs
e1
in
let
p1
:=
reifyTerm
xs
e1
in
let
p2
:=
reifyTerm
xs
e2
in
let
p2
:=
reifyTerm
xs
e2
in
...
...
This diff is collapsed.
Click to expand it.
src/Universes.v
View file @
38ff4812
...
@@ -1068,7 +1068,9 @@ Lemma proj1_again' : forall r, proof r
...
@@ -1068,7 +1068,9 @@ Lemma proj1_again' : forall r, proof r
The
first
goal
looks
reasonable
.
Hypothesis
[
H0
]
is
clearly
contradictory
,
as
[
discriminate
]
can
show
.
*
)
The
first
goal
looks
reasonable
.
Hypothesis
[
H0
]
is
clearly
contradictory
,
as
[
discriminate
]
can
show
.
*
)
discriminate
.
try
discriminate
.
(
*
Note
:
Coq
8.6
is
now
solving
this
subgoal
automatically
!
*
This
line
left
here
to
keep
everything
working
in
*
8.4
,
8.5
,
and
8.6
.
*
)
(
**
%
\
vspace
{-
.15
in
}%
[[
(
**
%
\
vspace
{-
.15
in
}%
[[
H
:
proof
p
H
:
proof
p
H1
:
And
p
q
=
And
p0
q0
H1
:
And
p
q
=
And
p0
q0
...
...
This diff is collapsed.
Click to expand it.
staging/updates.rss
View file @
38ff4812
...
@@ -11,6 +11,14 @@
...
@@ -11,6 +11,14 @@
<webMaster>
adam@chlipala.net
</webMaster>
<webMaster>
adam@chlipala.net
</webMaster>
<docs>
http://blogs.law.harvard.edu/tech/rss
</docs>
<docs>
http://blogs.law.harvard.edu/tech/rss
</docs>
<item>
<title>
Book source updated for Coq 8.6
</title>
<pubDate>
Wed, 12 Jul 2017 14:56:07 EDT
</pubDate>
<link>
http://adam.chlipala.net/cpdt/
</link>
<author>
adamc@csail.mit.edu
</author>
<description>
The online versions of the book have been updated with code that builds with Coq 8.6, the latest version, as well as old versions 8.4 and 8.5.
</description>
</item>
<item>
<item>
<title>
Book source updated for Coq 8.5
</title>
<title>
Book source updated for Coq 8.5
</title>
<pubDate>
Wed, 5 Aug 2015 18:08:34 EDT
</pubDate>
<pubDate>
Wed, 5 Aug 2015 18:08:34 EDT
</pubDate>
...
...
This diff is collapsed.
Click to expand it.
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