writing: a26312a33e3b4162413d85ec1bfee5baa1c350bc

     1: \newpage
     2: 
     3: \section{Groups of Coq tactics and number assignment}\label{sec:coqtactics}
     4: 
     5: % We have divided the Coq tactics in the groups presented in Table~\ref{tab:coqtactics}.
     6: 
     7: Table~\ref{tab:coqtactics} splits the Coq tactics into different groups. The formula used in the function $[.]_{tactic}$ 
     8: to compute the value of a Coq tactic is given by 
     9: $i+\sum_{j=0}^k\frac{1}{10 \times 2^{j-1}}$ where $i$ is the group of the tactic and $k$ is the position 
    10: of the tactic in that group (cf. right side of Table~\ref{tab:coqtactics}). 
    11: 
    12: \begin{table}[h]
    13: \tbl{{\scriptsize \emph{Groups of Coq tactics}}\label{tab:coqtactics}}{
    14: \centering
    15: \begin{tabular}{l||l}
    16: 
    17: Group & Tactics of the group\\
    18: 
    19: \hline
    20: \hline
    21: Group 1:           &  \lstinline?exact, eexact, assumption, eassumption, ?\\
    22: Applying theorems &  \lstinline?refine, apply, eapply, simple apply, lapply, ?\\
    23: \hline
    24: Group 2:           &  \lstinline?constructor, split, exists, left, right, ?\\
    25: Managing inductive constructors & \lstinline?econstructor, esplit, eexists, eleft, eright?\\
    26: \hline
    27: Group 3:           &  \lstinline?intro, intros, clear, rever, move, rename,  ?\\
    28: Managing local context & \lstinline?set, remember, pose, decompose?\\
    29: \hline
    30: Group 4:            &  \lstinline?assert, cut, pose, specialize, generalize, ?\\
    31: Controlling proof flow & \lstinline?evar, instantiate, admit, absurd, ?\\
    32: & \lstinline?contradition, contradict, exfalso?\\
    33: \hline
    34: Group 5:            & \lstinline?destruct, case, ecase, simple destruct,?\\
    35: Case analysis and induction & \lstinline?induction, einduction, elim, eelim, ?\\
    36:  & \lstinline?simple induction, double induction, ?\\
    37:      & \lstinline?dependent induction, functional induction,?\\
    38:   & \lstinline? discriminate, injection, fix, cofix, ?\\
    39:     & \lstinline? case_eq, elimtype?\\
    40: \hline
    41: Group 6:          &  \lstinline?rewrite, erewrite, cutrewrite, replace, ?\\
    42: Rewriting expressions &  \lstinline?reflexivity, symmetry, transitivity, subst, ?\\
    43: &  \lstinline?stepl, change?\\
    44: \hline
    45: Group 7:          &  \lstinline?cbv, compute, vm_compute, red, hnf, simpl, ?\\
    46: Performing computations  &  \lstinline?unfold, fold, pattern, conv_tactic?\\
    47: \hline
    48: Group 8:           &  \lstinline?auto, trivial, eauto, autounfold, ?\\
    49: Automation       &  \lstinline?autorewrite?\\
    50: \hline
    51: Group 9:           &  \lstinline?tauto, intuition, rtauto, firstorder, ?\\
    52: Decision procedures & \lstinline?congruence?\\
    53: \hline
    54: Group 10 &  \lstinline?decide equality, compare, simplify_eq,?\\
    55: Equality & \lstinline?esimplify_eq?\\
    56: \hline
    57: Group 11 &  \lstinline?inversion, dependent inversion,?\\
    58: Inversion & \lstinline?functional inversion, quote?\\
    59: \hline
    60: Group 12 & \lstinline?classical_left, classical_right?\\
    61: Classical tactics & \lstinline??\\
    62: \hline
    63: Group 13 & \lstinline?omega, ring, field, fourier?\\
    64: Automatizing & \\
    65: \hline
    66: Group 14 & Rest of Coq tactics\\
    67: \hline
    68: \end{tabular}}
    69: \end{table}
    70: 
    71: 
    72: