Instrucciones
Implementa la codificación y la decodificación del cifrado de valla.
El cifrado de valla es una forma de cifrado por transposición que recibe su nombre de la manera en que se codifica.
Ya lo usaban los antiguos griegos.
En el cifrado de valla, el mensaje se escribe hacia abajo sobre los sucesivos «carriles» de una valla imaginaria, y luego se sube al llegar al fondo (como un zigzag).
Finalmente, el mensaje se lee por filas.
Por ejemplo, con tres «carriles» 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 se lee:
WECRLTEERDSOEEFEAOCAIVDEN
Para descifrar un mensaje, tomas la forma en zigzag y rellenas el texto cifrado a lo largo de las filas.
? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
La primera fila tiene siete lugares 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 pensar como un par ⟨x, h⟩, donde x es el valor y h es la demostración de su validez.
Se puede acceder al valor dentro de un subtipo (x, en este caso) usando .val; por ejemplo, x.val.
Se puede acceder a su demostración usando .property; por ejemplo, x.property.
También se puede acceder a ambos mediante coincidencia de patrones, como siempre.
Para construir un valor de un subtipo, es necesario demostrar su validez; en este caso, que el número es mayor que 0.
En Lean hay varios lemas y teoremas 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.
