listings coq style

lstcoq.sty

% lstlisting coq style (inspired from https://github.com/cmc333333/forensics-thesis)
% lstlisting coq style (inspired from a file of Assia Mahboubi)
%
\lstdefinelanguage{coq}{ 
%
% Anything betweeen $ becomes LaTeX math mode
mathescape=true,
%
% Comments may or not include Latex commands
texcl=false, 
%
% Vernacular commands
morekeywords=[1]{Section, Module, End, Require, Import, Export,
  Variable, Variables, Parameter, Parameters, Axiom, Hypothesis,
  Hypotheses, Notation, Local, Tactic, Reserved, Scope, Open, Close,
  Bind, Delimit, Definition, Let, Ltac, Fixpoint, CoFixpoint, Add,
  Morphism, Relation, Implicit, Arguments, Unset, Contextual,
  Strict, Prenex, Implicits, Inductive, CoInductive, Record,
  Structure, Canonical, Coercion, Context, Class, Global, Instance,
  Program, Infix, Theorem, Lemma, Corollary, Proposition, Fact,
  Remark, Example, Proof, Goal, Save, Qed, Defined, Hint, Resolve,
  Rewrite, View, Search, Show, Print, Printing, All, Eval, Check,
  Projections, inside, outside, Def},
%
% Gallina
morekeywords=[2]{forall, exists, exists2, fun, fix, cofix, struct,
  match, with, end, as, in, return, let, if, is, then, else, for, of,
  nosimpl, when},
%
% Sorts
morekeywords=[3]{Type, Prop, Set, true, false, option},
%
% Various tactics, some are std coq subsumed by ssr, for the manual purpose
morekeywords=[4]{pose, set, move, case, elim, apply, clear, hnf,
  intro, intros, generalize, rename, pattern, after, destruct,
  induction, using, refine, inversion, injection, rewrite, congr,
  unlock, compute, ring, field, fourier, replace, fold, unfold,
  change, cutrewrite, simpl, have, suff, wlog, suffices, without,
  loss, nat_norm, assert, cut, trivial, revert, bool_congr, nat_congr,
  symmetry, transitivity, auto, split, left, right, autorewrite},
%
% Terminators
morekeywords=[5]{by, done, exact, reflexivity, tauto, romega, omega,
  assumption, solve, contradiction, discriminate},
%
% Control
morekeywords=[6]{do, last, first, try, idtac, repeat},
%
% Comments delimiters, we do turn this off for the manual
morecomment=[s]{(*}{*)},
%
% Spaces are not displayed as a special character
showstringspaces=false,
%
% String delimiters
morestring=[b]",
morestring=[d]’,
%
% Size of tabulations
tabsize=4,
%
% Enables ASCII chars 128 to 255
extendedchars=false,
%
% Case sensitivity
sensitive=true,
%
% Automatic breaking of long lines
breaklines=false,
%
% Default style fors listings
% basicstyle=\small,
%
% Position of captions is bottom
captionpos=b,
%
% flexible columns
columns=[l]flexible,
%
% Style for (listings') identifiers
identifierstyle={\codefontfamily\color{black}},
% Style for declaration keywords
keywordstyle=[1]{\codefontfamily\bfseries\color{black}},
% Style for gallina keywords
keywordstyle=[2]{\codefontfamily\color{dkgreen}},
% Style for sorts keywords
keywordstyle=[3]{\codefontfamily\color{ltblue}},
% Style for tactics keywords
keywordstyle=[4]{\codefontfamily\color{dkblue}},
% Style for terminators keywords
keywordstyle=[5]{\codefontfamily\color{dkred}},
%Style for iterators
keywordstyle=[6]{\codefontfamily\color{ff79c6}},
% Style for strings
stringstyle=\codefontfamily,
% Style for comments
commentstyle={\codefontfamily\color{dkgreen}},
%
%moredelim=**[is][\codefontfamily\color{red}]{/&}{&/},
literate=
    % {fun}{{$\lambda\;$}}1
    % {nat}{{$\mathbb{N}\;$}}1
    % {Prop}{{$\mathbb{P}\;$}}1
    {True}{{$\top$}}1
    {False}{{$\bot$}}1
    {|-}{{$\vdash$}}1
    {|=}{{$\vDash$}}1
    {forall}{{\color{dkgreen}{$\forall\;$}}}1
    {exists}{{$\exists\;$}}1
    {<-}{{$\leftarrow\;$}}1
    {=>}{{$\Rightarrow\;$}}1
    {==}{{\code{==}\;}}1
    {==>}{{\code{==>}\;}}1
%    {:>}{{\code{:>}\;}}1
    {->}{{$\rightarrow\;$}}1
    {<->}{{$\leftrightarrow\;$}}1
    {<==}{{$\leq\;$}}1
    {\#}{{$^\star$}}1 
    {\\o}{{$\circ\;$}}1 
   % {\@}{{$\cdot$}}1 
    {\/\\}{{$\wedge\;$}}1
    {\\\/}{{$\vee\;$}}1
    % {++}{{++}}1
    {~}{{$\lnot$}}1
    {\@\@}{{$@$}}1
    {\\mapsto}{{$\mapsto\;$}}1
    {\\hline}{{\rule{\linewidth}{0.5pt}}}1
%
}[keywords,comments,strings]

\lstnewenvironment{coq}{\lstset{language=coq}}{}

% pour inliner dans le texte
\def\coqe{\lstinline[language=coq, basicstyle=\small]}
% pour inliner dans les tableaux / displaymath...
\def\coqes{\lstinline[language=coq, basicstyle=\scriptsize]}