Cifra de cerca de trilhos

Instruções

Implemente a codificação e a decodificação da cifra de cerca (rail fence cipher).

A cifra de cerca é um tipo de cifra de transposição que recebe esse nome pela forma como é codificada. Ela já era usada pelos antigos gregos.

Na cifra de cerca, a mensagem é escrita de cima para baixo em "trilhos" sucessivos de uma cerca imaginária e, ao chegar ao fundo, sobe de volta (como em um zigue-zague). Por fim, a mensagem é lida linha a linha.

Por exemplo, usando três "trilhos" e a mensagem "WE ARE DISCOVERED FLEE AT ONCE", quem cifra escreve o seguinte:

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 . .

Depois, lê o seguinte:

WECRLTEERDSOEEFEAOCAIVDEN

Para decifrar uma mensagem, você monta o formato de zigue-zague e preenche o texto cifrado ao longo das linhas.

? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

A primeira linha tem sete posições que podem ser preenchidas 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 você ler ao longo do formato de zigue-zague, vai conseguir ler a mensagem original.

Subtipos

Este exercício define um subtipo chamado Positive, para todos os números naturais maiores que 0. Um subtipo pode ser pensado como um par ⟨x, h⟩, onde x é o valor e h é a prova de sua validade.

O valor dentro de um subtipo (x, neste caso) pode ser acessado usando .val, por exemplo, x.val. Sua prova pode ser acessada usando .property, por exemplo, x.property. Ambos também podem ser acessados por casamento de padrões, como de costume.

Para construir um valor para um subtipo, é necessário provar sua validade, neste caso, que o número é maior que 0.

Existem vários lemas e teoremas em Lean que podem servir como 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.

---

Fonte

Wikipedia