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
be7d465a
Commit
be7d465a
authored
Jul 27, 2012
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Changes during more coqdoc hacking
parent
b8535f49
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
22 additions
and
13 deletions
+22
-13
Coinductive.v
src/Coinductive.v
+1
-2
Equality.v
src/Equality.v
+11
-9
Subset.v
src/Subset.v
+2
-2
Universes.v
src/Universes.v
+8
-0
No files found.
src/Coinductive.v
View file @
be7d465a
...
@@ -543,10 +543,9 @@ Qed.
...
@@ -543,10 +543,9 @@ Qed.
Definition
var
:=
nat
.
Definition
var
:=
nat
.
(
**
We
define
a
type
[
vars
]
of
maps
from
variables
to
values
.
To
define
a
function
[
set
]
for
setting
a
variable
'
s
value
in
a
map
,
we
import
the
[
Arith
]
module
from
Coq
'
s
standard
library
,
and
we
use
its
function
[
beq_nat
]
for
comparing
natural
numbers
.
*
)
(
**
We
define
a
type
[
vars
]
of
maps
from
variables
to
values
.
To
define
a
function
[
set
]
for
setting
a
variable
'
s
value
in
a
map
,
we
use
the
standard
library
function
[
beq_nat
]
for
comparing
natural
numbers
.
*
)
Definition
vars
:=
var
->
nat
.
Definition
vars
:=
var
->
nat
.
Require
Import
Arith
.
Definition
set
(
vs
:
vars
)
(
v
:
var
)
(
n
:
nat
)
:
vars
:=
Definition
set
(
vs
:
vars
)
(
v
:
var
)
(
n
:
nat
)
:
vars
:=
fun
v
'
=>
if
beq_nat
v
v
'
then
n
else
vs
v
'
.
fun
v
'
=>
if
beq_nat
v
v
'
then
n
else
vs
v
'
.
...
...
src/Equality.v
View file @
be7d465a
...
@@ -413,18 +413,16 @@ UIP_refl
...
@@ -413,18 +413,16 @@ UIP_refl
:
forall
(
U
:
Type
)
(
x
:
U
)
(
p
:
x
=
x
)
,
p
=
eq_refl
x
:
forall
(
U
:
Type
)
(
x
:
U
)
(
p
:
x
=
x
)
,
p
=
eq_refl
x
]]
]]
The
theorem
%
\
index
{
Gallina
terms
!
UIP
\
_
refl
}%
[
UIP_refl
]
comes
from
the
[
Eqdep
]
module
of
the
standard
library
.
Do
the
Coq
authors
know
of
some
clever
trick
for
building
such
proofs
that
we
have
not
seen
yet
?
If
they
do
,
they
did
not
use
it
for
this
proof
.
Rather
,
the
proof
is
based
on
an
_
axiom_
,
the
term
[
Eq_rect_eq
.
eq_rect_eq
]
below
.
*
)
The
theorem
%
\
index
{
Gallina
terms
!
UIP
\
_
refl
}%
[
UIP_refl
]
comes
from
the
[
Eqdep
]
module
of
the
standard
library
.
Do
the
Coq
authors
know
of
some
clever
trick
for
building
such
proofs
that
we
have
not
seen
yet
?
If
they
do
,
they
did
not
use
it
for
this
proof
.
Rather
,
the
proof
is
based
on
an
_
axiom_
,
the
term
[
eq_rect_eq
]
below
.
*
)
(
*
begin
hide
*
)
Definition
ere
:=
eq_rect_eq
.
(
*
end
hide
*
)
(
*
begin
hide
*
)
Import
Eq_rect_eq
.
(
*
end
hide
*
)
Print
eq_rect_eq
.
Print
eq_rect_eq
.
(
**
%
\
vspace
{-
.15
in
}%
[[
(
**
%
\
vspace
{-
.15
in
}%
[[
eq_rect_eq
=
***
[
eq_rect_eq
:
fun
U
:
Type
=>
Eq_rect_eq
.
eq_rect_eq
U
forall
(
U
:
Type
)
(
p
:
U
)
(
Q
:
U
->
Type
)
(
x
:
Q
p
)
(
h
:
p
=
p
)
,
:
forall
(
U
:
Type
)
(
p
:
U
)
(
Q
:
U
->
Type
)
(
x
:
Q
p
)
(
h
:
p
=
p
)
,
x
=
eq_rect
p
Q
x
p
h
]
x
=
eq_rect
p
Q
x
p
h
]]
]]
The
axiom
%
\
index
{
Gallina
terms
!
eq
\
_
rect
\
_
eq
}%
[
eq_rect_eq
]
states
a
"fact"
that
seems
like
common
sense
,
once
the
notation
is
deciphered
.
The
term
[
eq_rect
]
is
the
automatically
generated
recursion
principle
for
[
eq
]
.
Calling
[
eq_rect
]
is
another
way
of
[
match
]
ing
on
an
equality
proof
.
The
proof
we
match
on
is
the
argument
[
h
]
,
and
[
x
]
is
the
body
of
the
[
match
]
.
The
statement
of
[
eq_rect_eq
]
just
says
that
[
match
]
es
on
proofs
of
[
p
=
p
]
,
for
any
[
p
]
,
are
superfluous
and
may
be
removed
.
We
can
see
this
intuition
better
in
code
by
asking
Coq
to
simplify
the
theorem
statement
with
the
[
compute
]
reduction
strategy
(
which
,
by
the
way
,
applies
all
applicable
rules
of
the
definitional
equality
presented
in
this
chapter
'
s
first
section
)
.
*
)
The
axiom
%
\
index
{
Gallina
terms
!
eq
\
_
rect
\
_
eq
}%
[
eq_rect_eq
]
states
a
"fact"
that
seems
like
common
sense
,
once
the
notation
is
deciphered
.
The
term
[
eq_rect
]
is
the
automatically
generated
recursion
principle
for
[
eq
]
.
Calling
[
eq_rect
]
is
another
way
of
[
match
]
ing
on
an
equality
proof
.
The
proof
we
match
on
is
the
argument
[
h
]
,
and
[
x
]
is
the
body
of
the
[
match
]
.
The
statement
of
[
eq_rect_eq
]
just
says
that
[
match
]
es
on
proofs
of
[
p
=
p
]
,
for
any
[
p
]
,
are
superfluous
and
may
be
removed
.
We
can
see
this
intuition
better
in
code
by
asking
Coq
to
simplify
the
theorem
statement
with
the
[
compute
]
reduction
strategy
(
which
,
by
the
way
,
applies
all
applicable
rules
of
the
definitional
equality
presented
in
this
chapter
'
s
first
section
)
.
*
)
...
@@ -463,6 +461,10 @@ fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
...
@@ -463,6 +461,10 @@ fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
End
fhlist_map
.
End
fhlist_map
.
(
*
begin
hide
*
)
Require
Eqdep_dec
.
(
*
end
hide
*
)
(
**
It
is
worth
remarking
that
it
is
possible
to
avoid
axioms
altogether
for
equalities
on
types
with
decidable
equality
.
The
[
Eqdep_dec
]
module
of
the
standard
library
contains
a
parametric
proof
of
[
UIP_refl
]
for
such
cases
.
To
simplify
presentation
,
we
will
stick
with
the
axiom
version
in
the
rest
of
this
chapter
.
*
)
(
**
It
is
worth
remarking
that
it
is
possible
to
avoid
axioms
altogether
for
equalities
on
types
with
decidable
equality
.
The
[
Eqdep_dec
]
module
of
the
standard
library
contains
a
parametric
proof
of
[
UIP_refl
]
for
such
cases
.
To
simplify
presentation
,
we
will
stick
with
the
axiom
version
in
the
rest
of
this
chapter
.
*
)
...
...
src/Subset.v
View file @
be7d465a
...
@@ -402,7 +402,7 @@ Notation "'Yes'" := (left _ _).
...
@@ -402,7 +402,7 @@ Notation "'Yes'" := (left _ _).
Notation
"'No'"
:=
(
right
_
_
)
.
Notation
"'No'"
:=
(
right
_
_
)
.
Notation
"'Reduce' x"
:=
(
if
x
then
Yes
else
No
)
(
at
level
50
)
.
Notation
"'Reduce' x"
:=
(
if
x
then
Yes
else
No
)
(
at
level
50
)
.
(
**
The
[
Reduce
]
notation
is
notable
because
it
demonstrates
how
[
if
]
is
overloaded
in
Coq
.
The
[
if
]
form
actually
works
when
the
test
expression
has
any
two
-
constructor
inductive
type
.
Moreover
,
in
the
[
then
]
and
[
else
]
branches
,
the
appropriate
constructor
arguments
are
bound
.
This
is
important
when
working
with
[
sumbool
]
s
,
when
we
want
to
have
the
proof
stored
in
the
test
expression
available
when
proving
the
proof
obligations
generated
in
the
appropriate
branch
.
(
**
The
%
\
coqdocnotation
{%
#
<
tt
>
#
Reduce
#
</
tt
>
#
%}%
notation
is
notable
because
it
demonstrates
how
[
if
]
is
overloaded
in
Coq
.
The
[
if
]
form
actually
works
when
the
test
expression
has
any
two
-
constructor
inductive
type
.
Moreover
,
in
the
[
then
]
and
[
else
]
branches
,
the
appropriate
constructor
arguments
are
bound
.
This
is
important
when
working
with
[
sumbool
]
s
,
when
we
want
to
have
the
proof
stored
in
the
test
expression
available
when
proving
the
proof
obligations
generated
in
the
appropriate
branch
.
Now
we
can
write
[
eq_nat_dec
]
,
which
compares
two
natural
numbers
,
returning
either
a
proof
of
their
equality
or
a
proof
of
their
inequality
.
*
)
Now
we
can
write
[
eq_nat_dec
]
,
which
compares
two
natural
numbers
,
returning
either
a
proof
of
their
equality
or
a
proof
of
their
inequality
.
*
)
...
@@ -429,7 +429,7 @@ Eval compute in eq_nat_dec 2 3.
...
@@ -429,7 +429,7 @@ Eval compute in eq_nat_dec 2 3.
]]
]]
*
)
*
)
(
**
Note
that
the
[
Yes
]
and
[
No
]
notations
are
hiding
proofs
establishing
the
correctness
of
the
outputs
.
(
**
Note
that
the
%
\
coqdocnotation
{%
#
<
tt
>
#
Yes
#
</
tt
>
#
%}%
and
%
\
coqdocnotation
{%
#
<
tt
>
#
No
#
</
tt
>
#
%}%
notations
are
hiding
proofs
establishing
the
correctness
of
the
outputs
.
Our
definition
extracts
to
reasonable
OCaml
code
.
*
)
Our
definition
extracts
to
reasonable
OCaml
code
.
*
)
...
...
src/Universes.v
View file @
be7d465a
...
@@ -776,6 +776,10 @@ Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
...
@@ -776,6 +776,10 @@ Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
end
.
end
.
Qed
.
Qed
.
(
*
begin
hide
*
)
Require
Eqdep_dec
.
(
*
end
hide
*
)
(
**
These
corollaries
are
special
cases
of
proof
irrelevance
.
In
developments
that
only
need
proof
irrelevance
for
equality
,
there
is
no
need
to
assert
full
irrelevance
.
(
**
These
corollaries
are
special
cases
of
proof
irrelevance
.
In
developments
that
only
need
proof
irrelevance
for
equality
,
there
is
no
need
to
assert
full
irrelevance
.
Another
facet
of
proof
irrelevance
is
that
,
like
excluded
middle
,
it
is
often
provable
for
specific
propositions
.
For
instance
,
[
UIP
]
is
provable
whenever
the
type
[
A
]
has
a
decidable
equality
operation
.
The
module
[
Eqdep_dec
]
of
the
standard
library
contains
a
proof
.
A
similar
phenomenon
applies
to
other
notable
cases
,
including
less
-
than
proofs
.
Thus
,
it
is
often
possible
to
use
proof
irrelevance
without
asserting
axioms
.
Another
facet
of
proof
irrelevance
is
that
,
like
excluded
middle
,
it
is
often
provable
for
specific
propositions
.
For
instance
,
[
UIP
]
is
provable
whenever
the
type
[
A
]
has
a
decidable
equality
operation
.
The
module
[
Eqdep_dec
]
of
the
standard
library
contains
a
proof
.
A
similar
phenomenon
applies
to
other
notable
cases
,
including
less
-
than
proofs
.
Thus
,
it
is
often
possible
to
use
proof
irrelevance
without
asserting
axioms
.
...
@@ -844,6 +848,10 @@ Check dependent_unique_choice.
...
@@ -844,6 +848,10 @@ Check dependent_unique_choice.
This
axiom
lets
us
convert
a
relational
specification
[
R
]
into
a
function
implementing
that
specification
.
We
need
only
prove
that
[
R
]
is
truly
a
function
.
An
alternate
,
stronger
formulation
applies
to
cases
where
[
R
]
maps
each
input
to
one
or
more
outputs
.
We
also
simplify
the
statement
of
the
theorem
by
considering
only
non
-
dependent
function
types
.
*
)
This
axiom
lets
us
convert
a
relational
specification
[
R
]
into
a
function
implementing
that
specification
.
We
need
only
prove
that
[
R
]
is
truly
a
function
.
An
alternate
,
stronger
formulation
applies
to
cases
where
[
R
]
maps
each
input
to
one
or
more
outputs
.
We
also
simplify
the
statement
of
the
theorem
by
considering
only
non
-
dependent
function
types
.
*
)
(
*
begin
hide
*
)
Require
RelationalChoice
.
(
*
end
hide
*
)
Require
Import
ClassicalChoice
.
Require
Import
ClassicalChoice
.
Check
choice
.
Check
choice
.
(
**
%
\
vspace
{-
.15
in
}%
[[
(
**
%
\
vspace
{-
.15
in
}%
[[
...
...
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