Tactics Index

# Coq Reference Manual

# Tactics Index

`∣∣`, 9.2 `;`, 9.2 `;[…``∣``…``∣``…]`, 9.2 `abstract`, 9.2 `absurd`, 8.4.1 `admit`, 8.3.17 `apply`, 8.3.6 `apply … with`, 8.3.6 `apply … in`, 8.3.9 `assert`, 8.3.8 `assert as`, 8.3.8 `assert by`, 8.3.8 `assumption`, 8.3.1 `auto`, 8.12.1 `autorewrite`, 8.12.13 `autounfold`, 8.12.3 `case`, 8.7.2 `case_eq`, 8.7.2 `cbv`, 8.5.1 `change`, 8.3.12 `change … in`, 8.3.12 `classical_left`, 8.11.1 `classical_right`, 8.11.1 `clear`, 8.3.2 `clear dependent`, 8.3.2 `clearbody`, 8.3.2 `cofix`, 8.3.14 `compare`, 8.9.2 `compute`, 8.5.1, 8.5.1 `congruence`, 8.12.8 `constr_eq`, 8.3.18 `constructor`, 8.6.1 `contradict`, 8.4.3 `contradiction`, 8.4.2 `cut`, 8.3.8 `cutrewrite`, 8.8.2 `decide equality`, 8.9.1 `decompose`, 8.7.6 `decompose record`, 8.7.6 `decompose sum`, 8.7.6 `dependent destruction`, 8.7.5 `dependent induction`, 8.7.5 `dependent induction … generalizing`, 8.7.5 `dependent inversion`, 8.10.1 `dependent inversion … as` , 8.10.1 `dependent inversion … as … with`, 8.10.1 `dependent inversion … with`, 8.10.1 `dependent inversion_clear`, 8.10.1 `dependent inversion_clear … as`, 8.10.1 `dependent inversion_clear … as … with`, 8.10.1 `dependent inversion_clear … with`, 8.10.1 `dependent rewrite ->`, 8.9.6 `dependent rewrite <-`, 8.9.6 `destruct`, 8.7.2 `discriminate`, 8.9.3 `discrR`, 3.2.4 `do`, 9.2 `eapply`, 8.3.6, 10.2 `eapply` `…``in`, 8.3.9 `eassumption`, 8.3.1 `eauto`, 8.12.2 `ecase`, 8.7.2 `econstructor`, 8.6.1 `edestruct`, 8.7.2 `ediscriminate`, 8.9.3 `eelim`, 8.7.1 `eexact`, 8.2.1 `eexists`, 8.6.1 `einduction`, 8.7.1 `einjection`, 8.9.4 `eleft`, 8.6.1 `elim … using`, 8.7.1 `elimtype`, 8.7.1 `erewrite`, 8.8.1 `eright`, 8.6.1 `esimplify_eq`, 8.9.5 `esplit`, 8.6.1 `evar`, 8.3.15 `exact`, 8.2.1 `exfalso`, 8.4.4 `exists`, 8.6.1 `f_equal`, 8.8.9 `fail`, 9.2 `field`, 8.12.11, 23.7 `field_simplify`, 8.12.11, 23.7 `field_simplify_eq`, 8.12.11, 23.7 `first`, 9.2 `firstorder`, 8.12.7 `firstorder` tactic, 8.12.7 `firstorder using`, 8.12.7 `firstorder with`, 8.12.7 `fix`, 8.3.13 `fold`, 8.5.6 `fourier`, 8.12.12 `functional induction`, 8.7.7, 10.4 `generalize`, 8.3.10 `generalize dependent`, 8.3.10 | `has_evar`, 8.3.20 `hnf`, 8.5.3 `idtac`, 9.2 `induction`, 8.7.1 `info`, 9.2 `injection`, 8.9.4 `injection … as`, 8.9.4 `instantiate`, 8.3.16 `intro`, 8.3.5 `intro after`, 8.3.5 `intro at bottom`, 8.3.5 `intro at top`, 8.3.5 `intro before`, 8.3.5 `intros`, 8.3.5 `intros` intro_pattern, 8.7.3 `intros until`, 8.3.5, 8.3.5 `intuition`, 8.12.5 `inversion`, 8.10.1, 10.5 `inversion … as`, 8.10.1 `inversion … as … in`, 8.10.1 `inversion … in`, 8.10.1 `inversion … using`, 8.10.1 `inversion … using … in`, 8.10.1 `inversion_clear`, 8.10.1 `inversion_clear … as … in`, 8.10.1 `inversion_clear … in`, 8.10.1 `inversion_cleardots as`, 8.10.1 `is_evar`, 8.3.19 `is_var`, 8.3.21 `lapply`, 8.3.6 `lazy`, 8.5.1 `left`, 8.6.1 `legacy field`, 23.9.3 `legacy ring`, 23.9.1 `lia`, 20.3 `move`, 8.3.3 `nsatz`, 24.1 `omega`, 8.12.9, 19.1 `pattern`, 8.5.7 `pose`, 8.3.7 `pose proof`, 8.3.8, 8.3.8 `progress`, 9.2 `psatz`, 20.1 `quote`, 8.10.4, 10.8 `red`, 8.5.2 `refine`, 8.2.2, 10.1 `reflexivity`, 8.8.4 `remember`, 8.3.7 `rename`, 8.3.4 `repeat`, 9.2 `replace … with`, 8.8.3 `revert`, 8.3.11 `revert dependent`, 8.3.11 `rewrite`, 8.8.1 `rewrite ->`, 8.8.1 `rewrite <-`, 8.8.1 `rewrite … at`, 8.8.1 `rewrite … by`, 8.8.1 `rewrite … in`, 8.8.1 `right`, 8.6.1 `ring`, 8.12.10, 23, 23.4 `ring_simplify`, 8.12.10, 23.4 `rtauto`, 8.12.6 `set`, 8.3.7 `setoid_replace`, 25 `simpl`, 8.5.4 `simpl … in`, 8.5.4 `simple apply`, 8.3.6 `simple apply` `…``in`, 8.3.9 `simple destruct`, 8.7.2 `simple eapply` `…``in`, 8.3.9 `simple induction`, 8.7.1 `simple inversion`, 8.10.1 `simple inversion … as`, 8.10.1 `simplify_eq`, 8.9.5 `solve`, 9.2 `specialize`, 8.3.8 `split`, 8.6.1 `split_Rabs`, 3.2.4 `split_Rmult`, 3.2.4 `stepl`, 8.8.8 `stepr`, 8.8.8 `subst`, 8.8.7 `symmetry`, 8.8.5 `symmetry in`, 8.8.5 `tauto`, 8.12.4 `transitivity`, 8.8.6 `trivial`, 8.12.1 `try`, 9.2 `unfold`, 8.5.5 `unfold … in`, 8.5.5 `vm_compute`, 8.5.1, 8.5.1