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
e2cd4519
Commit
e2cd4519
authored
Jun 08, 2012
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Typesetting pass over LogicProg
parent
ee274487
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
7 additions
and
11 deletions
+7
-11
LogicProg.v
src/LogicProg.v
+7
-11
No files found.
src/LogicProg.v
View file @
e2cd4519
...
@@ -143,7 +143,7 @@ Example five_plus_three : plusR 5 3 8.
...
@@ -143,7 +143,7 @@ Example five_plus_three : plusR 5 3 8.
auto
6.
auto
6.
(
**
Sometimes
it
is
useful
to
see
a
description
of
the
proof
tree
that
[
auto
]
finds
,
with
the
%
\
index
{
tactics
!
info
}%
[
info
]
tactical
.
*
)
(
**
Sometimes
it
is
useful
to
see
a
description
of
the
proof
tree
that
[
auto
]
finds
,
with
the
%
\
index
{
tactics
!
info
}%
[
info
]
tactical
.
(
This
tactical
is
not
available
in
Coq
8.4
as
of
this
writing
,
but
I
hope
it
reappears
soon
.
)
*
)
Restart
.
Restart
.
info
auto
6.
info
auto
6.
...
@@ -155,7 +155,7 @@ Restart.
...
@@ -155,7 +155,7 @@ Restart.
Qed
.
Qed
.
(
*
end
thide
*
)
(
*
end
thide
*
)
(
**
The
two
key
components
of
logic
programming
are
%
\
index
{
backtracking
}%
_
backtracking_
and
%
\
index
{
unification
}%
_u
nification_
.
To
see
these
techniques
in
action
,
consider
this
further
silly
example
.
Here
our
candidate
proof
steps
will
be
reflexivity
and
quantifier
instantiation
.
*
)
(
**
The
two
key
components
of
logic
programming
are
%
\
index
{
backtracking
}%
_
backtracking_
and
%
\
index
{
unification
}%
_u
nification_
.
To
see
these
techniques
in
action
,
consider
this
further
silly
example
.
Here
our
candidate
proof
steps
will
be
reflexivity
and
quantifier
instantiation
.
*
)
Example
seven_minus_three
:
exists
x
,
x
+
3
=
7.
Example
seven_minus_three
:
exists
x
,
x
+
3
=
7.
(
*
begin
thide
*
)
(
*
begin
thide
*
)
...
@@ -185,7 +185,7 @@ Qed.
...
@@ -185,7 +185,7 @@ Qed.
Example
seven_minus_three
'
:
exists
x
,
plusR
x
3
7.
Example
seven_minus_three
'
:
exists
x
,
plusR
x
3
7.
(
*
begin
thide
*
)
(
*
begin
thide
*
)
(
**
We
could
attempt
to
guess
the
quantifier
instantiation
manually
as
before
,
but
here
there
is
no
need
.
Instead
of
[
apply
]
,
we
use
%
\
index
{
tactics
!
eapply
}%
[
eapply
]
instead
,
which
proceeds
with
placeholder
%
\
index
{
unification
variable
}%
_u
nification
variables_
standing
in
for
those
parameters
we
wish
to
postpone
guessing
.
*
)
(
**
We
could
attempt
to
guess
the
quantifier
instantiation
manually
as
before
,
but
here
there
is
no
need
.
Instead
of
[
apply
]
,
we
use
%
\
index
{
tactics
!
eapply
}%
[
eapply
]
instead
,
which
proceeds
with
placeholder
%
\
index
{
unification
variable
}%
_u
nification
variables_
standing
in
for
those
parameters
we
wish
to
postpone
guessing
.
*
)
eapply
ex_intro
.
eapply
ex_intro
.
(
**
[[
(
**
[[
...
@@ -380,7 +380,7 @@ Finished transaction in 2. secs (1.92012u,0.044003s)
...
@@ -380,7 +380,7 @@ Finished transaction in 2. secs (1.92012u,0.044003s)
Abort
.
Abort
.
End
slow
.
End
slow
.
(
**
Sometimes
,
though
,
transitivity
is
just
what
is
needed
to
get
a
proof
to
go
through
automatically
with
[
eauto
]
.
For
those
cases
,
we
can
use
named
%
\
index
{
hint
databases
}%
_
hint
databases_
to
segragate
hints
into
different
groups
that
may
be
called
on
as
needed
.
Here
we
put
[
eq_trans
]
into
the
database
[
slow
]
.
*
)
(
**
Sometimes
,
though
,
transitivity
is
just
what
is
needed
to
get
a
proof
to
go
through
automatically
with
[
eauto
]
.
For
those
cases
,
we
can
use
named
%
\
index
{
hint
databases
}%
_
hint
databases_
to
segragate
hints
into
different
groups
that
may
be
called
on
as
needed
.
Here
we
put
[
eq_trans
]
into
the
database
[
slow
]
.
*
)
(
*
begin
thide
*
)
(
*
begin
thide
*
)
Hint
Resolve
eq_trans
:
slow
.
Hint
Resolve
eq_trans
:
slow
.
...
@@ -791,7 +791,7 @@ Theorem bool_neq : true <> false.
...
@@ -791,7 +791,7 @@ Theorem bool_neq : true <> false.
(
*
begin
thide
*
)
(
*
begin
thide
*
)
auto
.
auto
.
(
**
[
crush
]
would
have
discharged
this
goal
,
but
the
default
hint
database
for
[
auto
]
contains
no
hint
that
applies
.
*
)
(
**
A
call
to
[
crush
]
would
have
discharged
this
goal
,
but
the
default
hint
database
for
[
auto
]
contains
no
hint
that
applies
.
*
)
Abort
.
Abort
.
...
@@ -804,7 +804,7 @@ Theorem bool_neq : true <> false.
...
@@ -804,7 +804,7 @@ Theorem bool_neq : true <> false.
Qed
.
Qed
.
(
*
end
thide
*
)
(
*
end
thide
*
)
(
**
[
Extern
]
hints
may
be
implemented
with
the
full
Ltac
language
.
This
example
shows
a
case
where
a
hint
uses
a
[
match
]
.
*
)
(
**
A
[
Hint
Extern
]
may
be
implemented
with
the
full
Ltac
language
.
This
example
shows
a
case
where
a
hint
uses
a
[
match
]
.
*
)
Section
forall_and
.
Section
forall_and
.
Variable
A
:
Set
.
Variable
A
:
Set
.
...
@@ -842,7 +842,7 @@ End forall_and.
...
@@ -842,7 +842,7 @@ End forall_and.
User
error
:
Bound
head
variable
User
error
:
Bound
head
variable
>>
>>
Coq
'
s
[
auto
]
hint
databases
work
as
tables
mapping
%
\
index
{
head
symbol
}%
_
head
symbols_
to
lists
of
tactics
to
try
.
Because
of
this
,
the
constant
head
of
an
[
Extern
]
pattern
must
be
determinable
statically
.
In
our
first
[
Extern
]
hint
,
the
head
symbol
was
[
not
]
,
since
[
x
<>
y
]
desugars
to
[
not
(
eq
x
y
)]
;
and
,
in
the
second
example
,
the
head
symbol
was
[
P
]
.
Coq
'
s
[
auto
]
hint
databases
work
as
tables
mapping
%
\
index
{
head
symbol
}%
_
head
symbols_
to
lists
of
tactics
to
try
.
Because
of
this
,
the
constant
head
of
an
[
Extern
]
pattern
must
be
determinable
statically
.
In
our
first
[
Extern
]
hint
,
the
head
symbol
was
[
not
]
,
since
[
x
<>
y
]
desugars
to
[
not
(
eq
x
y
)]
;
and
,
in
the
second
example
,
the
head
symbol
was
[
P
]
.
Fortunately
,
a
more
basic
form
of
[
Hint
Extern
]
also
applies
.
We
may
simply
leave
out
the
pattern
to
the
left
of
the
[
=>
]
,
incorporating
the
corresponding
logic
into
the
Ltac
script
.
*
)
Fortunately
,
a
more
basic
form
of
[
Hint
Extern
]
also
applies
.
We
may
simply
leave
out
the
pattern
to
the
left
of
the
[
=>
]
,
incorporating
the
corresponding
logic
into
the
Ltac
script
.
*
)
...
@@ -948,12 +948,8 @@ subgoal 4 is:
...
@@ -948,12 +948,8 @@ subgoal 4 is:
Qed
.
Qed
.
End
garden_path
.
End
garden_path
.
(
**
remove
printing
*
*
)
(
**
It
can
also
be
useful
to
apply
the
[
autorewrite
with
db
in
*
]
form
,
which
does
rewriting
in
hypotheses
,
as
well
as
in
the
conclusion
.
*
)
(
**
It
can
also
be
useful
to
apply
the
[
autorewrite
with
db
in
*
]
form
,
which
does
rewriting
in
hypotheses
,
as
well
as
in
the
conclusion
.
*
)
(
**
printing
*
$
*
$
*
)
Lemma
in_star
:
forall
x
y
,
f
(
f
(
f
(
f
x
)))
=
f
(
f
y
)
Lemma
in_star
:
forall
x
y
,
f
(
f
(
f
(
f
x
)))
=
f
(
f
y
)
->
f
x
=
f
(
f
(
f
y
))
.
->
f
x
=
f
(
f
(
f
y
))
.
(
*
begin
thide
*
)
(
*
begin
thide
*
)
...
...
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