Este projeto descreve o uso da linguagem Maple para desenvolvimento da Indução Matemática e Recursão na disciplina de Fundamentos da Matemática para Computação II. Com uso da tradução livre do documento que foi disponibilizado do livro Matemática Discreta do Keneth H. Rosen, descreveremos como a Indução pode ser facilmente entendida e utilizada com Maple .
==Introdução==
Neste capítulo descreveremos como o maple pode ser usado para ajudar na compreensão e construção de provas matemáticas. Capacidades computacionais podem não parecer particularmente relevantes para o estudo das provas, embora na realidade essas capacidades possam ser úteis em provas de várias maneiras. Neste capítulo, descrevemos como o maple pode ser útil para trabalhar com regras formais de inferência, descrevemos como pode ajudar a compreender provas construtivas e não construtivas. Além disso, mostramos como usar o maple para ajudar a desenvolver provas usando indução matemática, até mesmo mostrando sua utilidade para ambos o passo base e passo indutivo, na prova da fórmula de somatório. Ademais, mostraremos como o maple pode ser usado para computar termos de sequencias definidas recursivamente. Vamos também comparar a eficiência da geração de termos dessa sequencia via técnicas indutivas versus técnicas recursivas.
==Método de prova==
Embora o maple não possa receber teoremas e resultados de provas para esses teoremas, pode receber expressões lógicas e simplificadas ou determinar características tais como: se uma expressão booleana pode ser satisfeita ou se é uma tautologia. Para trabalhar com expressões lógicas no maple, precisamos usar alguns dos recursos oferecidos pelo pacote de {\bf logic}(um assunto abordado de maneira mais aprofundada no capítulo 9).
Primeiramente examinaríamos os operadores lógicos: conjunção, disjunção, negação e {\bf implicação}. Não existe (no Maple). Para estudar as condicionais, devemos trabalhar com os operadores booleanos inativos oferecidos pelo pacote de {\bf '''logic}'''. Todos esses são iniciados com o caracter {\bf '''mexpr} $\''' <math>&$ </math> , por exemplo: usamos $\<math>'''&{\bf and}$ '''</math> ao invés de {\bf <math>'''and} '''</math> e $\<math>'''¬'''$ </math> ao invés de <math>'''not'''</math>. Em seguida, vão alguns exemplos do uso de operadores booleanos inativos:
[[File:imagem1.png]]
==Indução Matemática==
O maple pode ser usado para auxiliar na elaboração de provas de várias afirmações matemáticas usando a indução matemática. De fato, com o maple como seu assistente, você pode conduzir inteiramente o processo de descoberta e averiguação de forma intuitiva. É provável que entre os primeiros exemplos de indução matemática, encontremos a verificação da fórmula $<math>1+2+3+...+n = n(n+1)/2$</math>,a soma dos primeiros n inteiros positivos. O maple se adequa para provar fórmulas como essa porque os passos envolvidos numa prova indutiva incluem manipulação simbólica. É possível gerar uma grande quantidade de dados numéricos para serem examinado.
[[File:imagem14.png]]
[[File:imagem21.png]]
Podemos usar o procedimento '''subs''' para verificar o passo base da indução; neste caso o passo base é $<math>n=1$</math>
[[File:imagem22.png]]
Os resultados coincidem, então o passo indutivo é verificado. A fórmula agora segue por indução matemática. Assim, podemos concluir que enquanto o maple ainda não é capaz de construir provas inteiramente por conta própria, é uma ferramenta muito efetiva para ser usada na construção de provas interativas.
Agora, vamos considerar um exemplo mais complicado. A fórmula do somatório.
$<math>S = 1.1! + 2.2! +$...$+n.n!$</math>
É bem menos óbvio que o exemplo anterior. Para descobri-lo, iniciaremos gerando alguns dados numéricos.
[[File:imagens.png]]
Desta evidencia, devemos inferir a conjectura que a fórmula para nosso somatório é: $<math>S=(n+1)!-1$</math>
A prova indutiva pode ser conduzida assim como foi feito no primeiro exemplo.
==Definições Recursiva e Interativa==
As funções do maple podem ser definidas tanto processualmente (usando a função proc) como explicitamente (usando a notação $<math>->$</math>), cada um desses métodos envolve meios interativos e recursivos de definição. Iniciamos nosso estudo, usando a função $<math>->$ </math> do maple. Se nós quiséssemos definir uma função polinomial $<math>A(n)= 3n^3 + 41n^2- 3n + 101$ </math> nós usaríamos o seguinte comando:
[[File:imagem30.png]]
Agora, se quiséssemos definir uma função recursivamente, digamos:
$<math>b(n) =b(n-1)^2 + 2b(n-1) +6$</math>, com a condição inicial $<math>b(0) =2$</math>, então informaríamos(inserir):
[[File:imagem31.png]]
[[File:imagem32.png]]
Agora, criaremos uma função similar a {\bf '''b}''', chamada {\bf '''f1}''', que encontrará os números Fibonacci.
[[File:image33.png]]
Enquanto a notação “<math>->” </math> para funções é conveniente e intuitiva, ela não oferece todas as facilidades para melhoria da eficiência que estão disponíveis no uso do comando {\bf '''proc}'''. Para forçar o maple a calcular esses valores de forma eficiente, usamos a opção {\bf '''remember} ''' para definições de procedimentos afetados pelo uso do {\bf '''proc}'''. Esta opção exige que o maple lembre de qualquer valor para procedimento que já tenha sido computado através do armazenamento destes em uma tabela Fibonacci.
[[File:imagem34.png]]
Esse método processual engloba ambos os casos, o caso base (quando <math>n <=2</math>) e os casos indutivos (como na condição {\bf '''else}'''). Adicionalmente, o procedimento tem a indicação da função remember, forçando o maple a manter controle sobre quais valores da função já foram encontrados, para que estes sejam diretamente verificados ao invés de serem novamente computados.
[[File:imagem35.png]]
[[File:imagem45.png]]
Isso constrói uma lista indicando quais entre os primeiros 500 números Fibonacci são múltiplos de 5. Os dados indicam que o enésimo número Fibonacci $<math>F_n$ </math> é divisível por 5, somente se n é divisível por 5. Para obter evidências para a conversão, devemos testar se $<math>F_5n$ </math> é divisível por 5, para tantos n quanto forem possíveis. Para que nosso teste seja conciso e ainda permita testar um grande intervalo(série) de valores, vamos implementá-lo de maneira que nenhum resultado seja produzido, a menos que seja encontrado um contra exemplo.
[[File:imagem46.png]]
[[File:imagem49.png]]
Você pode tentar averiguar se esse padrão persiste, substituindo $500$ na definição de {\bf fib\_list} '''fib_list''' por números muito maiores. (O teste da divisibilidade por 111, nós deixamos pra você).2 – A notória conjectura $<math>3x + 1$ </math> (também conhecida como conjectura de Collatz e por vários outros nomes) afirma que: independente de qual inteiro x você escolha para iniciar, em iteração com a função f(x), onde f(x) = x/2, se x é par e f(x) = 3x+1 se x é ímpar, sempre produz o inteiro 1. Cheque essa conjectura para tantos inteiros positivos possíveis.
Para inicar, precisamos definir a função, a qual examinaremos.