레일 펜스 암호

지침

레일 펜스 암호의 인코딩과 디코딩을 구현해요.

레일 펜스 암호는 인코딩하는 방식에서 이름을 따온 전위 암호의 한 종류예요. 고대 그리스인들도 이미 사용했어요.

레일 펜스 암호에서는 상상 속 울타리의 연속된 "레일"을 따라 메시지를 아래로 써 내려가다가, 바닥에 닿으면 다시 위로 올라가요 (지그재그처럼요). 마지막으로 메시지를 행 단위로 읽어요.

예를 들어 "레일" 세 개와 "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 . .

이제 지그재그 모양을 따라 읽으면 원래 메시지를 읽을 수 있어요.

하위 타입

이 연습 문제에서는 0보다 큰 모든 자연수를 나타내는 Positive라는 하위 타입을 정의해요. 하위 타입은 쌍 ⟨x, h⟩로 생각할 수 있는데, 여기서 x는 값이고 h는 그 값이 유효하다는 증명이에요.

하위 타입 안의 값(여기서는 x)은 .val을 사용해 접근할 수 있어요. 예를 들어 x.val처럼요. 그 증명은 .property를 사용해 접근할 수 있어요. 예를 들어 x.property처럼요. 둘 다 평소처럼 패턴 매칭으로도 접근할 수 있어요.

하위 타입의 값을 만들려면 그 값이 유효하다는 것, 즉 여기서는 그 수가 0보다 크다는 것을 증명해야 해요.

Lean에는 이 증명의 출발점이 될 수 있는 여러 보조 정리와 정리가 있어요. 예를 들어 Nat.zero_lt_succ는 임의의 자연수 n에 대해 0 < n + 1이라는 것을 주장하는 보조 정리예요.

---

출처

Wikipedia