%% LyX 1.3 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[english]{amsbook}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\setlength\parskip{\smallskipamount}
\setlength\parindent{0pt}
\usepackage{amssymb}

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
 \numberwithin{section}{chapter}
 \theoremstyle{plain}    
 \newtheorem{thm}{Theorem}[section]
 \numberwithin{equation}{section} %% Comment out for sequentially-numbered
 \numberwithin{figure}{section} %% Comment out for sequentially-numbered
 \theoremstyle{definition}
 \newtheorem*{defn*}{Définition}
 \theoremstyle{definition}
  \newtheorem*{example*}{Exemple}
 \theoremstyle{definition}
  \newtheorem{problem}[thm]{Problem}
 \theoremstyle{plain}    
 \newtheorem*{thm*}{Théorème} 
 \theoremstyle{plain}    
 \newtheorem*{conjecture*}{Conjecture} 
 \theoremstyle{definition}
  \newtheorem{xca}{Exercice}
 \theoremstyle{remark}
 \newtheorem*{rem*}{Remarque}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathbb{C}}
\usepackage{hyperref}

\usepackage[francais,american]{babel}
\makeatother
\begin{document}

\newcommand{\Imp}{\textrm{ }\rightarrow\textrm{ }}

\newcommand{\Equiv}{\textrm{ }\Leftrightarrow\textrm{ }}
 
\newcommand{\s}{\textrm{ }}

