1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
\DOC LEANCOP
\TYPE {LEANCOP : thm list -> term -> thm}
\SYNOPSIS
Attempt to prove a term by first-order proof search using leanCop
connection-based prover.
\DESCRIBE
A call {LEANCOP[theorems] `tm`} will attempt to prove {tm} using pure
first-order reasoning, taking {theorems} as the starting-point. It will usually
either prove it completely or run for an infeasibly long time, but it may
sometimes fail quickly.
Although {LEANCOP} is capable of some fairly non-obvious pieces of first-order
reasoning, and will handle equality adequately, it does purely logical
reasoning. It will exploit no special properties of the constants in the goal,
other than equality and logical primitives. Any properties that are needed must
be supplied explicitly in the theorem list, e.g. {LE_REFL} to tell it that {<=}
on natural numbers is reflexive, or {REAL_ADD_SYM} to tell it that addition on
real numbers is symmetric.
\FAILURE
Fails if the term is unprovable within the search bounds.
\EXAMPLE
A typical application is to prove some elementary logical lemma for use inside
a tactic proof:
{
# LEANCOP [EXTENSION; IN_INSERT]
`x INSERT y INSERT s = y INSERT x INSERT s`;;
}
\USES
Generating simple logical lemmas as part of a large proof.
\SEEALSO
LEANCOP_TAC, MESON, METIS, NANOCOP.
\ENDDOC
|
