レールフェンス暗号

説明

レールフェンス暗号の暗号化と復号を実装してください。

レールフェンス暗号は転置暗号の一種で、その名前は暗号化の方法に由来します。 古代ギリシャ人もすでに使っていました。

レールフェンス暗号では、メッセージを架空のフェンスのレールに順に下向きに書いていき、一番下まで来たら上向きに進みます（ジグザグのように）。 最後に、メッセージを行ごとに読み取ります。

たとえば、3本のレールとメッセージ"WE ARE DISCOVERED FLEE AT ONCE"を使うと、暗号化する人は次のように書き出します。

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 . .

次に、次のように読み取ります。

WECRLTEERDSOEEFEAOCAIVDEN

メッセージを復号するには、ジグザグの形を用意し、暗号文を行に沿って埋めていきます。

? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

1行目には7つのマスがあり、"WECRLTE"を入れることができます。

W . . . E . . . C . . . R . . . L . . . T . . . E
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

次に、2行目に"ERDSOEEFEAOC"を入れます。

W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

最後の行には"AIVDEN"が残ります。

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 . .

この状態でジグザグの形に沿って読むと、元のメッセージを読み取ることができます。

サブタイプ

この演習では、0より大きいすべての自然数を表すPositiveというサブタイプを定義します。 サブタイプは、⟨x, h⟩というペアとして考えることができます。ここで、xは値、hはそれが有効であることの証明です。

サブタイプの中の値（ここではx）には、.valを使ってアクセスできます。たとえばx.valです。 その証明には、.propertyを使ってアクセスできます。たとえばx.propertyです。 どちらも、通常どおりパターンマッチングでもアクセスできます。

サブタイプの値を作るには、それが有効であること、ここではその数が0より大きいことを証明する必要があります。

Leanには、この証明の出発点として使える補題や定理がいくつかあります。 たとえば、Nat.zero_lt_succは、任意の自然数nについて0 < n + 1が成り立つことを主張する補題です。

---

出典

Wikipedia