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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
\DOC MESON_TAC
\TYPE {MESON_TAC : thm list -> tactic}
\SYNOPSIS
Automated first-order proof search tactic.
\DESCRIBE
A call to {MESON_TAC[theorems]} will attempt to establish the current goal
using pure first-order reasoning, taking {theorems} as the starting-point. (It
does not take the assumptions of the goal into account, but the similar
function {ASM_MESON_TAC} does.) It will usually either solve the goal
completely or run for an infeasible length of time before terminating, but it
may sometimes fail quickly.
Although {MESON_TAC} 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.
For more challenging first-order problems, {METIS_TAC} may be recommended.
\FAILURE
Fails if the goal is unprovable within the search bounds, though not
necessarily in a feasible amount of time.
\EXAMPLE
Here is a simple logical property taken from Dijstra's EWD 1062-1, which we set
as our goal:
{
# g `(!x. x <= x) /\
(!x y z. x <= y /\ y <= z ==> x <= z) /\
(!x y. f(x) <= y <=> x <= g(y))
==> (!x y. x <= y ==> f(x) <= f(y))`;;
}
It is solved quickly by:
{
# e(MESON_TAC[]);;
0..0..1..3..8..17..solved at 25
CPU time (user): 0.
val it : goalstack = No subgoals
}
Note however that the proof did not rely on any special features of `{<=}'; any
binary relation symbol would have worked. Even simple proofs that rely on
special properties of the constants need to have those properties supplied in
the list. Note also that {MESON} is limited to essentially first-order
reasoning, meaning that it cannot invent higher-order quantifier
instantiations. Thus, it cannot prove the following, which involves a
quantification over a function {g}:
{
# g `!f:A->B s.
(!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)) <=>
(?g. !x. x IN s ==> (g(f(x)) = x))`;;
}
\noindent However, we can manually reduce it to two subgoals:
{
# e(REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
EXISTS_TAC `?g:B->A. !y x. x IN s /\ y = f x ==> g y = x` THEN
CONJ_TAC THENL
[REWRITE_TAC[GSYM SKOLEM_THM]; AP_TERM_TAC THEN ABS_TAC]);;
val it : goalstack = 2 subgoals (2 total)
`(!y x. x IN s /\ y = f x ==> g y = x) <=> (!x. x IN s ==> g (f x) = x)`
`(!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) <=>
(!y. ?g. !x. x IN s /\ y = f x ==> g = x)`
}
\noindent and both of those are solvable directly by {MESON_TAC[]}.
\SEEALSO
ASM_MESON_TAC, GEN_MESON_TAC, MESON, METIS_TAC.
\ENDDOC
|
