Indexes

Preamble

The language

match

The proof engine

Set

Unset

Proof using

L

User extensions

type_scope

function_scope

Scheme

Functional

Derive

Inversion

Practical tools

-j

Addendum

in

:=

omega

lra

lia

nra

nia

psatz

nsatz

Reference

+ (backtracking branching)

... : ... (goal selector)

... : ... (ssreflect)

=>

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

_

abstract

abstract (ssreflect)

absurd

admit

all: ...

apply

apply (ssreflect)

apply ... in

apply ... in ... as

assert

assert_fails

assert_succeeds

assumption

auto

autoapply

autorewrite

autounfold

btauto

by

case

case (ssreflect)

cbn

cbv

change

change_no_check

classical_left

classical_right

clear

clearbody

cofix

compare

compute

congr

congruence

congruence with

constr_eq

constr_eq_strict

constructor

contradict

contradiction

convert_concl_no_check

cut

cutrewrite

cycle

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

eapply

eassert

eassumption

easy

eauto

ecase

econstructor

edestruct

ediscriminate

eelim

eenough

eexact

eexists

einduction

einjection

eintros

eleft

elim

elim (ssreflect)

elim ... with

elimtype

enough

epose

epose proof

eremember

erewrite

eright

eset

esimplify_eq

esplit

evar

exact

exact_no_check

exactly_once

exfalso

exists

f_equal

fail

field

field_simplify

field_simplify_eq

finish_timing

first

first (ssreflect)

first last

firstorder

fix

fold

function induction

functional inversion

generalize

generally have

gfail

give_up

guard

has_evar

have

hnf

idtac

induction

induction ... using ...

info_trivial

injection

instantiate

intro

intros

intros ...

intuition

inversion

inversion ... using ...

inversion_clear

inversion_sigma

is_evar

is_var

lapply

last

last first

lazy

left

let ... := ...

ltac-seq

match goal

move

move ... after ...

move ... at bottom

move ... at top

move ... before ...

native_cast_no_check

native_compute

notypeclasses refine

now

once

only ... : ...

optimize_heap

over

par: ...

pattern

pose

pose (ssreflect)

pose proof

progress

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

rtauto

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

solve_constraints

specialize

split

split_Rabs

split_Rmult

start ltac profiling

stepl

stepr

stop ltac profiling

subst

suff

suffices

swap

symmetry

tauto

time

time_constr

timeout

transitivity

transparent_abstract

trivial

try

tryif

typeclasses eauto

under

unfold

unify

unlock

unshelve

vm_cast_no_check

vm_compute

without loss

wlog

|| (left-biased branching)