Instrucciones
Implementa la codificación y la descodificación para el cifrado de la valla ferroviaria.
El cifrado de la valla ferroviaria es un tipo de cifrado de transposición que recibe su nombre de la forma en que se cifra.
Ya lo usaban los antiguos griegos.
En el cifrado de la valla ferroviaria, el mensaje se escribe hacia abajo en sucesivos «raíles» de una valla imaginaria y, al llegar abajo, se sube (como en un zigzag).
Por último, el mensaje se lee por filas.
Por ejemplo, con tres «raíles» y el mensaje «WE ARE DISCOVERED FLEE AT ONCE», quien cifra escribe:
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 . .
Y después lee:
WECRLTEERDSOEEFEAOCAIVDEN
Para descifrar un mensaje, se toma la forma en zigzag y se rellena el texto cifrado a lo largo de las filas.
? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
La primera fila tiene siete huecos que se pueden rellenar con «WECRLTE».
W . . . E . . . C . . . R . . . L . . . T . . . E
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Ahora la segunda fila toma «ERDSOEEFEAOC».
W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Y deja «AIVDEN» para la última fila.
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 . .
Si ahora lees a lo largo de la forma en zigzag, puedes leer el mensaje original.
Subtipos
Este ejercicio define un subtipo llamado Positive, para todos los números naturales mayores que 0.
Un subtipo se puede concebir como un par ⟨x, h⟩, donde x es el valor y h es la prueba de su validez.
Al valor dentro de un subtipo (x, en este caso) se puede acceder usando .val, por ejemplo, x.val.
A su prueba se puede acceder usando .property, por ejemplo, x.property.
También se puede acceder a ambos mediante coincidencia de patrones, como es habitual.
Para construir un valor para un subtipo, es necesario demostrar su validez; en este caso, que el número es mayor que 0.
Hay varios lemas y teoremas en Lean que pueden servir como punto de partida para esta demostración.
Por ejemplo, Nat.zero_lt_succ es un lema que afirma que, para cualquier número natural n: 0 < n + 1.
Puedes encontrar una buena referencia para la demostración de teoremas en Lean en la documentación principal.
