栅栏密码

说明

实现栅栏密码的编码和解码。

栅栏密码是一种换位密码，名字来自它的编码方式。古希腊人就已经使用过它。

在栅栏密码中，消息沿着想象中栅栏的一条条“栏”向下写，到达底部后再向上移动（就像之字形）。最后，再按行读出消息。

例如，使用 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

要解密一条消息，先画出之字形，再沿着各行填入密文。

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

第一行有 7 个空位，可以填入“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 . .

现在沿着之字形读下去，就能读出原始消息。

子类型

本练习定义了一个名为 Positive 的子类型，适用于所有大于 0 的自然数。 子类型可以看作一个二元组 ⟨x, h⟩，其中 x 是值，h 是该值有效的证明。

子类型内部的值（这里是 x）可以通过 .val 访问，例如 x.val。 它的证明可以通过 .property 访问，例如 x.property。 两者也都和往常一样，可以通过模式匹配来访问。

要为子类型构造一个值，必须先证明它有效，在这里就是要证明这个数字大于 0。

Lean 中有许多引理和定理可以作为这个证明的起点。 例如，Nat.zero_lt_succ 是一条引理，它断言对任意自然数 n 都有：0 < n + 1。

---

来源

Wikipedia