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
988f2896
Commit
988f2896
authored
Feb 04, 2013
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Unnecessary eauto
parent
1e47dade
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
4 additions
and
6 deletions
+4
-6
Predicates.v
src/Predicates.v
+4
-6
No files found.
src/Predicates.v
View file @
988f2896
...
...
@@ -808,14 +808,12 @@ Lemma even_contra' : forall n', even n' -> forall n, n' = S (n + n) -> False.
induction
1
;
crush
;
match
goal
with
|
[
H
:
S
?
N
=
?
N0
+
?
N0
|-
_
]
=>
destruct
N
;
destruct
N0
end
;
crush
;
eauto
.
end
;
crush
.
Qed
.
(
**
We
write
the
proof
in
a
way
that
avoids
the
use
of
local
variable
or
hypothesis
names
,
using
the
%
\
index
{
tactics
!
match
}%
[
match
]
tactic
form
to
do
pattern
-
matching
on
the
goal
.
We
use
unification
variables
prefixed
by
question
marks
in
the
pattern
,
and
we
take
advantage
of
the
possibility
to
mention
a
unification
variable
twice
in
one
pattern
,
to
enforce
equality
between
occurrences
.
The
hint
to
rewrite
with
[
plus_n_Sm
]
in
a
particular
direction
saves
us
from
having
to
figure
out
the
right
place
to
apply
that
theorem
,
and
we
also
take
critical
advantage
of
a
new
tactic
,
%
\
index
{
tactics
!
eauto
}%
[
eauto
]
.
(
**
We
write
the
proof
in
a
way
that
avoids
the
use
of
local
variable
or
hypothesis
names
,
using
the
%
\
index
{
tactics
!
match
}%
[
match
]
tactic
form
to
do
pattern
-
matching
on
the
goal
.
We
use
unification
variables
prefixed
by
question
marks
in
the
pattern
,
and
we
take
advantage
of
the
possibility
to
mention
a
unification
variable
twice
in
one
pattern
,
to
enforce
equality
between
occurrences
.
The
hint
to
rewrite
with
[
plus_n_Sm
]
in
a
particular
direction
saves
us
from
having
to
figure
out
the
right
place
to
apply
that
theorem
.
The
[
crush
]
tactic
uses
the
tactic
[
intuition
]
,
which
,
when
it
runs
out
of
tricks
to
try
using
only
propositional
logic
,
by
default
tries
the
tactic
[
auto
]
,
which
we
saw
in
an
earlier
example
.
For
now
,
think
of
[
eauto
]
as
a
potentially
more
expensive
version
of
[
auto
]
that
considers
more
possible
proofs
;
see
Chapter
13
for
more
detail
.
The
quick
summary
is
that
[
eauto
]
considers
applying
a
lemma
even
when
the
form
of
the
current
goal
doesn
not
uniquely
determine
the
values
of
all
of
the
lemma
'
s
quantified
variables
.
The
original
theorem
now
follows
trivially
from
our
lemma
.
*
)
The
original
theorem
now
follows
trivially
from
our
lemma
,
using
a
new
tactic
%
\
index
{
tactics
!
eauto
}%
[
eauto
]
,
a
fancier
version
of
[
auto
]
whose
explanation
we
postpone
to
Chapter
13.
*
)
Theorem
even_contra
:
forall
n
,
even
(
S
(
n
+
n
))
->
False
.
intros
;
eapply
even_contra
'
;
eauto
.
...
...
@@ -829,7 +827,7 @@ Lemma even_contra'' : forall n' n, even n' -> n' = S (n + n) -> False.
induction
1
;
crush
;
match
goal
with
|
[
H
:
S
?
N
=
?
N0
+
?
N0
|-
_
]
=>
destruct
N
;
destruct
N0
end
;
crush
;
eauto
.
end
;
crush
.
(
**
One
subgoal
remains
:
...
...
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