Prove theorems in HOL Light via MCP tools. Use when the user asks to prove a theorem, verify a proof, or work with HOL Light tactics, goals, or lemmas.
You have access to a HOL Light theorem prover via MCP tools. This document teaches you how to use them effectively.
HOL Light is a classical higher-order logic theorem prover. The law of excluded middle is available, and proof by contradiction is fine. Only use (* ... *) for OCaml comments.
One-shot proofs: If you know the full tactic, use prove(goal, tactic) to get the theorem in a single call.
Interactive proofs:
"proved":trueAlways read the goal state carefully before choosing a tactic. The structured JSON tells you exactly what hypotheses you have and what you need to show.
| Tactic | Use when |
|---|---|
GEN_TAC | Goal is !x. P(x) — strips one universal quantifier |
X_GEN_TAC \n:num`` | Like GEN_TAC but names the variable |
STRIP_TAC | Goal has ==>, /\, or ! at the top — strips one connective |
REPEAT STRIP_TAC | Strip all top-level connectives at once |
CONJ_TAC | Goal is P /\ Q — splits into two subgoals |
DISJ1_TAC / DISJ2_TAC | Goal is P \/ Q — choose which disjunct to prove |
EQ_TAC | Goal is P <=> Q — splits into P ==> Q and Q ==> P |
DISCH_TAC | Move antecedent of P ==> Q into hypotheses |
EXISTS_TAC \witness`` | Goal is ?x. P(x) — provide the witness |
| Tactic | Use when |
|---|---|
REWRITE_TAC[thm1; thm2] | Rewrite goal using equations (left-to-right) |
ASM_REWRITE_TAC[thms] | Rewrite using hypotheses AND given theorems |
ONCE_REWRITE_TAC[thm] | Rewrite one pass, all topmost matches (not just one match!) |
GEN_REWRITE_TAC I [thm] | Rewrite at top level only |
GEN_REWRITE_TAC (RAND_CONV) [thm] | Rewrite only the operand of the top-level application |
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [thm] | Rewrite inside the LHS of a binary operator |
SIMP_TAC[thms] | Conditional rewriting (handles side conditions) |
ASM_SIMP_TAC[thms] | Conditional rewriting with hypotheses |
| Tactic | Solves |
|---|---|
ARITH_TAC | Linear arithmetic over naturals and integers (goal only, ignores hypotheses) |
REAL_ARITH_TAC | Linear arithmetic over reals |
MESON_TAC[thms] | First-order logic with given lemmas |
ASM_MESON_TAC[thms] | First-order logic with hypotheses + lemmas |
TAUT (as a rule) | Propositional tautologies: TAUT \p /\ q ==> q`` |
SET_TAC[thms] | Set-theoretic goals |
RING_TAC | Ring equalities |
WORD_RULE | Word (bitvector) equalities |
CONV_TAC WORD_RULE | Word equalities as a tactic |
| Tactic | Use when |
|---|---|
INDUCT_TAC | Induction on the outermost !n. (natural number) |
LIST_INDUCT_TAC | Induction on a list |
MATCH_MP_TAC thm | Apply a theorem backwards (modus ponens in reverse) |
| Tactic | Effect |
|---|---|
ASM_REWRITE_TAC[] | Rewrite goal using all hypotheses |
FIRST_X_ASSUM MATCH_MP_TAC | Use first matching hypothesis backwards (consumes it) |
FIRST_ASSUM MATCH_MP_TAC | Same but keeps the hypothesis |
UNDISCH_TAC \term`` | Move a hypothesis back to the goal as antecedent |
SUBGOAL_THEN \P` ASSUME_TAC` | Assert and prove an intermediate fact |
SUBGOAL_THEN \P` MP_TAC` | Assert, prove, and add as antecedent of goal |
SUBGOAL_THEN \P` SUBST1_TAC` | Assert, prove, and substitute the equality in goal |
SUBGOAL_THEN \P` STRIP_ASSUME_TAC` | Assert, prove, and split conjunctions into separate assumptions |
ABBREV_TAC \x = expr`` | Replace expr with x in goal, add expr = x as assumption |
EXPAND_TAC "x" | Expand an abbreviation introduced by ABBREV_TAC |
| Combinator | Meaning |
|---|---|
tac1 THEN tac2 | Apply tac1, then tac2 to all resulting subgoals |
tac1 THENL [tac2; tac3] | Apply tac1, then tac2 to first subgoal, tac3 to second |
REPEAT tac | Apply tac repeatedly until it fails |
TRY tac | Try tac, succeed even if it fails |
search_theorems searches by name substring. The search is cheap — use it freely. Tips:
search_theorems name="EVEN" for theorems about EVENsearch_theorems name="ADD" for addition theoremsADD_, MULT_, LE_, LT_, EVEN_, ODD_, DIV_, MOD_<=> or = in the statementYou can also use eval for more powerful searches:
eval 'search [`EVEN`]' -- search by subterm pattern
eval 'search [`EVEN`; `ODD`]' -- multiple patterns
apply_tactic "SIMP_TAC[thm1; thm2; thm3]"
apply_tactic "REWRITE_TAC[DEF1; DEF2] THEN ARITH_TAC"
apply_tactic "INDUCT_TAC" -- creates base case + inductive step
apply_tactic "base case tactic" -- solve base case
apply_tactic "ASM_REWRITE_TAC[...] THEN inductive step tactic"
search_theorems name="KEY_LEMMA"
apply_tactic "MATCH_MP_TAC KEY_LEMMA THEN ..."
apply_tactic "ASM_CASES_TAC `P` THEN ASM_REWRITE_TAC[]"
apply_tactic "SUBGOAL_THEN `intermediate_fact` ASSUME_TAC"
-- prove the sub-lemma first, then use it
REWRITE_TAC[GSYM thm] can loop. Use ONCE_REWRITE_TAC[GSYM thm] instead.ONCE_REWRITE_TAC rewrites ALL topmost matches, not just one. If the goal has f a b and f c d, and the theorem matches f x y, both get rewritten in one pass. For targeted single-occurrence rewriting, use GEN_REWRITE_TAC with conversionals like RAND_CONV, LAND_CONV.FIRST_X_ASSUM consumes the hypothesis. Use FIRST_ASSUM when you need to reuse it.ARITH_TAC ignores hypotheses. Use UNDISCH_TAC \needed_fact`to bring assumptions into the goal first.ASM_ARITH_TACuses hypotheses but can hang with manyval(...)` terms.ASM_ARITH_TAC hangs with many assumptions. Discard irrelevant ones first with REPEAT (FIRST_X_ASSUM (K ALL_TAC)) or targeted UNDISCH_TAC + DISCH_TAC.SUBST1_TAC silently succeeds even when the LHS doesn't appear in the goal. It just does nothing. This makes FIRST_ASSUM(fun th -> SUBST1_TAC(SYM th)) unreliable — it picks the first assumption where the tactic "succeeds" (which is all of them). Use EXPAND_TAC "name" to expand abbreviations instead.THEN vs THENL after SUBGOAL_THEN ... SUBST1_TAC. THEN applies the proof to ALL subgoals (both the equality proof and the main goal). Use THENL [equality_proof; ALL_TAC] to target only the first subgoal.WORD_RULE hangs on val(word(...)). Normalize via VAL_WORD_EQ first.n - m = 0 when m >= n. Use ARITH_TAC for goals involving subtraction.* is right-associative for num. Use explicit parentheses to avoid surprises.MESON_TAC, ARITH_TAC) can diverge on hard goals.For proving properties of AArch64 machine code (requires arm/proofs/base.ml):
| Tactic | Use when |
|---|---|
ARM_MK_EXEC_RULE mc | Decode a machine code byte list into instruction theorems |
ENSURES_INIT_TAC "s0" | Initialize symbolic state for an ensures proof |
ARM_STEPS_TAC EXEC (1--n) | Symbolically execute n instructions |
ARM_SIM_TAC EXEC (1--n) | INIT + STEPS + FINAL in one shot |
ENSURES_FINAL_STATE_TAC | Close postcondition and frame |
ENSURES_WHILE_PAUP_TAC a b pc_body pc_back inv | Declare a counting-up loop with invariant |
COND_CASES_TAC | Case split on a conditional branch |
CONV_TAC WORD_RULE | Solve word (bitvector) equalities |
WORD_BLAST | Bit-blasting for word goals |
Typical ARM proof pattern:
REPEAT STRIP_TAC THEN ENSURES_INIT_TAC "s0" THEN
ARM_STEPS_TAC EXEC (1--n) THEN
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
CONV_TAC WORD_RULE
hol_type with term `1 + 1` returns num)needs (e.g., hol_load with file "Library/words.ml")MESON_TAC diverges)ARITH_TAC, MESON_TAC[], or ASM_MESON_TAC[] often solve goals outright.search_theorems to find the right lemma name rather than guessing.REPEAT STRIP_TAC is almost always a good opening move.ASM_REWRITE_TAC[] is your friend. It rewrites with all hypotheses. Use it after STRIP_TAC.SUBGOAL_THEN for declarative proofs. Clear intermediate goals make proofs easier to follow.