\documentclass[12pt]{amsart}
\usepackage{amsmath}
\usepackage[portuges]{babel}
\usepackage{enumerate}
% uncomment next line to get pdf files with hyperlinks
%\usepackage[pdftex,bookmarks=true]{hyperref}

\input{deflogic.tex}
\input{defport}
\usepackage{epsf}



\def\stdin{\emph{stdin}}
\def\stdout{\emph{stdout}}
\def\natnum{\textbf{Natnum}}
\title{Indu\c c\~ao Matem\'atica}

\author{Raul H.C. Lopes}

\begin{document}

\maketitle

\section{Indu\c c\~ao matem\'atica}

\subsection{Conjunto indutivamente definido}

Considere a seguinte defini\c c\~ao, encontrada em \cite{apostol:calculus}.

\begin{em}\textbf{ Defini\c c\~ao de um conjunto indutivo.}
Um conjunto de n\'umeros reais \'e chamado de \text{conjunto indutivo} se ele
tem as seguintes propriedades:
\begin{enumerate}
  \item O n\'umero $1$ pertence ao conjunto.
  \item Para todo $x$ pertencente ao conjunto, o n\'umero $x+1$ tamb\'em pertence
ao conjunto.
\end{enumerate}
  
\end{em}

Essa defini\c c\~ao apresenta um \emph{m\'etodo para computar} n\'umeros reais
a partir de um elemento inicial: o n\'umero $1$. Note que essa defini\c c\~ao 
limita-se a estabelecer como encontrar elementos de \textbf{um} conjunto 
indutivo de reais (os inteiros positivos): 
ela nem tenta cobrir todo o conjunto de reais e nem
mesmo determinar exatamente todos os elementos do conjunto indutivo em quest\~ao.

Veja agora a seguinte defini\c c\~ao retirada da mesma fonte.

\begin{em}\textbf{Defini\c c\~ao de inteiros positivos.}
  Um n\'umero real \'e chamado inteiro positivo se ele pertence a todo conjunto 
indutivo.
\end{em}

A defini\c c\~ao acima, claramente referindo-se e complementando a anterior,
tentar definir exatamente o conjunto dos inteiros positivos estabelecendo 
que ele \'e a interse\c c\~ao de todos os conjuntos poss\'{\i}veis de se obter, usando
a primeira defini\c c\~ao.

Al\'em de estabelecer um ``m\'etodo para enumerar'' todos os elementos do 
conjunto de inteiros positivos, essas duas defini\c c\~oes\ sugerem:
\begin{enumerate}[i]
  \item um m\'etodo para testar se qualquer $z$ \'e um inteiro postivo: tal teste consistiria em verificar
se $z$ \'e o elemento inicial do conjunto definido ou se ele pode ser reescrito 
como $x+1$, para algum $x$ pertencente ao conjunto definido. 
  \item um m\'etodo de prova de propriedades sobre conjuntos de inteiros positivos. Para provar a
propriedade $P\,n$, para todo $n$ inteiro positivo basta:
\begin{enumerate}[1]
  \item Provar que a propriedade $P$ \'e v\'alida  para o elemento inicial do conjunto de interesse;
  \item Provar que $P\,k$ implica $P(k+1)$, ou seja, que, para
qualquer elemento do conjunto em questao, se $P$ vale para esse elemento, ent\~ao $P$ vale
para o seu sucessor.
\end{enumerate}
\end{enumerate}

\begin{eg}\label{eg:pa}
Provar que para todo $n$
$$\bnd{+}{i}{\lelt1in}{i} = \frac{n(n-1)}2$$
\proofbeg

Aplicar o m\'etodo de prova acima delineado demanda:
\begin{itemize}
\item Identificar a propriedade a provar. Seja $P$ uma fun\c c\~ao que mapeia um inteiro para
booleanos (conjunto $\{True,False\}$), definido por
$$ P = \lambda n. \bnd{+}{i}{\lelt1in}{i} = \frac{n(n-1)}2$$

Dada esta defini\c c\~ao, a propriedade que se deseja provar seria
$$\bnd{\land}n{}{P\,n}$$

\item Garantir que a propriedade trata de conjuntos indutivos, no caso inteiros positivos. Isto
demanda ser mais preciso na defini\c c\~ao do $n$: assumir que o objetivo \'e provar $P$ para todo
inteiro prositivo. Logo, $P$ assume a seguinte defini\c c\~ao:
$$ P = \lambda n. \bnd{+}i{i \in \Pos\land\lelt1in}{i} = \frac{n(n-1)}2$$

O objetivo agora \'e provar:
$$\bnd{\land}n{n\in\Pos}{P\,n}$$

\item Provar que a nova propriedade vale para $1$.

\begin{align*}
P 1  =& (\bnd +{i}{i\in\Pos\land\lelt1i1}{i} = \frac{1(1-1)}2) \\
& = \jsttxt{\EmptyRangeAx} \\
& 0 = \frac{1(1-1)}2 \\
& = \jsttxt{\arithmetic} \\
& 0 = 0\\
& = \jstop{\bndall x{}{x=x}} \\
& \ltrue
\end{align*}

Observa\c c\~oes importantes sobre o trecho de prova acima:
\begin{itemize}
\item Por \emph{transitividade da igualdade}, o trecho mostra que $P 1 = \ltrue$, o que diz em
ess\^encia que $P 1$ \'e verdadeiro.
\item Cada passo de prova \'e um processo de reescrita baseado em algum axioma.
\item A igualdade \'e usada como equival\^encia l\'ogica: duas express\~oes com valores booleanos 
iguais s\~ao logicamente equivalentes.
\end{itemize}

\item Provar que, quando $P\,k$ \'e verdadeiro, onde $k\in\Pos$, ent\~ao $P(k+1)$ tamb\'em \'e
verdadeiro. Reescrevendo $P(k+1)$:

$$P(k+1) = (\bndsum{i}{i\in\Pos\land\lelt1i{k+1}}{i} = \frac{(k+1)(k+1-1)}2)$$  

Note que assumir  $P\,k$ como verdadeiro, consiste em assumir

$$\bndsum{i}{i\in\Pos\land\lelt1i{k}}{i} = \frac{k(k-1)}2$$


\begin{align*}
\quad & \bnd{+}{i}{i\in\Pos\land\lelt1i{k+1}}{i}\\
 =& \jsttxt{\SumRecDef} \\
 & \bnd+{i}{i\in\Pos\land\lelt1i{k}}{i}+k \\
 =& \jst{Assumindo}{P\,k}\\
 & \frac{k(k-1)}2 + k\\
 =& \jsttxt{\arithmetic}\\
 & \frac{k(k+1)}2
\end{align*}
\end{itemize}
Observa\c c\~oes importantes sobre o trecho de prova acima:
\begin{itemize}
\item Neste trecho de prova, foi feita a op\c c\~ao de se reescrever o lado esquerdo da igualdade 
que $P(k+1)$ representa at\'e encontrar o lado direito dessa mesma igualdade.
\item Cada passo da prova foi novamente um passo de reescrever alguma f\'ormula usando um axioma ou
uma hip\'otese previamente apressentados.
\item A transitividade da igualdade novamente garante a consist\^encia da prova.
\item Voc\^e \'e livre para escolher seu estilo de prova, mas cada passo deve ser logicamente
justificado.
\end{itemize}

\proofend
\end{eg}

O princ\'{\i}pio de prova delineado acima e usado no \refeg{pa} \'e formalizado como
\emph{Princ\'{\i}pio da Indu\c c\~ao Matem\'atica.}

\begin{definition}\label{def:WMI}
\textbf{Princ\'{\i}pio da Indu\c c\~ao Matem\'atica sobre \Nat}
$$\bndall{n}{n\in\Nat}{P\,n} = P\,0 \land \bndall{k}{k\in\Nat}{P\,k\limp P(k+1)}$$
\end{definition}

\begin{ex}\label{ex:pmifrk}
Prove que 
$$\bndall{n0}{n0\Nat}{\bndall{n}{n\in\Nat n0\leq n}{P\,n} = P\,n_0 \land \bndall{k}{k\in\Nat\land k\leq n_0}{P\,k\limp P(k+1)}}$$
\end{ex}


\begin{eg}
Prove que $$\bndall n{n\in\Nat\land n\geq 4}{n^2 \leq 2^n}$$
   

   \proofbeg 
   \begin{align*}
    & \bndall n{n\in\Nat\land n\geq 4}{n^2 \leq 2^n}\\
    =& \jsttxt{\refex{pmifrk}}\\
    &(4^2\leq 2^4) \land \bndall k{k\in\Nat\land k\geq 4}{k^2 \leq 2^k\limp (k+1)^2\leq 2^{k+1}}\\
    \text\proofof&{4^2\leq 2^4}\\
    & 4^2\leq2^4\\
    =& \jsttxt\arithmetic\\
    &\ltrue\\
    \text\proofof&{\bndall k{k\in\Nat\land k\geq 4}{k^2 \leq 2^k\limp (k+1)^2\leq 2^{k+1}}}\\
    \txtIH&{k_0\in\Nat, k_0\geq 4, P\,k = k_0^2\leq2^{k_0}}\\
    \text\proofof&{(k_0+1)^2\leq2^{k_0+1}}\\
    & (k_0+1)^2\\
    =&\jsttxt\arithmetic\\
    &k_0^2+(2k_0+1)\\
    \leq&\jstop{P\,k}\\
    &2^{k_0}+(2k_0+1)\\
    \leq&\jst{when}{k_0\geq3, 2k_0+1\leq k_0^2}\\
    &2^{k_0}+k_0^2\\
    \leq&\jstop{P\,k}\\
    &2^{k_0}+2^{k_0}\\
    =&\jsttxt\arithmetic\\
    &2^{k_0+1}
   \end{align*}
  
   \proofend
\end{eg}


\begin{ex}
 Prove por indu\c c\~ao:
  \begin{enumerate}
    \item $ \bndsum{i}{\lele{1}{i}{n}} i = n(n+1)/2$

    \item $ \bndsum{i}{\lelt{0}{i}{n}}{2^i} = 2^n-1$

    \item $ \bndsum{i}{\lelt{0}{i}{n}}{3^i} = (3^n-1)/2$

    \item $ \bndsum{i}{\lele{1}{i}{n}}{i^2} = n(n+1)(2n+1)/6$

    \item $ \bndsum{i}{\lele{0}{i}{n}}{i.2^i} = (n-1).2^{n+1}+2$

    \item $ \bndsum{i}{\lele{0}{i}{n}}{(2i+1)^2} = (n+1) (2n+1)(2n+3)/3$

    \item $ \bndsum{i}{\lele{0}{i}{n}}{i(i+1)(i+2)} = n(n+1)(n+2)(n+3)/4$

    \item $ \bndall{n,a}{n\geq 1 \land a\neq 1}{\bndsum{i}{\lelt{0}{i}{n}}{a^i} = (1-a^n)/(1-a)}$
    \item $ \bndall{n}{n\geq 1}{\bndsum{i}{\lele{1}{i}{n}}{1/(i.(i+1)}) = n/(n+1)}$
    \item $ \bndall{n}{n\geq 3}{n+1 < 2^n}$
    \item $ \bndall{n}{n\geq 4}{n^2 \leq 2^n}$
    \item $ \bndall{n}{n\geq 7}{3^n < n!}$
  
  \end{enumerate}
\end{ex}

\subsection{Ouro de tolo?}

J\'a d\'a para conjecturar: o m\'etodo de prova acima, o chamado \emph{Princ\'{\i}pio
da Indu\c c\~ao}, deve ser aplic\'avel \`a prova de propriedades  de
 qualquer conjunto cont\'avel. Ent\~ao...
Dado  o conjunto de humanos, que nem mesmo \'e infinito, ficamos tentados 
a realizar aplica\c c\~oes\ mais interessantes.
\begin{ex}
Prove que todas as garotas loiras t\^em olhos claros.

\end{ex}

Para obter a prova acima, voc\^e pode:
\begin{enumerate}
  \item Esquecer o \PI\ e partir para o experimento. Que tal na sua turma
de \emph{Estruturas de Dados}? \'E claro que isso demanda definir:
\begin{enumerate}[i]
  \item O que s\~ao garotas? \textsl{Ok! Isso pode n\~ao ser politicamente correto!}
  \item O que s\~ao olhos claros?
\end{enumerate}
  \item Tentar \PI, mas quem s\~ao $P\,k$ e $P(k+1)$? Ali\'as, esse \'e o ponto 
fundamental de toda a prova por indu\c c\~ao: indentificar $P\,k$, a \emph{hip\'otese
de indu\c c\~ao}, e realizar o \emph{passo indutivo} para obter $P(k+1)$.
\end{enumerate}

Ok! De volta ao reino de \Nat...

Veja o seguinte ``teorema''e sua ``prova'', retirados de \cite{DEK:TAoCP-I}.
\begin{etheo}
  Dados inteiros positivos $a$ e $n$, $a^{n-1} = 1$.

\eproof
\begin{enumerate}[1]
  \item Para $n=1$, $a^{1-1} = a^0 = 1$.
  \item Para $n=k+1$, 
          \[a^{(k+1)-1}=a^k=a^{k-1}\cdot a = \frac{a^{k-1}\cdot a^{k-1} }{a^{(k-2)}} = \frac{1\cdot 1}{1} = 1\]
\end{enumerate}
\end{etheo}

O que est\'a errado? Talvez o fato de que para se obter a prova para $n=k+1$,
foram usados como hip\'oteses o fato de que a assertiva seria v\'alida 
para $n=k$ e $n=k-1$? N\~ao! Na verdade, como mostrado na pr\'oxima se\c c\~ao, esse
\'e um racioc\'{\i}nio v\'alido.


\subsection{Indu\c c\~ao para \wfs s}
Considere a seguinte s\'erie, conhecida como s\'erie de Fibonacci\footnote{Veja em
\cite{gs:discretemaths} e \cite{DEK:TAoCP-I} hist\'oria, fatos e folclore
em torno do n\'umeros de Fibonacci.}.

\begin{definition}\label{def:fibs}
A s\'erie de Fibonacci \'e o conjunto indutivo dos $F_i$, definidos por: 
\begin{align*}
  F_0 = & 0 \\
  F_1 = & 1 \\
  F_n = & F_{n-1}+F_{n-2}, \text{ para } n>1 
\end{align*}
\end{definition}


\begin{eg}\label{eg:fibLTTwoExpN}

Prove que $$\bndall{n}{n\in\Nat}{F_n<2^n}$$
\proofbeg
\begin{align*}
& \bndall{n}{n\in\Nat}{F_n<2^n}\\
=&\jsttxt{\refdef{WMI}}\\
&F_0 < 2^0 \land \bndall{k}{k\in\Nat}{F_k < 2^k \limp F_{k+1} < 2^{k+1}}\\
\text\proofof&F_0<2^0\\
&F_0 < 2_0\\
=&\jsttxt{F (axioma 0) e \arithmetic}\\
&0<1\\
=\\
&\ltrue\\
\text\proofof&\bndall{k}{k\in\Nat}{F_k < 2^k \limp F_{k+1} < 2^{k+1}}\\
\txtIH&k\in\Nat,P\,k=F_k<2^k\\
&F_{k+1} < 2^{k+1}\\
=&\jsttxt{F (axioma 2)}\\
&F_k+F_{k-1}\\
&< \jstop{P\,k}\\
&2^k+F_{k-1}\\
&\jst{Nenhuma hip\'otese sobre}{F_{k-1}}
\end{align*}

\end{eg}
O \refeg{fibLTTwoExpN} n\~ao pode ser completado porque n\~ao h\'a hip\'oteses sobre o valor de
$F_{k-1}$. A seguinte variante do princ\'{\i}pio da indu\c c\~ao poderia ajudar, se usada com
cuidado.

\begin{definition}\label{def:SMI}
\textbf{Princ\'{\i}pio da Indu\c c\~ao Forte.} 
$$\bndall{n}{n\in\Nat}{P\,n} = %
\bndall{n}{n\in\Nat}{\bndall{k}{k\in\Nat\land k < n}{P\,k\limp P\,n}}$$
\end{definition}
O \refeg{fibLTTwoExpN} poderia agora ser completado desde que se \refdef{SMI} para assumir que
$F_{k-1} < 2^{k-1}$. Mas, seguindo o mesmo racioc\'{\i}nio, a seguinte prova tamb\'em seria
trivialmente obtida.

\begin{eg}\label{eg:evenFib}
Use a \refdef{SMI} e o racioc\'{\i}nio do \refeg{fibLTTwoExpN} para provar que todos os n\'umeros da
s\'erie de Fibonacci s\~ao pares.
\end{eg}
Humm... Mas, $1,3,5$ todos est\~ao na s\'erie de Fibonacci e s\~ao \'{\i}mpares. 
Bem, talvez sejam apenas uns poucos, uma minoria. Basta disfar\c car e fingir
que n\~ao est\~ao l\'a. O teorema seria ``aproximadamente v\'alido.'' 
Ou... ``esquece tudo: essa tal de \CC\ n\~ao funciona porque
o fundamento matem\'atico n\~ao \'e confi\'avel.'' 
Ou\dots 
O que est\'a errado? A s\'erie de Fibonacci \'e um conjunto indutivo com dois \emph{elementos
iniciais}: $F_0 = 0$ e $F_1 = 1$. O chamado \emph{caso base} da prova por indu\c c\~ao deve 
demandar a prova de que a propriedade em quest\~ao vale para esses dois elementos.
No \refeg{evenFib}, no \emph{caso base}, demanda-se provar que $F_1$ \'e par. A prova falha nesse
ponto.

Considere o seguinte problema.\footnote{Retirado das notas de aula de 
Tom Leighton, do curso de Mathematics for Computer Science, MIT, Setembro/97.}

\begin{ex}
\label{leighton:stamps}
  Para qualquer n\'umero $n\ge 8$, \'e poss\'{\i}vel obter a partir de uma soma de 
fatores todos iguais a $3$ ou $5$.
\end{ex}

\begin{ex}
Prove que os princ\'{\i}pios da \refdef{WMI} e \refdef{SMI} s\~ao equivalentes
\end{ex}



\subsection{Classe indutiva}

\begin{definition}\label{def:inductiveClass}
  $\mathfrak{X}$ \'e uma classe indutiva se:
  \begin{enumerate}[(i)]
    \item seus elementos s\~ao gerados a partir de uma das seguintes opera\c c\~oes:
    \begin{enumerate}[1.]
    \item existe uma especifica\c c\~ao inicial $\mathcal{B}$ 
de um conjunto de elementos que
pertencem a $\mathfrak{X}$ (chamados elementos iniciais);
    \item existe um conjunto $\mathcal{M}$ de opera\c c\~oes\ que aplicadas a elementos 
de $\mathfrak{X}$ produzem novos elementos de $\mathfrak{X}$.
  \end{enumerate}
   \item Todos elemento de $\mathfrak{X}$ pode ser obtido come\c cando com um
ou mais elementos de $\mathcal{B}$ e aplicando a cada passo uma opera\c c\~ao de
$\mathcal{M}$ a elementos obtidos em algum passo anterior ou obtidos de  
$\mathcal{B}$.
  \end{enumerate}

� comum dizer que $\mathcal{X}$ \'e a menor classe (ou o fecho universial da classe), 
cujos elementos iniciais s\~ao
dados por $\mathcal{B}$ e que tem novos elementos constru\'{\i}dos por aplica\c c\~oes\
repetidas de $\mathcal{M}$. \footnote{Veja cap\'{\i}tulos iniciais \cite{curry:foundations} sobre 
conceitos de  classe indutiva, algoritmo, e quest�es definidas e 
semi-definidas.}
\end{definition}

\begin{eg}
\label{class:fibs}
  A s\'erie de Fibonacci \'e uma classe indutiva, cujos elementos iniciais s\~ao
$F_0 = $ e $F_1 = 1$. Qualquer $F_n$, para $n>1$, \'e obtido da soma de
$F_{n-1}$ e $F_{n_2}$.
\end{eg}

O \PI\ fica mais claro quando aplicado ao conceito de classe indutiva.
\begin{definition}
  Uma propriedade $P$ \'e v\'alida para todos os elementos de uma classe indutiva
$\mathfrak{X}$ se:
  \begin{enumerate}[(i)]
    \item $P$ \'e v\'alida para todos os elementos iniciais de $\mathfrak{X}$ ($P$
\'e v\'alida para os elementos gerados por $\mathcal{B}$).
   \item Qualquer opera\c c\~ao $\mathcal{M}$ (que permite gerar elementos
de $\mathfrak{X}$ a partir de elementos j\'a conhecidos) preserva a validade de
$P$.
  \end{enumerate}
\end{definition}

\begin{eg}
  Uma propriedade \'e v\'alida para classe da s\'erie de Fibonacci, introduzida
na \refdef{fibs}, se ela for v\'alida para seus elementos iniciais: $0$ e
$1$. Logo, a propriedade de que todos os elementos da classe s\~ao pares,
do \refeg{evenFib}, n\~ao \'e v\'alida.
\end{eg}


\begin{ex}
  Reveja sua prova do \refeg{fibLTTwoExpN} \`a luz do conceito de
classe indutiva.
\end{ex}

\begin{ex}\label{ex:fibLimits}

  Seja $\phi = (1+\sqrt{5})/2$. Prove que
  \[ \phi^{n-2} \leq F_n \leq \phi^{n-1} \]
\end{ex}

\section{Well-Founded Sets}

O princ\'{\i}pio da Indu\c c\~ao apresentado na \refdef{SMI} pode ser generalizado para qualquer
conjunto que possa ser caraterizado como \emph{well founded}. Classes indutivas podem ser
caraterizadas a partir do conceito de \emph{well-foundedness}.

\begin{definition}\label{def:minimal}

\textbf{Elemento Minimal.}
Dado um par \pair U\prec, y \'e um elemento minimal de S, denotado por \minimal yU\prec, se
$$y\in S \land \bndall{x}{x\prec y:x\not\in S}.$$
\end{definition}

\begin{definition}\label{def:wfs}
Um conjunto  $U$ \'e dito \emph{well founded} por uma rela\c c\~ao $\prec$, denotado por 
\wff U\prec, quando todo
subconjunto n\~ao vazio de
$U$ tem um elemento minimal.
\end{definition}

\begin{ex}
Defina uma rela\c c\~ao de preced\^encia para a s\'erie de Fibonacci e liste seus elementos
minimais.
\end{ex}

\begin{definition}\label{def:WFSI}

\textbf{Indu\c c\~ao Matem\'atica sobre Well-Founded Sets}.
Dado um par \pair U\prec, tal que \wff U\prec, a sequinte equival\^encia define o princ\'{\i}pio
de prova por indu\c c\~ao para propriedades sobre $U$:
$$\bndall x{x\in U}{P\,x}$$
$$=$$%
$$\bndall x{x\in U}{\bndall y{y\in U\land y\prec u}{P\,y}\limp P\,x}$$
\end{definition}

Note que a \refdef{WFSI} demanda provar $P\,x$ para todo $x \in U$, mas permite assumir como
hip\'otese que 
$P$ vale para todos os elementos que precedem $x$. Isso equivale dizer que essa defini\c c\~ao
demanda provar que $P\,k$ sempre que $k$ \'e um elemento
minimal em \wff U\prec. Isso \'e explicitamente colocado na \refdef{AWFSI}.

\begin{definition}\label{def:AWFSI}

\textbf{Indu\c c\~ao Matem\'atica sobre Well-Founded Sets (alternativa).} 
Dado um par \pair U\prec, tal que \wff U\prec, a sequinte equival\^encia define o princ\'{\i}pio
de prova por indu\c c\~ao para propriedades sobre $U$:
$$\bndall x{x\in U}{P\,x}$$ 
$$=$$
$$\bndall y{\minimal yU\prec}{P\,y}$$
$$\land$$%
$$\bndall x{x\in U\land x\not\in\minset U\prec}{\bndall y{y\in U\land y\prec u}{P\,y}\limp P\,x}$$
\end{definition}

\begin{ex}
Use a \refdef{AWFSI} para provar que $F_n < 2^n$.
\end{ex}

\begin{theo}
  Qualquer $M\subseteq\Nat$, tal que $M$ n\~ao \'e vazio,  tem um elemento m\'{\i}nimo.
  \proofbeg
    Assumindo que $M\subseteq\Nat$ e que $M$ n\~ao tem elemento m\'{\i}nimo, chega-se
\`a contradi\c c\~ao de que $M$ \'e vazio.
    Por \PIF, prova-se que $\bnd{\forall}{n}{n\in\Nat}{n\not\in M}$.
    \begin{enumerate}[(1)]
      \item Para $n=0$, $n\not\in M$ ou $n$ seria m\'{\i}nimo, pois $M\subseteq\Nat$
e $0$ \'e m\'{\i}nimo em $\Nat$.
      \item Assumindo-se que $\bnd{\forall}{k\in\Nat}{\le\le{0}{k}{n}}{k\not\in M}$, conclui-se que $k+1\not\in M$, ou $k+1$ seria m\'{\i}nimo de $M$.

Logo $M$ \'e vazio, ou $M$ tem m\'{\i}nimo.
    \end{enumerate}
  \proofend
\end{theo}

\begin{ex}
Construa a prova do \refex{fibLimits} usando a \refdef{AWFSI}.
\end{ex}


\section{Indu\c c\~ao e computa\c c\~ao}

Tipos de dados  s\~ao representa\c c\~oes\ em alguma linguagem de programa\c c\~ao de
classes indutivas. Na verdade, qualuqer computa\c c\~ao pode ser vista como
a atividade de enumerar os elementos de uma class indutiva.

\begin{ex}
Construa um argumento a favor de ou contra a seguinte afirma\c c\~ao:

\textsl{S\'o \'e computavel o que pode ser definido indutivamente.}

\end{ex}

\begin{ex}
Construa um argumento a favor ou contra de:
\textsl{Nem todas as fun\c c\~oes s\~ao comput\'aveis}
\end{ex}

\begin{eg}
\label{natnums}
Considere a classe \natnum\ como a menor classe que cont\'em:
\begin{enumerate}[(i)]
  \item $Z$, como \'unico elemento inicial;
  \item $(S x)$, quando $x$ j\'a pertence a \natnum.
\end{enumerate}


\end{eg}

\subsection{Admissibilidade de fun\c c\~oes}

Uma representa\c c\~ao em Haskell para a classe \natnum\ seria:

\begin{verbatim}

  data Natnum = Z | (S Natnum)
   deriving (Eq)

\end{verbatim}

Essa defini\c c\~ao cont\'em tr\^es elementos importantes:
\begin{enumerate}
\item Ela introduz $Z$ como  construtor do \'unico objeto inicial (elemento minimal) da classe.
\item Ela introduz um operador $S$ para construir novos elementos da classe a partir de elementos
j\'a existentes.
\item Atrav\'es da cl\'ausula \textbf{deriving (Eq)}, ela introduz extensionalidade que estabelece:
\begin{align*}
&Z = Z\\
&\bndall{n,m}{n,m\in\natnum}{(S(n) = S(m)) = (m = n)} 
\end{align*}

\end{enumerate}

Um exemplo de fun\c c\~ao para adi\c c\~ao de elementos dessa classe seria:

\begin{verbatim}

  itsum m Z = m
  itsum m (S n) = itsum (S m) n

\end{verbatim}

\'E importante entender os par\^ametros dessa defini\c c\~ao como vari\'aveis universalmente
quantificadas. Dessa forma, a defini\c c\~ao de \textbf{itsum} acima estaria estabelencendo que:
\begin{align*}
\bndall{m}{m\in\natnum}{itsum\ m\ Z = m}\\
\bndall{m,n}{m,n\in\natnum}{itsum\ m\ (S n) = itsum\ (S m)\ n}
\end{align*}

A fun\c c\~ao \textbf{itsum} acima definida permite introduzir dois conceitos
importantes:

\begin{enumerate}[1.]
  \item \emph{Admissibilidade da fun\c c\~ao}: a fun\c c\~ao acima ser\'a dita 
admiss\'{\i}vel porque existe uma medida de complexidade dos seus argumentos
que \'e sempre decrescente em qualquer chamada recursiva da mesma. Nessa
fun\c c\~ao, o segundo argumento da chamada recursiva \'e sempre mais simples
que o segundo argumento da chamada que a precede.

Por exemplo, assuma um mapeamento $f:Natnum \rightarrow\Nat$ que associa:
\begin{align*}
  f(m,Z) =& 0\\
  f(m,(S n))  =& f\,n+1  
\end{align*}

Claramente $f$ \'e uma medida de complexidade para os argumentos de chamada
de \textbf{itsum} que decresce a cada chamada recursiva, formando um cadeia
finita decrescente, com m\'{\i}nimo em $(m,Z)$.

 \item Diferentemente da fun\c c\~ao \textbf{recsum} abaixo, \textbf{itsum}
pode ser avaliada por um processo de repeti\c c\~ao  substitui\c c\~oes\ simples da
chamada original pela chamada recursiva.

\end{enumerate}

\begin{verbatim}

  recsum m Z = m
  recsum m (S n) = S(recsum m n) 
 
\end{verbatim}

A computa\c c\~ao de \textbf{recsum} demanda que uma mem\'oria seja mantida
das sucessivas chamadas recursivas para os \textbf{S} sejam adicionados
ao resultado final da chamada n\~ao recursiva.
 
A fun\c c\~ao \textbf{itsub} introduzida abaixo estabelece a a diferen\c ca absoluta de dois
elementos da class \natnum.

\begin{verbatim}
  
  itsub m Z = m
  itsub Z n = Z
  itsub (S m) (S n) = itsub m n

\end{verbatim}

\begin{ex}
Prove que \textbf{itsub} sempre termina.
\end{ex}

\begin{ex}
Prove:
$$\bndall{m,n}{m,n\in\natnum}{itsub\ m\ n = itsub\ n\ m}$$ 
\end{ex}


\begin{ex}
Defina uma fun\c c\~ao \textbf{pred}, que obt\'em o predecessor de um \natnum, e prove que 
\[ itsub m (S n) = pred(itsub m n) \]


Use indu\c c\~ao sobre $n$ (segundo argumento do $(m,n)$ da chamada recursiva.)
No passo indutiva, considere dois casos: quando $m$ \'e \textbf{Z} e quando
$m$ \'e \textbf{(S u)} para algum $u$. 
\end{ex}

\subsection{Generalizando indu\c c\~ao}
\'E importante observar que a medidade complexidade de argumentos de uma
fun\c c\~ao n\~ao precisa se restringir a um \'unico argumento. Atrav\'es do conceito de 
\emph{well-foundedness} 
(ver em \cite{gs:discretemaths} e tamb\'em \cite{DEK:TAoCP-III},
p\'agina 20, exerc\'{\i}cio 15), podemos generalizar todo o
conceito de indu\c c\~ao matem\'atica e de admissibilidade fun\c c\~oes\ se, dado
um conjunto $S$ (de inteiros, \textbf{Natnum}, tuplas, etc), pudermos
estabelecer um rela\c c\~ao $\prec$ tal que:
\begin{itemize}
  \item toda a cadeia em $S$ tem um m\'{\i}nimo $x$: para todo $y\in S$ existe um
m\'{\i}nimo $x$ tal que $x\prec x_1\prec x_2\prec\ldots\prec y$.
  \item Se, para $x,y,z\in S$, $x\prec y$ e $y\prec z$, ent\~ao $x\prec z$.
\end{itemize}


Uma fun\c c\~ao recursiva \'e admiss\'{\i}vel se os argumentos das suas chamadas 
recursivas admitem algum rela\c c\~ao de preced\^encia que determina um
\emph{well-founded set}

\begin{eg}
\begin{align*}
gcd\ m\ n =& if\ m < n\\
         & then\ gcd\ m\ (n-m)\\
         & else\ if\ m > n\\
         & then\ gcd\ (m-n)\ n\\
         & else\ m
\end{align*}

A rela\c c\~ao abaixo
\begin{align*}
  (m_0,n_0) \prec (m_1,n_1) & \text{ quando } m_0<m_1 \\
  (m_0,n_0) \prec (m_1,n_1) & \text{ quando } (m_0=m_1)\land (n_0<n_1)
\end{align*}

e o fato de que nas chamadas recursivas de \textbf{gcd} os argumentos
de chamada s\~ao sempre maiores ou iguais do zero pode ser usada para provar 
que a defini\c c\~ao de \textbf{gcd} \'e admiss\'{\i}vel ( sempre termina.)
\end{eg}

Por outro lado, usando indu\c c\~ao forte, a rela\c c\~ao $\prec$ acima e
o fato de que o maior divisor de $m$ e $n$ \'e tamb\'em o maior divisor de
$m$ e $m-n$ (quando $m$ \'e maior do que $n$), permite provar que a fun\c c\~ao
acima calcula corretamente o maior divisor comum de dois inteiros
positivos.

\begin{ex}
Prove que $gcd(m,n)$ sempre termina e que calcula corretamente os maior divisor comum de $m$ e $n$.
\end{ex}

\subsection{Tipos abstratos de dados}

\begin{ex}
  Crie em Haskell, ao menos, as seguintes fun\c c\~oes\ sobre o tipo \natnum.
Defina e prove condi\c c\~oes\ de corre\c c\~ao para as 
mesmas:
\begin{enumerate}
  \item Fun\c c\~oes para c\'aclculo de:
    \begin{itemize}
      \item soma de dois objetos;
      \item diferen\c ca de dois objetos;
      \item produto de dois objetos;
      \item divi\~ao de dois objetos;
      \item resto da divis\~ao inteira de dois objetos.
    \end{itemize}
  \item Fun\c c\~oes\ implementar os rela\c c\~oes\ l\'ogicas, apresentando condi\c c\~oes\
de corre\c c\~ao:
    \begin{enumerate}
      \item igualdade;
      \item desigualdade;
      \item menor que;
      \item maior que;
    \end{enumerate}
\end{enumerate}
\end{ex}

\begin{ex}
Dadas as defini\c c\~oes\ de multiplica\c c\~ao, divis\~ao e resto da divis\~ao, prove o teorema
correspondente a 
$m = q*n+r$, quando $q$ \'e quociente da divis\~ao de $m$ por $n$ e $r$ \'e o resto dessa divis\~ao.
\end{ex}


\bibliography{abbrev,analysis,formal,maths,algorithms,program,string}

\bibliographystyle{amsplain}



\end{document}

