% This .tex file uses ThaTeX and should be compiled with xetex.
% To obtain and install ThaTeX see:  https://github.com/tsouanas/thatex
\input thatexhandout

\def\PROFESSOR  {Θάνος}
\def\COURSE     {FMC1}
\def\SEMESTER   {2021.2}
\def\HANDOUT    {Problem Set 2}
\def\DEADLINE   {23/01/2022, 23h59}
\def\POINTS     {100 + \bonus{16}}
\def\STUDENT    {Θάνος \bf (gabarito)}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\fib#1{F_{#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mktitle

\rules Regras e esclarecimentos.
\rule: Podes citar como lemma (sem demonstrar) \emph{apenas:}
       (i) teoremas que são \emph{demonstrados} no fmcbook;
       (ii) teoremas que demonstramos na U1 no NNG.
\rule: Nenhuma outra consulta ou colaboração é permitida.
\rule: Todo o Problem Set está no mundo dos naturais; não dos inteiros!
       Isso tem uma conseqüência boa e uma ruim:
       (i) Podes citar como lemma gratuito (sem demonstrar) qualquer
       teorema que já demonstramos na U1 (incluindo os teoremas do NNG).
       (ii) Não podes usar operações e relações de inteiros.
       Por exemplo, não podes usar subtração: se na tua prova aparecer
       uma expressão que envolve subtração, seria um type error e
       tua demonstração sequer compilaria!
\rule: O E1 precisa ser resolvido por indução, e o E2 por recursão.
\rule: O E1 possui duas partes: existência (E1E) e unicidade (E1U).
       (i) Para a existência é obrigatório usar indução (em forma essencial).
       (ii) Para a unicidade não—mas a verdade é que aqui o uso de indução
       será provavelmente escondido nas demonstrações de lemmas
       citados-e-já-demonstrados e não explicitamente exposto no texto
       da tua demonstração.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\Question Problema E1. [64 pts]
Demonstre \emph{por indução} o teorema da divisão de Euclides para naturais:
\statement{para quaisquer naturais $a,b$ com $b \neq 0$,
existem únicos naturais $q,r$ tais que: (i) $a = bq + r$; (ii) $r < b$.}

