Skip to content
myreen edited this page Aug 8, 2012 · 11 revisions

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
  • 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

Clone this wiki locally