# Coq Reference Manual

# Tactics Index

∣∣, 9.2 ;, 9.2 ;[…∣…∣…], 9.2 abstract, 9.2 absurd, 8.4.6 admit, 8.4.5 apply, 8.2.4 apply … in, 8.2.5 apply … with, 8.2.4 assert, 8.4.1 assert as, 8.4.1 assert by, 8.4.1 assumption, 8.2.2 auto, 8.8.1 autorewrite, 8.8.4 autounfold, 8.8.3 case, 8.5.1 case_eq, 8.5.1 cbv, 8.7.1 change, 8.6.9 change … in, 8.6.9 classical_left, 8.16.1 classical_right, 8.16.1 clear, 8.3.3 clear dependent, 8.3.3 clearbody, 8.3.3 cofix, 8.5.10 compare, 8.14.2 compute, 8.7.1, 8.7.1 congruence, 8.10.5 constr_eq, 8.12.1 constructor, 8.2.6 contradict, 8.4.8 contradiction, 8.4.7 cut, 8.4.1 cutrewrite, 8.6.2 decide equality, 8.14.1 decompose, 8.3.8 decompose record, 8.3.8 decompose sum, 8.3.8 dependent destruction, 8.5.4 dependent induction, 8.5.4 dependent induction … generalizing, 8.5.4 dependent inversion, 8.5.8 dependent inversion … as , 8.5.8 dependent inversion … as … with, 8.5.8 dependent inversion … with, 8.5.8 dependent inversion_clear, 8.5.8 dependent inversion_clear … as, 8.5.8 dependent inversion_clear … as … with, 8.5.8 dependent inversion_clear … with, 8.5.8 dependent rewrite ->, 8.14.4 dependent rewrite <-, 8.14.4 destruct, 8.5.1 discriminate, 8.5.6 discrR, 3.2.4 do, 9.2 double induction, 8.5.3 eapply, 8.2.4 eapply … in, 8.2.5 eassumption, 8.2.2 eauto, 8.8.2 ecase, 8.5.1 econstructor, 8.2.6 edestruct, 8.5.1 ediscriminate, 8.5.6 eelim, 8.5.2 eexact, 8.2.1 eexists, 8.2.6 einduction, 8.5.2 einjection, 8.5.7 eleft, 8.2.6 elim … using, 8.5.2 elimtype, 8.5.2 erewrite, 8.6.1 eright, 8.2.6 esimplify_eq, 8.14.3 esplit, 8.2.6 evar, 8.4.3 exact, 8.2.1 exfalso, 8.4.9 exists, 8.2.6 f_equal, 8.13.1 fail, 9.2 field, 8.17.3, 24.7 field_simplify, 8.17.3, 24.7 field_simplify_eq, 8.17.3, 24.7 first, 9.2 firstorder, 8.10.4 firstorder tactic, 8.10.4 firstorder using, 8.10.4 firstorder with, 8.10.4 fix, 8.5.9 fold, 8.7.6 fourier, 8.17.4 functional induction, 8.5.5, 13.2 generalize, 8.4.2 generalize dependent, 8.4.2 has_evar, 8.12.4 | hnf, 8.7.3 idtac, 9.2 induction, 8.5.2 info, 9.2 injection, 8.5.7 injection … as, 8.5.7 instantiate, 8.4.4 intro, 8.3.1 intro after, 8.3.1 intro at bottom, 8.3.1 intro at top, 8.3.1 intro before, 8.3.1 intros, 8.3.1 intros intro_pattern, 8.3.2 intros until, 8.3.1, 8.3.1 intuition, 8.10.2 inversion, 8.5.8 inversion … as, 8.5.8 inversion … as … in, 8.5.8 inversion … in, 8.5.8 inversion … using, 8.5.8, 13.3 inversion … using … in, 8.5.8 inversion_clear, 8.5.8 inversion_clear … as, 8.5.8 inversion_clear … as … in, 8.5.8 inversion_clear … in, 8.5.8 is_evar, 8.12.3 is_var, 8.12.5 lapply, 8.2.4 lazy, 8.7.1 left, 8.2.6 legacy field, 24.9.3 legacy ring, 24.9.1 lia, 21.5 lra, 21.1 move, 8.3.5 nia, 21.6 nsatz, 25.1 omega, 8.17.1, 20.1 pattern, 8.7.7 pose, 8.3.7 pose proof, 8.4.1, 8.4.1 progress, 9.2 psatz, 21.1 quote, 8.15.2, 10.3 red, 8.7.2 refine, 8.2.3 reflexivity, 8.6.4 remember, 8.3.7 rename, 8.3.6 repeat, 9.2 replace … with, 8.6.3 revert, 8.3.4 revert dependent, 8.3.4 rewrite, 8.6.1 rewrite ->, 8.6.1 rewrite <-, 8.6.1 rewrite … at, 8.6.1 rewrite … by, 8.6.1 rewrite … in, 8.6.1 right, 8.2.6 ring, 8.17.2, 24, 24.4 ring_simplify, 8.17.2, 24.4 rtauto, 8.10.3 set, 8.3.7 setoid_replace, 26 simpl, 8.7.4 simpl … in, 8.7.4 simple apply, 8.2.4 simple apply … in, 8.2.5 simple destruct, 8.5.1 simple eapply … in, 8.2.5 simple induction, 8.5.2 simple inversion, 8.5.8 simple inversion … as, 8.5.8 simplify_eq, 8.14.3 solve, 9.2 specialize, 8.4.1 split, 8.2.6 split_Rabs, 3.2.4 split_Rmult, 3.2.4 stepl, 8.6.8 stepr, 8.6.8 subst, 8.6.7 symmetry, 8.6.5 symmetry in, 8.6.5 tauto, 8.10.1 timeout, 9.2 transitivity, 8.6.6 trivial, 8.8.1 try, 9.2 unfold, 8.7.5 unfold … in, 8.7.5 unify, 8.12.2 vm_compute, 8.7.1, 8.7.1