\answer Existência.
Seja $b \neq 0$ e logo seja $b'$ o predecessor de $b$: $b = Sb'$.
Por indução no $a$.
\crproofpart{Base.}
Imediato pois $0 = b \ntimes 0 + 0$ e $0 < b$.
Ou seja, temos quociente $0$ e resto $0$.
\crproofpart{Passo indutivo.}
Seja $a$ tal que
$$
\text{existem $q,r$ tais que $a = bq + r$ {\&} $r < b$}
\tag {H.I.}
$$
e logo sejam $q_a, r_a$ tais naturais:
$a = bq_a + r_a$\fact 1 {\&} $r_a < b$\fact 2.
Pela \byfact 1, temos $Sa = S(bq_a + r_a) = bq_a + Sr_a$\fact 3.
Pela \byfact 2, $r_a \leq b'$.
Logo $r_a = b'$ ou $r_a < b'$.
Separamos em casos:
\crcase{Caso $r_a = b'$.}
Calculamos:
\compute
Sa &= bq_a + Sr_a  \by {pela \byfact 3} \\
   &= bq_a + Sb'   \by {hipótese do caso} \\
   &= bq_a + b     \by {pela escolha do $b'$} \\
   &= bSq_a        \by {pela \reversed{(a2)}} \\
   &= bSq_a + 0.   \\
\endcompute
Neste caso então, o quociente é o $Sq_a$ e o resto o $0$.
\crcase{Caso $r_a < b'$.}
Aqui temos $Sr_a < Sb' = b$ e logo a \byfact 3
já nos fornece os naturais que precisamos:
o quociente é o $q_a$ e o resto o $Sr_a$.
\qed

\answer Unicidade.
Sejam $a,b,q_1,r_1,q_2,r_2$ com $b \neq 0$
tais que $bq_1 + r_1 = a = bq_2 + r_2$\fact 1 {\&} $r_1,r_2 < b$.
Já que $\leq$ é total, suponha sem perda de generalidade que $q_1 \leq q_2$.
Logo seja $d$ tal que $q_1 + d = q_2$\fact 2.
Calculamos:
\compute
\cancel{bq_1} + r_1
&= bq_2 + r_2                  \by {pela \byfact 1} \\
&= b(q_1 + d) + r_2            \by {pela escolha de $d$} \\
&= (bq_1 + bd) + r_2           \\
&= \cancel{bq_1} + (bd + r_2). \\
\intertext{Cancelando os $bq_1$ temos}
r_1 &= bd + r_2.\fact 3
\endcompute
Separamos em casos sobre o $d$:
\crcase{Caso $d = 0$.}
Substituindo $d \asseq 0$ nas \byfact 2 e \byfact 3
obtemos $q_1 = q_2$ e $r_1 = r_2$ respectivamente.
\crcase{Caso $d = Sd'$ para algum $d'$.}
Calculamos:
\compute
r_1 &= bd + r_2         \\
    &= bSd' + r_2       \by {pela escolha de $d'$} \\
    &= (bd' + b) + r_2  \\
    &= b + (bd' + r_2). \\
\endcompute
Logo $b \leq r_1$ e portanto este caso é impossível, já que $r_1 < b$.
\qed

\Question Problema E2. [\bonus{16} pts]
Define \emph{recursivamente} as funções $\rem$ e $\quot$ nos naturais.
Considere que seu segundo argumento necessariamente terá a forma $Sb$ para algum natural $b$.
Exemplos de ``input--output'':
\mathcols 3
\quot (18,3) &= 6 & \quot (13,5) &= 2 & \quot (7,12) &= 0  \\
\rem  (18,3) &= 0 & \rem  (13,5) &= 3 & \rem  (7,12) &= 7. \\
\endmathcols

\answer Resposta.
A definição por recursão vem diretamente da demonstração por indução
no {\bf E1} onde estabelecemos a existência do quociente e do resto,
\emph{os construindo}.
Optei para usar $Sb'$ para o segundo argumento das funções aqui
pois assim a ligação com o {\bf E1} fica mais aparente ainda.
\eop
Definimos:
\mathcols 2
\quot (0,Sb')  &= 0 &
\rem  (0,Sb')  &= 0 \\
\quot (Sa,Sb') &= \cases{ Sq_a , & se $r_a = b'$; \\
                          q_a  , & se $r_a < b'$; \\ } &
\rem  (Sa,Sb') &= \cases{ 0    , & se $r_a = b'$; \\
                          Sr_a , & se $r_a < b'$; \\ } \\
\endmathcols
$$
\text{onde:} \quad \mathcoled {
  q_a &= \quot(a,Sb')  \\
  r_a &= \rem (a,Sb'). \\
}
$$

\Question Problema F. [36 pts]
Definimos a seqüência dos números Fibonacci pelas
\mathcols 3
\fib {0}   &= 0 &
\fib {S0}  &= 1 &
\fib {SSn} &= \fib {Sn} + \fib n.
\endmathcols
Demonstre que para quaisquer $m,n\in\nats$,
$$
\fib {S(m+n)} = \fib {Sm} \fib {Sn} + \fib m \fib n.
$$

\answer Demonstração.
Por indução no $m$.
\crproofpart{Base: $\lforall {n \in \nats} {\fib {S(0+n)} = \fib {S0} \fib {Sn} + \fib 0 \fib n}$.}
Seja $n \in \nats$.
Calculamos:
\compute
\fib {S0} \fib {Sn} + \fib 0 \fib n
&= 1 \ntimes \fib {Sn} + 0 \ntimes \fib n \\
&= \fib {Sn} \\
&= \fib {S(0+n)}  \obvious \\
\endcompute
\crproofpart{Passo indutivo.}
Seja $w$ tal que
$$
\lforall {t \in \nats}
   {\fib {S(w+t)} = \fib {Sw} \fib {St} + \fib w \fib t}.
\tag {H.I.}
$$
Vamos demonstrar que
$$
\lforall {n \in \nats}
   {\fib {S(Sw+n)} = \fib {SSw} \fib {Sn} + \fib {Sw} \fib n}.
$$
Seja $n \in \nats$.
Calculamos:
\compute
\fib {SSw} \fib {Sn} + \fib {Sw} \fib n
&= (\fib {Sw} + \fib w) \fib {Sn} + \fib {Sw} \fib n             \by {def.~de $\fib {SSw}$} \\
&= (\fib {Sw} \fib {Sn} + \fib w \fib {Sn}) + \fib {Sw} \fib n   \\
&= \fib {Sw} \fib {Sn} + (\fib w \fib {Sn}  + \fib {Sw} \fib n)  \\
&= \fib {Sw} \fib {Sn} + (\fib {Sw} \fib n  + \fib w \fib {Sn})  \\
&= (\fib {Sw} \fib {Sn} + \fib {Sw} \fib n) + \fib w \fib {Sn}   \\
&= \fib {Sw} (\fib {Sn} + \fib n) + \fib w \fib {Sn}             \\
&= \fib {Sw} \fib {SSn} + \fib w \fib {Sn}                       \by {def.~de $\fib {SSn}$} \\
&= \fib {S(w + Sn)}                                              \by {H.I.~com $t \asseq Sn$} \\
&= \fib {S(Sw + n)}.                                             \\
\endcompute
\qed

\bye
