Instructions
Implémente le chiffrement et le déchiffrement du chiffre de la clôture.
Le chiffre de la clôture est une forme de chiffre de transposition qui tire son nom de la façon dont il est chiffré.
Il était déjà utilisé par les Grecs de l'Antiquité.
Dans le chiffre de la clôture, le message s'écrit vers le bas sur des « rails » successifs d'une clôture imaginaire, puis remonte lorsqu'on atteint le bas (comme un zigzag).
Enfin, on lit le message ligne par ligne.
Par exemple, avec trois « rails » et le message « WE ARE DISCOVERED FLEE AT ONCE », voici ce qu'écrit celui qui chiffre :
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 . .
Puis on lit :
WECRLTEERDSOEEFEAOCAIVDEN
Pour déchiffrer un message, on reprend la forme en zigzag et on remplit le texte chiffré le long des lignes.
? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
La première ligne compte sept emplacements que l'on peut remplir avec « WECRLTE ».
W . . . E . . . C . . . R . . . L . . . T . . . E
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Maintenant, la deuxième ligne accueille « ERDSOEEFEAOC ».
W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Ce qui laisse « AIVDEN » pour la dernière ligne.
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 tu suis maintenant la forme en zigzag, tu peux lire le message d'origine.
Sous-types
Cet exercice définit un sous-type appelé Positive, pour tous les entiers naturels supérieurs à 0.
On peut voir un sous-type comme un couple ⟨x, h⟩, où x est la valeur et h la preuve de sa validité.
On peut accéder à la valeur contenue dans un sous-type (x, dans ce cas) en utilisant .val, par exemple x.val.
On peut accéder à sa preuve en utilisant .property, par exemple x.property.
On peut aussi accéder aux deux par filtrage par motif, comme d'habitude.
Pour construire une valeur d'un sous-type, il faut prouver sa validité, dans ce cas, que le nombre est supérieur à 0.
Lean contient un certain nombre de lemmes et de théorèmes qui peuvent servir de point de départ pour cette preuve.
Par exemple, Nat.zero_lt_succ est un lemme qui affirme que pour tout entier naturel n : 0 < n + 1.
On trouve une bonne référence pour la démonstration de théorèmes en Lean dans la documentation de base.
