Instruções
Implementa a codificação e a descodificação da cifra Rail Fence.
A cifra Rail Fence é uma forma de cifra de transposição que recebe o nome da forma como é codificada.
Já era utilizada pelos antigos gregos.
Na cifra Rail Fence, a mensagem é escrita de forma descendente em "carris" sucessivos de uma cerca imaginária, e sobe quando chega ao fundo (como um zigue-zague).
Por fim, a mensagem é lida por linhas.
Por exemplo, com três "carris" e a mensagem "WE ARE DISCOVERED FLEE AT ONCE", quem cifra escreve:
W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . A . . . I . . . V . . . D . . . E . . . N . .
De seguida, lê:
WECRLTEERDSOEEFEAOCAIVDEN
Para desencriptar uma mensagem, tomas a forma em zigue-zague e preenches o texto cifrado ao longo das linhas.
? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
A primeira linha tem sete lugares que podem ser preenchidos com "WECRLTE".
W . . . E . . . C . . . R . . . L . . . T . . . E
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Agora, a segunda linha recebe "ERDSOEEFEAOC".
W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Deixando "AIVDEN" para a última linha.
W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . A . . . I . . . V . . . D . . . E . . . N . .
Se agora leres ao longo da forma em zigue-zague, consegues ler a mensagem original.
Subtipos
Este exercício define um subtipo chamado Positive, para todos os números naturais maiores do que 0.
Um subtipo pode ser pensado como um par ⟨x, h⟩, em que x é o valor e h é a prova da sua validade.
O valor dentro de um subtipo (x, neste caso) pode ser acedido através de .val, por exemplo, x.val.
A sua prova pode ser acedida através de .property, por exemplo, x.property.
Ambos podem também ser acedidos por correspondência de padrões, como habitualmente.
Para construir um valor para um subtipo, é necessário provar a sua validade, neste caso, que o número é maior do que 0.
Há vários lemas e teoremas em Lean que podem servir de ponto de partida para esta prova.
Por exemplo, Nat.zero_lt_succ é um lema que afirma que, para qualquer número natural n: 0 < n + 1.
Podes encontrar uma boa referência para a prova de teoremas em Lean na documentação principal.
