Projeto - Formalização da equivalência entre diferentes noções de permutação, e da correção do algoritmo bubblesort.

A proposta deste projeto é formalizar a equivalência entre duas noções distintas de permutação, e alternativamente, formalizar a correção do algoritmo bubblesort.

Objetivos:

  1. (20 pontos) Formalizar a equivalência entre as diferentes noções de permutação denominadas perm e equiv, OU
  2. (20 pontos) Formalizar a correção do algoritmo bubblesort, ou seja, enunciar e provar o teorema que estabelece que para qualquer lista l, o algoritmo bubblesort vai retornar uma permutação de l que está ordenada, E
  3. (10 pontos) Escrever um relatório sobre o projeto.

Etapas do projeto:

  1. Formação dos grupos: O primeiro passo consiste na formação dos grupos. Cada grupo pode ter até 4 pessoas. Se preferir fazer o projeto sozinho, basta acessar o link e criar o seu grupo. Caso contrário, primeiro combine a formação do grupo com os colegas. Em seguida, apenas um participante do grupo clica no link acima e em seguida no botão "Create team". Uma vez criado o grupo, os outros participantes devem clicar no botão "Join" do grupo criado.
  2. Desenvolva as tarefas citadas nos objetivos acima da forma como achar mais adequado.
  3. (Opcional) Fundamentos de Git e GitHub: link

Prazo: [2022-09-04 dom]. Nesta data, o repositório de cada grupo deve conter 2 arquivos no ramo principal:

  1. O arquivo lc1_2022_1_projeto.v contendo toda a formalização em Coq;
  2. O arquivo lc1-2022-1-relatorio.pdf contendo o relatório do grupo.