شيفرة السياج

التعليمات

نفّذ الترميز وفك الترميز لشيفرة السياج.

شيفرة السياج شكل من أشكال شيفرات النقل، وقد اكتسبت اسمها من الطريقة التي تُرمَّز بها. وقد استخدمها الإغريق القدماء بالفعل.

في شيفرة السياج، تُكتب الرسالة نزولًا على "قضبان" متتالية لسياج تخيلي، ثم تتحرك صعودًا عند الوصول إلى القاع (على شكل خط متعرج). وفي النهاية تُقرأ الرسالة في صفوف.

على سبيل المثال، باستخدام ثلاثة "قضبان" والرسالة "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.

---

المصدر

ويكيبيديا