Utasítások
Valósítsd meg a sínkerítés-rejtjel kódolását és dekódolását.
A sínkerítés-rejtjel az átrendezéses rejtjelek egy fajtája, amely a nevét arról kapta, ahogyan kódolják.
Már az ókori görögök is használták.
A sínkerítés-rejtjelnél az üzenetet egy képzeletbeli kerítés egymást követő „sínjein” lefelé haladva írjuk le, majd amikor elérünk az aljára, felfelé fordulunk (cikkcakkban).
Végül az üzenetet soronként olvassuk le.
Például három „sín” és a „WE ARE DISCOVERED FLEE AT ONCE” üzenet esetén a kódoló ezt írja ki:
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 . .
Majd ezt olvassa le:
WECRLTEERDSOEEFEAOCAIVDEN
Egy üzenet visszafejtéséhez vedd a cikkcakk alakzatot, és írd be a rejtjelezett szöveget a sorokba.
? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Az első sorban hét hely van, amit ki lehet tölteni a „WECRLTE” szöveggel.
W . . . E . . . C . . . R . . . L . . . T . . . E
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
A második sorba most az „ERDSOEEFEAOC” kerül.
W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .
Az utolsó sorra pedig az „AIVDEN” marad.
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 . .
Ha most végigolvasol a cikkcakk alakzat mentén, elolvashatod az eredeti üzenetet.
Altípusok
Ez a feladat definiál egy Positive nevű altípust minden 0-nál nagyobb természetes számra. Az altípusra gondolhatsz úgy, mint egy ⟨x, h⟩ párra, amelyben x az érték, h pedig annak a bizonyítéka, hogy érvényes.
Az altípusban lévő értéket (esetünkben x-et) a .val segítségével érheted el, például így: x.val. A bizonyítékát a .property segítségével, például így: x.property. Mindkettő elérhető mintaillesztéssel is, ahogy megszokhattad.
Ahhoz, hogy értéket hozz létre egy altípushoz, bizonyítanod kell az érvényességét, esetünkben azt, hogy a szám nagyobb 0-nál.
A Leanben számos lemma és tétel áll rendelkezésre, amelyek kiindulópontul szolgálhatnak ehhez a bizonyításhoz. Például a Nat.zero_lt_succ egy olyan lemma, amely azt állítja, hogy bármely n természetes számra: 0 < n + 1.
A Leanbeli tételbizonyításhoz jó kiindulópontot nyújt az alapdokumentáció.
