-
Notifications
You must be signed in to change notification settings - Fork 143
Proof
thtuerk edited this page Aug 23, 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.
- 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
- qmatch{_assum,}_abbrev_tac
- qabbrev_tac
- unabbrev_all_tac
- markerTheory.Abbrev_def
- qmatch{_assum,}_rename_tac
- qx_gen_tac
- X_CHOOSE_THEN
- qpat_abbrev_tac
- qpat_assum
- export rewrites
- NO_TAC, TRY, ORELSE, THEN1
- CONSEQ_REWRITE_CONV / CONSEQ_REWRITE_TAC
- DEPTH_CONSEQ_CONV / DEPTH_CONSEQ_CONV_TAC
- EXISTS_EQ_CONSEQ_CONV / FORALL_EQ_CONSEQ_CONV
- FORALL_PROD, EXISTS_PROD, LAMBDA_PROD
- UNCURRY
- PairCases_on
- PABS_ELIM_CONV
- PABS_INTRO_CONV
- conj_asm{1,2}_tac
- CONJ_ASSOC, ...
- AC
- any support in simplifier?
- stuff like RIGHT_FORALL_IMP_THM
- QuantHeuristics
- QUANT_INST_ss [std_qp]
- QUANT_INST_TAC
- proofManagerLib.save
- CONV_TAC
The library Sanity allows to check theorems and whole theories with simple syntactic checks. For example, clashes between theorem names in different theories, dodgy variable names, forgotten or unnecessary quantification etc. can be checked.
-
-, >>, ...