Prova da (issue #21)

[Patrick20022]

Precisei assumir que xs.1 ≠ [] (ou seja, que a primeira parte da SymList não está vazia), porque, quando o primeiro lado da lista simétrica está vazio, a definição de snocSL faz uma reorganização nos componentes para manter a estrutura válida.

Isso quebra a igualdade com snoc x (fromSL (xs.1, xs.2)), pois os lados da SymList mudam de lugar, e a lista final construída por fromSL não coincide com a lista obtida aplicando snoc diretamente.

Com xs.1 ≠ [], essa troca não acontece, e aí funciona normalmente.

[arademaker]

o ponto principal deste example é mostrar que a implementação de SymList apenas como um par de listas não é suficiente. Não é uma prova que queremos completar.

Veja que sem assumir nada, quando fazemos a indução sobre as o caso base nil chega em ⊢ bs.reverse = bs o que obviamente só é verdade quando bs é uma lista de apenas um elemento. Mas não temos nesta implementação como saber que bs tem que ser single para quando as é nula. Se vc assumir que a primeira lista é não vazia, constrói uma contradição no caso base da indução e prova por contradição que ⊢ bs.reverse = bs, mas ai não estamos provando a equivalência das função para qualquer SymList certo?

[arademaker]

Eu comentei todo este example para suprimir este warning da compilação, dado que este será um caso que não queremos completar a prova.