PROVE

bossLib.PROVE : thm list -> term -> thm

Also exported as BasicProvers.PROVE.

Prove a theorem with use of supplied lemmas.

An invocation PROVE thl M attempts to prove M using an automated reasoner supplied with the lemmas in thl. The automated reasoner performs a first order proof search. It currently provides some support for polymorphism and higher-order values (lambda terms).

Failure

If the proof search fails, or if M does not have type bool.

Example

> PROVE []  (concl SKOLEM_THM);
Meson search level: ........
val it = ⊢ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x): thm

> let open arithmeticTheory
  in
   PROVE [ADD_ASSOC, ADD_SYM, ADD_CLAUSES]
     (Term `x + 0 + y + z = y + (z + x)`)
  end;
Meson search level: ............
val it = ⊢ x + 0 + y + z = y + (z + x): thm

Comments

Some output (a row of dots) is currently generated as PROVE works. If the frequency of dot emission becomes slow, that is a sign that the term is not likely to be proved with the current lemmas.

Unlike MESON_TAC, PROVE can handle terms with conditionals.

See also

bossLib.PROVE_TAC, mesonLib.MESON_TAC, mesonLib.ASM_MESON_TAC