Proof

This page lists an number of useful tactics together with a few examples that illustrate their use. We also comment on what makes a proof robust or fragile.

Rewriting and Simplification

• rw, fs, lrw, simp, ...
• srw_ss, std_ss, bool_ss, pure_ss
• ARITH_ss
• DNF_ss
• link to writing custom simpsets etc.
• EQUIV_EXTRACT_ss

Abbreviations

• qmatch{_assum,}_abbrev_tac
• qabbrev_tac
• unabbrev_all_tac
• markerTheory.Abbrev_def

Renaming

• qmatch{_assum,}_rename_tac
• qx_gen_tac
• X_CHOOSE_THEN

Matching

• qpat_abbrev_tac
• qpat_assum

Improving automation

• export rewrites
• NO_TAC, TRY, ORELSE, THEN1

ConseqConv stuff

• CONSEQ_REWRITE_CONV / CONSEQ_REWRITE_TAC
• DEPTH_CONSEQ_CONV / DEPTH_CONSEQ_CONV_TAC
• EXISTS_EQ_CONSEQ_CONV / FORALL_EQ_CONSEQ_CONV

Pairs and tuple terms

• FORALL_PROD, EXISTS_PROD, LAMBDA_PROD
• UNCURRY
• PairCases_on
• PABS_ELIM_CONV
• PABS_INTRO_CONV

Conjunctions

• conj_asm{1,2}_tac
• CONJ_ASSOC, ...

Associative/Commutative operators

• AC

Equivalence relations

• any support in simplifier?

Quantifiers

• stuff like RIGHT_FORALL_IMP_THM
• QuantHeuristics
• QUANT_INST_ss [std_qp]
• QUANT_INST_TAC

Interactive proof management

• proofManagerLib.save

computeLib

Conversions

• CONV_TAC

Style

lcsymtacs

• -, >>, ...

infix and operator rebinding

semicolons

indentation

opening theories and libraries