MESON_TAC : thm list -> tactic
Automated first-order proof search tactic.
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 CONDITIONS
Fails if the goal is unprovable within the search bounds, though not
necessarily in a feasible amount of time.
Here is a simple logical property taken from Dijstra's EWD 1062-1, which we set
as our goal:
It is solved quickly by:
# 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))`;;
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:
0..0..1..3..8..17..solved at 25
CPU time (user): 0.
val it : goalstack = No subgoals
However, we can manually reduce it to two subgoals:
# 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))`;;
and both of those are solvable directly by MESON_TAC.
# 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
[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)`
- SEE ALSO
ASM_MESON_TAC, GEN_MESON_TAC, MESON, METIS_TAC.