coq.org

Curso de Coq da disciplina OPAT001

Exame final dia 04/07/2018

*Resultado competição tableaux*

*Notas trabalho tableux*

*Notas prova 1*

*Notas prova 2* - Respostas

*Tabela de táticas*

Aula	Data	Exercícios	Fonte
1 - Introdução à introdução de Coq	02/05/2018		aula1.v
2 - Programação Funcional em Coq	02/05/2018		aula2.v
3 - Recursão Primitiva em Coq	07/05/2018		aula3.v
4 - Prova por simplificação, reescrita e análise de caso	07/05/2018		aula4.v
5 - Prova por indução	09/05/2018		aula5.v
6 - Duplas de Naturais	14/05/2018		aula6.v
7 - Listas de Naturais	16/05/2018		aula7.v
8 - Mais provas sobre listas de naturais	21/05/2018		aula8.v
9 - Polimorfismo em Coq	21/05/2018		aula9.v
10 - Funções de ordem superior	23/05/2018		aula10.v
11 - Táticas Apply e Inversion	04/06/2018		aula11.v
12 - Variações de táticas e outras táticas	04/06/2018		aula12.v
13 - Lógica em Coq 1	06/06/2018		aula13.v
14 - Lógica em Coq 2	06/06/2018		aula14.v
15 - Aula para tirar dúvidas	11/06/2018

Primeiro Torneio de Artes em Coq da UDESC (Coq’s Art Tournament)

Resultado final mesmo!:

Posição	Nome	Pontos adicionais na prova prática	Estrelas
Primeiro	Feliperama	3	145
Segundo	F U T U R E	2	117
Terceiro	Flavio	1	111

Algumas pessoas foram legais e resoveram não validar suas estrelas, o que ajudou alguns necessitados de nota. Resolvi batizar esses de anjos! Anjos: Commander Shepard, Shmebulock, Marmita, Bugs, Feliperama, Fredie Mercury, mangusto_alado35 e JuroQueNãoColei.

Enviar arquivos doit*.v para rafaelcgs10@gmail.com.

Assunto do email: [OPAT001][CoqArTour][SeuNome]-DOIT*.

Fim do torneio: dia 12/06/2018.

Colar zera as suas estrelas

Utilizar teoremas da biblioteca padrão inválida o exercício.

Cada posição pode ser ocupada por vários empatados.

Os melhores colocados deverão defender suas provas numa entrevista agendada.

Desafio supremo em Coq

Quem resolver este desafio tira, automaticamente, 10 na prova prática.

Somente será aceito um vencedor do desafio.

Para concorrer é preciso estar na primeira colocação do torneio quando o mesmo for finalizado (dia 12/06).

Deve-se marcar a entrevista para defender as soluções do torneio e deste desafio no dia 13/06 antes da prova.

Como somente há um vencedor, então o primeiro a entregar a solução do desafio para rafaelcgs10@gmail.com vence.

Consultar na internet a prova informal do teorema é permitido, mas obviamente não é permitido copiar uma solução feita em Coq.

Utilizar as bibliotecas do Coq é permitido (e necessário).

Desafio

Referência

Software Foundations: Livro e vídeos