Projecto

O objectivo deste projecto é o de explorar o demonstrador de teoremas COQ para realizar provas simples. Sugere-se que os interessados realizem os exemplos do tutorial e de o survey Coq in a Hurry.

Para aplicar os conceitos estudados, devem escolher um (ou mais) dos desafios apresentados. Note que o trabalho é individual e a escolha do desafio deve ser sempre combinada com o docente. Para a entrega devem apresentar um pacote com o conjunto das scripts desenvolvidas (quer dos exemplos realizados, quer do desafio escolhido), "abundantemente" comentadas (preferencialmente fazendo uso da ferramenta coqdoc para produzir um documento contendo essas scripts). As sessões de apresentação irão consistir na execução e discussão das referidas scripts.

Apontadores Web:

• Coq web page
• Reference Manual
• Library Documentation

Desafios:

• Mostre que n^2 pode ser calculado como a soma dos primeiros n números ímpares.
• Demonstre que o somatório, para i=0..n de i e i^2 é respectivamente n*(n+1)/2 e n*(n+1)*(2*n+1)/6.
• Mostre que, para qualquer lista l, rev(rev(l))=l (rev é a função que inverte a ordem dos elementos numa lista).
• Considere a função f (a,b) (c,d) = (a*c+a*d+b*d, a*c+b*d). Mostre que:
  • a função é associativa e dispõe de elemento neutro.
  • a aplicação iterada dessa função (n vezes) sobre o valor (1,0) retorna o valor (Fib(n), Fib(n-1)) (onde Fib é a função de Fibonacci)