Tactic Index

+ | . | = | [ | _ | a | b | c | d | e | f | g | h | i | l | m | n | o | p | q | r | s | t | u | v | w | |


	+
	`+ (backtracking branching)`

	.
	`... : ... (goal selector)`
	`... : ... (ssreflect)`

	=
	`=>`

	[
	`[> ... \| ... \| ... ] (dispatch)`

	_
	`_`

	a
	`abstract`
	`abstract (ssreflect)`
	`absurd`
	`admit`
	`all: ...`
	`apply`
	`apply (ssreflect)`
	`apply ... in`
	`apply ... in ... as`
	`assert`
	`assert_fails`
	`assert_succeeds`
	`assumption`
	`auto`
	`autoapply`
	`autorewrite`
	`autounfold`

	b
	`btauto`
	`by`

	c
	`case`
	`case (ssreflect)`
	`cbn`
	`cbv`
	`change`
	`classical_left`
	`classical_right`
	`clear`
	`clearbody`
	`cofix`
	`compare`
	`compute`
	`congr`
	`congruence`
	`congruence with`
	`constr_eq`
	`constr_eq_strict`
	`constructor`
	`contradict`
	`contradiction`
	`cut`
	`cutrewrite`
	`cycle`

	d
	`debug auto`
	`debug trivial`
	`decide equality`
	`decompose`
	`dependent destruction`
	`dependent induction`
	`dependent inversion`
	`dependent inversion ... with ...`
	`dependent rewrite ->`
	`dependent rewrite <-`
	`destruct`
	`destruct ... eqn:`
	`dintuition`
	`discriminate`
	`discrR`
	`do`
	`do (ssreflect)`
	`done`
	`double induction`
	`dtauto`

	e
	`eapply`
	`eassert`
	`eassumption`
	`easy`
	`eauto`
	`ecase`
	`econstructor`
	`edestruct`
	`ediscriminate`
	`eelim`
	`eenough`
	`eexact`
	`eexists`
	`einduction`
	`einjection`
	`eleft`
	`elim`
	`elim (ssreflect)`
	`elim ... with`
	`elimtype`
	`enough`
	`epose`
	`epose proof`
	`eremember`
	`erewrite`
	`eright`
	`eset`
	`esimplify_eq`
	`esplit`
	`evar`
	`exact`
	`exactly_once`
	`exfalso`
	`exists`

	f
	`f_equal`
	`fail`
	`field`
	`field_simplify`
	`field_simplify_eq`
	`finish_timing`
	`first`
	`first (ssreflect)`
	`first last`
	`firstorder`
	`fix`
	`fold`
	`function induction`
	`functional inversion`

	g
	`generalize`
	`generally have`
	`gfail`
	`give_up`
	`guard`

	h
	`has_evar`
	`have`
	`hnf`

	i
	`idtac`
	`in`
	`induction`
	`induction ... using ...`
	`info_trivial`
	`injection`
	`instantiate`
	`intro`
	`intros`
	`intros ...`
	`intuition`
	`inversion`
	`inversion_clear`
	`inversion_sigma`
	`is_evar`
	`is_var`

	l
	`lapply`
	`last`
	`last first`
	`lazy`
	`left`
	`let ... := ...`
	`lia`
	`lra`
	`ltac-seq`

	m
	`match goal`
	`move`
	`move ... after ...`
	`move ... at bottom`
	`move ... at top`
	`move ... before ...`

	n
	`native_compute`
	`nia`
	`notypeclasses refine`
	`now`
	`nra`
	`nsatz`

	o
	`omega`
	`once`
	`only ... : ...`
	`optimize_heap`

	p
	`par: ...`
	`pattern`
	`pose`
	`pose (ssreflect)`
	`pose proof`
	`progress`
	`psatz`

	q
	`quote`

	r
	`red`
	`refine`
	`reflexivity`
	`remember`
	`rename`
	`repeat`
	`replace`
	`reset ltac profile`
	`restart_timer`
	`revert`
	`revert dependent`
	`revgoals`
	`rewrite`
	`rewrite (ssreflect)`
	`rewrite_strat`
	`right`
	`ring`
	`ring_simplify`
	`romega`
	`rtauto`

	s
	`set`
	`set (ssreflect)`
	`setoid_reflexivity`
	`setoid_replace`
	`setoid_rewrite`
	`setoid_symmetry`
	`setoid_transitivity`
	`shelve`
	`shelve_unifiable`
	`show ltac profile`
	`simpl`
	`simple apply`
	`simple destruct`
	`simple eapply`
	`simple induction`
	`simple inversion`
	`simple notypeclasses refine`
	`simple refine`
	`simplify_eq`
	`solve`
	`specialize`
	`split`
	`split_Rabs`
	`split_Rmult`
	`start ltac profiling`
	`stepl`
	`stepr`
	`stop ltac profiling`
	`subst`
	`suff`
	`suffices`
	`swap`
	`symmetry`

	t
	`tauto`
	`time`
	`time_constr`
	`timeout`
	`transitivity`
	`transparent_abstract`
	`trivial`
	`try`
	`tryif`
	`typeclasses eauto`

	u
	`unfold`
	`unify`
	`unlock`

	v
	`vm_compute`

	w
	`without loss`
	`wlog`

	\|
	`\|\| (left-biased branching)`