Quelle  root.tex

\documentclass[11pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{geometry}
\usepackage{isabelle,isabellesym}
\usepackage{amsmath, amssymb}
\usepackage{mathpartir}
\usepackage{newunicodechar}
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\newunicodechar{∀}{\ensuremath\forall}
\newunicodechar{∃}{\ensuremath\exists}
\newunicodechar{≠}{\ensuremath\neq}
\newunicodechar{–}{--}
\newunicodechar{…}{\dots}
\newunicodechar{⋀}{\ensuremath\bigwedge}
\newunicodechar{⟹}{\ensuremath\Longrightarrow}
\newunicodechar{∧}{\ensuremath\land}

\begin{document}

\title{Wlog -- Without Loss of Generality\thanks{Supported by the ERC consolidator grant CerQuS (819317), the PRG team grant “Secure Quantum Technology” (PRG946) from the Estonian Research Council, and the Estonian Cluster of Excellence ``Foundations of the Universe'' (TK202).}}
\author{Dominique Unruh\\
 \footnotesize RWTH Aachen, University of Tartu}
\maketitle

\begin{abstract}
  We introduce a new command \texttt{wlog} in Isabelle/HOL that allows us to (soundly) assume
  facts without loss of generality inside a proof.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

\section{Introduction}

We introduce a command \texttt{wlog} for assuming facts without loss of generality inside a proof in Isabelle/HOL.
The \texttt{wlog} command makes sure this is sound by requiring us to prove that the assumption is indeed made without loss of generality.

A simple example is the following:
\begin{verbatim}
lemma card_nth_roots_strengthened:
  assumes "c ≠ 0"
  shows   "card {z::complex. z ^ n = c} = n"
proof -
  wlog n_pos: "n > 0"
    using negation by (simp add: infinite_UNIV_char_0)
  have "card {z. z ^ n = c} = card {z::complex. z ^ n = 1}"
    by (rule sym, rule bij_betw_same_card, rule bij_betw_nth_root_unity) fact+
  also have "… = n" by (rule card_roots_unity_eq) fact+
  finally show ?thesis .
qed
\end{verbatim}

This proof is exactly like the proof of \verb|Complex.card_nth_roots| in the Isabelle/HOL library,
except that the latter uses the additional assumption \texttt{n > 0} in the theorem statement.
We omit this assumption and instead state that it can be assumed without loss of generality.
(\verb|wlog n_pos: "n > 0"|)
The next line then shows that this can be assumed without loss of generality.%
\footnote{The argument is basically:
  If $\lnot(n>0)$, then $n=0$ (since $n$ is a natural number).
  Then $\{z.\ z^n = c\}$ is infinite, and for infinite sets, the cardinality \texttt{card}
  is defined to be $0$ in Isabelle/HOL.
  Thus that cardinality is $0$.
  This reasoning is done almost automatically by Isabelle.}

Of course, we could have shown this theorem also, e.g., by doing a case distinction on whether $n=0$.
But this would additionally clutter the proof; the case $n=0$ is almost trivial, yet in the proof it will be a separate case on the same level as the main proof.
So doing a \texttt{wlog} improves readability here by allowing us to focus on the important parts of the proof
and reducing boilerplate.

In other cases, a \texttt{wlog} argument cannot easily be done as a case distinction.
E.g., if we say that we can assume w.l.o.g.~that $a\geq b$ because the case $a < b$ can be easily reduced to the $a\geq b$ case.
(This is common in symmetric situations.)
We give an example of this in the proof of lemma \verb|schur_ineq| below.

\bigskip

The full syntax of the \texttt{wlog} command is roughly as follows:
\begin{verbatim}
wlog wlogassmname: ‹wlogassm1› ‹wlogassm2›
     goal G  generalizing x y z  keeping fact1 fact2
  [… your proof …]
\end{verbatim}
(The defaults being: The goal is \texttt{?thesis}.
And empty lists of variables and facts for \texttt{generalizing} and \texttt{keeping}.)

This means that we assume w.l.o.g.~that the facts \texttt{wlogassm1} and \texttt{wlogassm2} hold
when proving the goal \texttt{G}.
We say that the assumptions \texttt{fact1} and \texttt{fact2} (made prior to the \texttt{wlog} command)
should still be available afterwards.
(If we include less assumptions here, the justification for the \texttt{wlog} command becomes easier.)
And we wish to generalize the variables \texttt{x, y, z};
that is, inside the justification of the \texttt{wlog}, we want to be allowed to use the theorem that we are proving
for other values of \texttt{x, y, z} (needed, e.g., in symmetry arguments).
And \texttt{[… your proof …]} is a proof of the fact that we can make the w.l.o.g.-assumption,
either as an apply-script or as an Isar subproof.

\bigskip

The \texttt{wlog} command is realized by translation to existing Isar commands. The above translates roughly to:
\begin{verbatim}
  presume hypothesis:
    ‹⋀x y z. wlogassm ⟹ fact1 ⟹ fact2 ⟹ G›
  have ‹G› if negation: ‹¬ (wlogassm1 ∧ wlogassm2)›
    [… your proof …]
  then show ‹G›
    [… autogenerated proof …]
next
  fix x y z
  assume fact1: ‹fact1› and fact2: ‹fact2›
  assume wlogassmname: ‹wlogassm1› ‹wlogassm2›
\end{verbatim}
(There are more steps and additional convenience definitions, but this is the main part.)

More examples of how to use \texttt{wlog} are given in the theory \texttt{Wlog\_Examples} below.

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: