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.

Abbreviations

• qmatch{_assum,}_abbrev_tac
• qabbrev_tac test test1
• 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

Pairs and tuple terms

• FORALL_PROD, EXISTS_PROD, LAMBDA_PROD
• UNCURRY
• PairCases_on

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

Interactive proof management

• proofManagerLib.save

computeLib

Conversions

• CONV_TAC

Style

lcsymtacs

• -, >>, ...

infix and operator rebinding

semicolons

indentation

opening theories and libraries