Specification language
match
in
type_scope
function_scope
Arguments
Proofs
Proof using
Scheme
Derive
Inversion
dependent destruction
dependent induction
lra
lia
nra
nia
psatz
zify
nsatz
Type
L
Using the Rocq Prover
Functional
coqrc
-vos
Appendix
+ (backtracking branching)
=>
[ … | … | … ] (dispatch)
[> … | … | … ] (dispatch)
abstract
abstract (ssreflect)
absurd
admit
apply
apply (ssreflect)
assert
assert_fails
assert_succeeds
assumption
auto
autoapply
autorewrite
autounfold
autounfold_one
btauto
bullet (- + *)
by
case
case (ssreflect)
case_eq
cbn
cbv
change
change_no_check
classical_left
classical_right
clear
clear dependent
clearbody
cofix
compare
compute
congr
congruence
constr_eq
constr_eq_nounivs
constr_eq_strict
constructor
context
contradict
contradiction
convert
cut
cycle
debug auto
debug eauto
debug trivial
decide
decide equality
decompose
decompose record
decompose sum
dependent generalize_eqs
dependent generalize_eqs_vars
dependent inversion
dependent inversion_clear
dependent rewrite
dependent simple inversion
destauto
destruct
dfs eauto
dintuition
discriminate
discrR
do
do (ssreflect)
done
dtauto
eapply
eassert
eassumption
easy
eauto
ecase
econstructor
edestruct
ediscriminate
eelim
eenough
eexact
eexists
einduction
einjection
eintros
eleft
elim
elim (ssreflect)
enough
epose
epose proof
eremember
erewrite
eright
eset
esimplify_eq
esplit
etransitivity
eval
evar
exact
exact (ssreflect)
exact_no_check
exactly_once
exfalso
exists
f_equal
fail
field
field_lookup
field_simplify
field_simplify_eq
finish_timing
first
first (ssreflect)
first last
firstorder
fix
fold
fresh
fun
functional induction
functional inversion
generalize
generalize dependent
generalize_eqs
generalize_eqs_vars
generally have
gfail
gintuition
give_up
guard
has_evar
have
head_of_constr
hnf
idtac
if-then-else (Ltac2)
induction
info_auto
info_eauto
info_trivial
injection
instantiate
intro
intros
intros until
intuition
inversion
inversion_clear
inversion_sigma
is_cofix
is_const
is_constructor
is_evar
is_fix
is_ground
is_ind
is_proj
is_var
lapply
last
last first
lazy
lazy_match!
lazy_match! goal
lazymatch
lazymatch goal
left
let
ltac-seq
match (Ltac2)
match goal
match!
match! goal
move
move (ssreflect)
multi_match!
multi_match! goal
multimatch
multimatch goal
native_cast_no_check
native_compute
not_evar
now
now_show
nsatz_compute
numgoals
once
only
optimize_heap
over
pattern
pose
pose (ssreflect)
pose proof
progress
protect_fv
rapply
red
refine
reflexivity
remember
rename
repeat
replace
reset ltac profile
restart_timer
revert
revert dependent
revgoals
rewrite
rewrite (ssreflect)
rewrite *
rewrite_db
rewrite_strat
right
ring
ring_lookup
ring_simplify
rtauto
set
set (ssreflect)
setoid_etransitivity
setoid_reflexivity
setoid_replace
setoid_rewrite
setoid_symmetry
setoid_transitivity
shelve
shelve_unifiable
show ltac profile
simpl
simple apply
simple congruence
simple destruct
simple eapply
simple induction
simple injection
simple inversion
simple subst
simplify_eq
soft functional induction
solve
solve_constraints
specialize
specialize_eqs
split
split_Rabs
split_Rmult
start ltac profiling
stepl
stepr
stop ltac profiling
subst
substitute
suff
suffices
swap
symmetry
tauto
time
time_constr
timeout
transitivity
transparent_abstract
trivial
try
tryif
type of
type_term
typeclasses eauto
under
unfold
unify
unlock
unshelve
vm_cast_no_check
vm_compute
with_strategy
without loss
wlia
wlog
wlra_Q
wnia
wnra_Q
wpsatz_Q
wpsatz_Z
wsos_Q
wsos_Z
xlia
xlra_Q
xlra_R
xnia
xnra_Q
xnra_R
xpsatz_Q
xpsatz_R
xpsatz_Z
xsos_Q
xsos_R
xsos_Z
zify_elim_let
zify_iter_let
zify_iter_specs
zify_op
zify_saturate
{
|| (first tactic making progress)
}
… : … (goal selector)
… : … (ssreflect)