رمز حصار ریلی

دستورالعمل‌ها

رمزگذاری و رمزگشایی را برای رمز Rail Fence پیاده‌سازی کنید.

رمز Rail Fence گونه‌ای از رمز جابجایی است که اسمش را از شیوه‌ی رمزگذاری‌اش گرفته است. یونانیان باستان هم از آن استفاده می‌کردند.

در رمز Rail Fence، پیام روی «ریل»های پیاپی یک حصار خیالی رو به پایین نوشته می‌شود و وقتی به پایین می‌رسیم رو به بالا حرکت می‌کند (مثل یک زیگزاگ). در پایان، پیام ردیف به ردیف خوانده می‌شود.

برای مثال، با سه «ریل» و پیام «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ها

این تمرین یک Subtype به اسم Positive تعریف می‌کند، برای همه‌ی اعداد طبیعی بزرگ‌تر از ۰. می‌توان Subtype را به‌صورت یک جفت ⟨x, h⟩ در نظر گرفت که در آن x مقدار و h اثبات درستی آن است.

به مقدار درون یک Subtype، که در اینجا x است، می‌توان با .val دسترسی داشت، مثلاً x.val. به اثبات آن هم می‌توان با .property دسترسی داشت، مثلاً x.property. همچنین می‌توان به هر دو مانند همیشه با تطبیق الگو هم دسترسی داشت.

برای ساختن یک مقدار برای یک Subtype، باید درستی آن را اثبات کرد، که در اینجا یعنی اثبات اینکه عدد بزرگ‌تر از ۰ است.

در Lean لم‌ها و قضیه‌های متعددی وجود دارد که می‌توانند به‌عنوان نقطه‌ی شروعی برای این اثبات به کار بیایند. برای نمونه، Nat.zero_lt_succ لمی است که بیان می‌کند برای هر عدد طبیعی n داریم: 0 < n + 1.

---

منبع

Wikipedia