柵欄密碼

說明

實作柵欄密碼的編碼與解碼。

柵欄密碼是一種換位密碼，名稱來自它的編碼方式。古希臘人早就在用了。

在柵欄密碼中，訊息會沿著一座想像柵欄上的一道道「欄杆」往下寫，寫到底部時再往上移動（就像鋸齒狀一樣）。最後再逐列把訊息讀出來。

舉例來說，使用三道「欄杆」和訊息「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

要解密訊息，就畫出鋸齒狀的圖形，然後把密文沿著各列填入。

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

第一列有七個位置，可以填入「WECRLTE」。

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

接著第二列填入「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 . .

現在只要沿著鋸齒狀的圖形讀下去，就能讀出原本的訊息。

Subtype

這個練習定義了一個稱為 Positive 的 Subtype，代表所有大於 0 的自然數。 Subtype 可以想成是一對 ⟨x, h⟩，其中 x 是值，h 是它有效性的證明。

Subtype 內的值（在這裡就是 x）可以透過 .val 取得，例如 x.val。 它的證明則可以透過 .property 取得，例如 x.property。 兩者也可以像平常一樣，透過模式比對取得。

要建構一個 Subtype 的值，就必須證明它的有效性，在這個例子中，也就是證明該數字大於 0。

Lean 中有許多引理與定理，可以作為這個證明的起點。 例如，Nat.zero_lt_succ 是一個引理，它斷言對任何自然數 n 而言：0 < n + 1。

---

出處

Wikipedia