\newcommand{\E}[1]{(\exists#1 )\textrm{ }}



\newcommand{\A}[1]{(\forall#1 )\textrm{ }}



\chapter{Proof techniques (section 2.1)}


\section{Theorems and Informal proofs}

What we have seen so far:

\begin{description}
\item [Argument]$P_{1}\wedge\cdots\wedge P_{n}\Imp Q$
\item [Syntax]how it's written
\item [Semantic]meaning in a given interpretation
\item [Valid~argument]~


True for all interpretations

True because of its very structure

\end{description}
Proofs of valid argument are purely based on syntactical rewriting
rules.

Only arguments that are true for all interpretations can be proved.


\subsection{Theorems}

We are now interested to work in a particular subject (say integer
arithmetic).

\begin{defn*}
A \emph{theorem} is an argument that is valid in this particular subject.
\end{defn*}
\begin{example*}
If $x$ is even and $y$ is even then $xy$ is even.

$E(x)$: $x$ is even

$\A{x}\A{y}[E(x)\wedge E(y)\Imp E(xy)]$
\end{example*}
This argument is true in this context, but not universally true.

How to prove it ?

Implicitly, we add new hypothesis which reflects basic facts of this
subject.

For example, we add the following hypothesis:

\begin{itemize}
\item $x$ is even if and only if there exists $y$ such that $x=2y$:\[
\A{x}[P(x)\s\leftrightarrow\s\E{y}x=2y]\]

\end{itemize}
Using those new hypothesis, it's now possible to write a formal logic
proof of the theorem. 

See \cite[Example 4 p.~87]{Gersting.MSCS}


\subsection{Formal and informal proofs:}

Remember that the goal of a proof is to be read by humans (in particular
yourself) in order to convince those humans.

The formal proof above is convincing in the sense that you can check
that all the steps are valid. However, it's very difficult to extract
the meaning of the proof:

\begin{itemize}
\item Why does it work ?
\item How could I reuse it for a similar problem ?
\end{itemize}
The problem is that the keys of the proofs are buried under layers
of insignificant details.

So, starting from now, we will write \emph{informal proofs}:

\begin{defn*}
An \emph{informal proof} is a narrative descriptions, of the ideas
and of the important steps of the proof, without extraneous details.
\end{defn*}
\begin{example*}
A proof of the theorem above could be written as follow:
\begin{proof}
Let $x$ and $y$ be two even integers. We can take $n$ and $m$
such that $x=2n$ and $y=2m$. 

Then, $xy=2(2nm)$. Since $2nm$ is an integer, $xy$ is an even number.
\end{proof}
Let see which details we omitted:
\end{example*}
\begin{enumerate}
\item Let $x$ and $y$ be two even integers.


Implicit universal instantiation

\item We can take $n$ and $m$ such that $x=2n$ and $y=2m$.


Implicit universal instantiation for $x$ and $y$ of the definition
of an even number

Implicit existential instantiation for $n$ and $m$

\item Then, $xy=2(2nm)$


Implicit use of rules of arithmetic

\item Since $2nm$ is an integer, $xy$ is an even number:


Implicit universal instantiation of the definition of an even number

Implicit universal generalization to get the final result

\end{enumerate}
\begin{problem}
Which details can we omit, and which not ?
\end{problem}
A reader will be convinced by the proof if he can check that he could
translate each step of the proof into one or several steps of a formal
proof.

So, this all depends on WHO reads the proof!

You should not write your proof for your instructor, but for yourself,
and for everybody else in the class.

A good rule of thumb is to imagine yourself rereading the proof in
a few month, and to check that even then, you could possibly translate
the proof into a formal one.

The difference between formal and informal proofs is very similar
to the difference between assembly and, say, C++ or Java. A C++ program
is not usable by itself. It's usable because it's possible to translate
it into assembly language.

However, there does not exists, and most likely will never exists,
a compiler that transforms informal proofs into formal proofs. English
is much to rich a language for this.


\subsection{Formal and informal theorems:}

Most of the time, we also won't write theorems as a formal argument,
but rather with an English sentence that could be translated into
a formal argument:

\begin{thm*}
Let $x$ and $y$ be two integers. {[}Some definitions: interpretation{]}

Assume x and y are even. {[}Some hypothesis: $P_{1}\wedge\cdots\wedge P_{n}${]}

Then, $xy$ is even. {[}Consequent: $Q${]}
\end{thm*}

\subsection{To Prove or not to prove}

In textbooks, you can be asked: prove that ...

\begin{itemize}
\item you know in advance it's true;
\item you just have to figure out how to prove it.
\end{itemize}
Usually, in real life, you first have to find what to prove.

\begin{itemize}
\item you don't even know in advance if it's true.
\end{itemize}
Two jobs:

\begin{itemize}
\item Find the good questions
\item Prove or disprove those questions
\end{itemize}
\begin{defn*}
A \emph{conjecture} is a statement that you guess is true, but that
you have not proved or disproved yet.
\end{defn*}
Classical steps:

\begin{enumerate}
\item Explore some examples
\item Try to see some pattern emerging
\item Formulate a conjecture
\item Try to prove (or disprove it)
\end{enumerate}
Steps 1-3 are inductive reasoning, whereas step 4 is deductive reasoning.

Finding the good questions is as important as solving them !

\begin{example*}
Fermat's conjecture.
\end{example*}
%


\subsection{Some {}``research'' around the factorial}

\begin{defn*}
Let $n$ be an integer. The factorial of $n$ is the number $n!:=n(n-1)\cdots1$.

For example, $1!=1$ and $4!=\dot{4}\cdot3\cdot2\cdot1=24$.
\end{defn*}
\begin{problem}
How big is $n!$ ?
\end{problem}

\section{Proof techniques}

We want to prove some argument of the form $P\Imp Q$.


\subsection{Disproof by counter example}

\begin{conjecture*}
If $n$ is a positive integer, then $n!<n^{3}$.
\end{conjecture*}

\subsection{Direct proof}

\begin{defn*}
\emph{Direct proof}
\begin{enumerate}
\item \emph{Assume} $P$
\item Deduce $Q$
\end{enumerate}
\end{defn*}
\begin{example*}
Prove that if x and y are even, then $xy$ is even.
\end{example*}
\begin{xca}
Prove that if x and y are even, then $x+y$ is even.
\end{xca}

\subsection{Proof by contraposition}

\begin{example*}
Prove that if $n^{2}$ is odd, then $n$ is odd.
\end{example*}
Hint: prove instead that if n is even, then n\textasciicircum{}2 is
even.

\begin{defn*}
\emph{Proof by contraposition:}
\begin{enumerate}
\item Assume $Q'$ (the consequent is false)
\item Prove $P'$ (the antecedent is also false)
\end{enumerate}
\end{defn*}
This technique relies on the fact that $P\Imp Q$ is equivalent to
$Q'\Imp P'$.

\begin{xca}
Prove that $xy$ is odd if and only if $x$ and $y$ are odd.
\end{xca}

\subsection{Exhaustive proof}

\begin{problem}
Can a proof by example be valid ?
\end{problem}
%

%

%

%

%

%%

Yes, if there is a finite number of cases to be treated.

\begin{example*}
Propositional logic formula (the truth table is finite)
\end{example*}
\begin{defn*}
\emph{Proof by exhaustion} means that all cases have been exhausted.

(and so are you \ldots{}).
\end{defn*}
\begin{example*}
Drawing a figure without lifting the pencil and without retracing
a line.
\end{example*}

\subsection{Some {}``research'' around rational numbers }

\begin{defn*}
A number $x$ is \emph{rational} if it can be written as $\frac{p}{q}$,
where $p$ and $q$ are integers.
\end{defn*}
\begin{example*}
$5,$ $\frac{-7}{5}$, $\frac{1}{-3}$, $\frac{14}{4}$, $\frac{7}{2}$,
\ldots{} are rational.
\end{example*}
\begin{problem}
Properties of rational numbers ?
\end{problem}
%

%

%

%

%

%

%

%

%

%

%%

\begin{rem*}
If $x$ is rational, it's always possible to choose $p$ and $q$
so that:
\begin{itemize}
\item $q$ is positive
\item $p$ and $q$ are \emph{relatively prime}


I.e., the biggest common divisor of $p$ and $q$ is $1$.

\end{itemize}
\end{rem*}
%

%

%%

\begin{problem}
Are all numbers rational ?
\end{problem}
%

\begin{problem}
Assume $x$ and $y$ are rational.
\begin{enumerate}
\item Is $x+y$ rational ?
\item Is $xy$ rational ?
\item Is $\frac{x}{y}$ rational ?
\end{enumerate}
\end{problem}
%

\begin{problem}
Is the square root of an integer a rational number ?
\end{problem}
%

\begin{problem}
Prove that the square root of $2$ is irrational.
\end{problem}

\subsection{Proof by contradiction}

\begin{thm*}
The square root of $2$ is irrational.
\end{thm*}
\begin{proof}
Let's assume the square root of $2$ is rational.

Let $p$ and $q$ be two integers such that $\sqrt{2}=\frac{p}{q}$
and $p$ and $q$ are relatively prime.

Then, we have $2=\left(\frac{p}{q}\right)^{2}$, and so $2q^{2}=p^{2}$.

Therefore $p^{2}$ is even, and we have seen that this implies that
$p$ is also even.

Let $k$ be the integer such that $p=2k$.

Then, we have $2q^{2}=p^{2}=\left(2k\right)^{2}=4k^{2}$, and so $q^{2}=2k^{2}$.

It follows that $q^{2}$ is even, and so $q$ is also even.

Conclusion: $p$ and $q$ are both even.

That's a contradiction, since $p$ and $q$ are relatively prime!
\end{proof}
\begin{defn*}
\emph{Proof by contradiction}
\begin{enumerate}
\item Assume the contrary
\item Deduce a contradiction
\end{enumerate}
\end{defn*}
This technique relies on the fact that:

\begin{enumerate}
\item $Q\wedge Q'$ is always false
\item if $P\rightarrow0$ is true, then $P$ is false.
\end{enumerate}

\subsection{Serendipity}

\begin{example*}
The chess board problem.
\end{example*}

\section{Summary}

\vspace{0.3cm}
\begin{center}\begin{tabular}{|c|c|c|}
\hline 
Goal&
Technique&
Name\tabularnewline
\hline
\hline 
$P\Imp Q$&
Assume $P$ ; deduce $Q$.&
Direct proof/Deduction method\tabularnewline
\hline 
$P'\rightarrow Q'$&
Prove $Q\rightarrow P$.&
Proof by contraposition\tabularnewline
\hline 
$Q'$&
Assume $Q$; deduce a contradiction.&
Proof by contradiction\tabularnewline
\hline 
$P\leftrightarrow Q$&
Prove $P\rightarrow Q$; prove $Q\rightarrow P$.&
\tabularnewline
\hline 
$P\wedge Q$&
Prove $P$ ; prove $Q$.&
\tabularnewline
\hline 
$P\vee Q$&
Prove $P'\rightarrow Q$&
\tabularnewline
\hline 
$(P_{1}\vee P_{2})\rightarrow Q$&
Prove $P_{1}\rightarrow Q$; prove $P_{2}\rightarrow Q$&
Proof by cases\tabularnewline
\hline 
$\A{x}Q(x)$&
Let $x$; prove $Q(x)$&
ui / ug\tabularnewline
\hline 
$\E{x}Q(x)$&
Construct $a$ such that $Q(a)$&
eg\tabularnewline
\hline 
&
Be smart&
Serendipity\tabularnewline
\hline
\end{tabular}\end{center}\vspace{0.3cm}

\end{document}
