Istruzioni
Implementa la codifica e la decodifica del cifrario rail fence.
Il cifrario Rail Fence è una forma di cifrario a trasposizione che prende il nome dal modo in cui viene codificato.
Era già usato dagli antichi Greci.
Nel cifrario Rail Fence, il messaggio viene scritto verso il basso su «rails» successivi di una recinzione immaginaria, poi risalendo quando si arriva in fondo (come uno zig-zag).
Infine il messaggio viene letto riga per riga.
Per esempio, usando tre «rails» e il messaggio «WE ARE DISCOVERED FLEE AT ONCE», chi cifra scrive:
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 . .
Poi legge:
WECRLTEERDSOEEFEAOCAIVDEN
Per decifrare un messaggio, si prende la forma a zig-zag e si riempiono le righe con il testo cifrato.
? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
La prima riga ha sette posizioni che possono essere riempite con «WECRLTE».
W . . . E . . . C . . . R . . . L . . . T . . . E
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Ora la seconda riga prende «ERDSOEEFEAOC».
W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Lasciando «AIVDEN» per l'ultima riga.
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 ora leggi lungo la forma a zig-zag, puoi leggere il messaggio originale.
Subtypes
Questo esercizio definisce un Subtype chiamato Positive, per tutti i numeri naturali maggiori di 0.
Un Subtype si può pensare come una coppia ⟨x, h⟩, dove x è il valore e h è la dimostrazione della sua validità.
Si può accedere al valore contenuto in un Subtype (x, in questo caso) usando .val, per esempio x.val.
Alla sua dimostrazione si può accedere usando .property, per esempio x.property.
Ad entrambi si può accedere anche tramite il pattern matching, come al solito.
Per costruire un valore per un Subtype, è necessario dimostrarne la validità, in questo caso che il numero sia maggiore di 0.
In Lean ci sono diversi lemmi e teoremi che possono servire come punto di partenza per questa dimostrazione.
Per esempio, Nat.zero_lt_succ è un lemma che afferma che per ogni numero naturale n: 0 < n + 1.
Un buon riferimento per la dimostrazione di teoremi in Lean si trova in la documentazione principale.
