Ltac ==== Goal & context management ------------------------- Automatic variable naming ~~~~~~~~~~~~~~~~~~~~~~~~~ * Do not rely on Coq's automatically generated names. * Consider enabling `Mangle Names `_. Braces and bullets ~~~~~~~~~~~~~~~~~~ TODO No epic proofs ~~~~~~~~~~~~~~ TODO Destruct patterns ----------------- TODO Defining custom tactics ----------------------- TODO ``Tactic Notation`` ------------------- TODO Guidance on specific tactics ---------------------------- ``intros``, ``revert``, ``rename``, ``clear`` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TODO ``admit``, ``give_up`` ~~~~~~~~~~~~~~~~~~~~~~ TODO ``easy``, ``now``, ``assumption``, ``trivial`` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TODO ``try`` ~~~~~~~ TODO ``lia``, ``nia`` ~~~~~~~~~~~~~~~~ TODO ``left``, ``right``, ``exists``, ``constructor`` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TODO ``reflexivity``, ``symmetry``, ``transitivity``, ``congruence`` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TODO ``absurd``, ``contradiction``, ``exfalso`` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TODO ``exact``, ``apply``, ``refine`` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TODO ``simpl``, ``red``, ``cbv`` ~~~~~~~~~~~~~~~~~~~~~~~~~~~ TODO ``rewrite``, ``subst`` ~~~~~~~~~~~~~~~~~~~~~~ TODO ``assert ... as``, ``enough`` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TODO ``pose proof ... as`` ~~~~~~~~~~~~~~~~~~~~~ TODO ``remember ... as`` ~~~~~~~~~~~~~~~~~~~ TODO ``change ... with`` ~~~~~~~~~~~~~~~~~~~ TODO ``generalize`` ~~~~~~~~~~~~~~ TODO ``specialize`` ~~~~~~~~~~~~~~ TODO ``auto`` ~~~~~~~~ TODO ``eintros``, ``evar``, ``eauto``, ``erefine``, ``eassumption``, ``eenough``, ``instantiate`` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TODO