Шифр паркану

Вказівки

Реалізуймо кодування та декодування для шифру залізничної огорожі.

Шифр залізничної огорожі - це різновид шифру перестановки, назва якого походить від способу кодування. Його використовували ще давні греки.

У шифрі залізничної огорожі повідомлення записують униз по послідовних «рейках» уявної огорожі, а дійшовши до низу, рухаються вгору (як зигзаг). Потім повідомлення зчитують по рядках.

Наприклад, використовуючи три «рейки» та повідомлення «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 . .

Якщо тепер читати вздовж зигзагоподібної форми, можна прочитати початкове повідомлення.

Підтипи

Ця вправа визначає підтип з назвою Positive для всіх натуральних чисел, більших за 0. Підтип можна розглядати як пару ⟨x, h⟩, де x - це значення, а h - доведення його правильності.

До значення всередині підтипу (у цьому випадку x) можна дістатися за допомогою .val, наприклад x.val. До його доведення можна дістатися за допомогою .property, наприклад x.property. До обох можна також дістатися за допомогою зіставлення зі зразком, як звично.

Щоб побудувати значення для підтипу, потрібно довести його правильність, у цьому випадку довести, що число більше за 0.

У Lean є низка лем і теорем, які можуть стати відправною точкою для цього доведення. Наприклад, Nat.zero_lt_succ - це лема, яка стверджує, що для будь-якого натурального числа n: 0 < n + 1.

---

Джерело

Wikipedia