निर्देश
रेल फेंस साइफर के लिए एन्कोडिंग और डिकोडिंग बनाइए।
रेल फेंस साइफर एक तरह का ट्रांसपोज़िशन साइफर है। इसका नाम इस बात से पड़ा है कि इसे किस तरह एन्कोड किया जाता है। इसे प्राचीन यूनानी पहले से इस्तेमाल करते थे।
रेल फेंस साइफर में संदेश को एक काल्पनिक बाड़ की एक के बाद एक "रेल" पर नीचे की ओर लिखा जाता है। नीचे पहुँचने पर लिखना ऊपर की ओर बढ़ने लगता है (ज़िग-ज़ैग की तरह)। अंत में संदेश को पंक्तियों में पढ़कर निकाला जाता है।
उदाहरण के लिए, तीन "रेल" और संदेश "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 होता है।
Lean में प्रमेय सिद्ध करने के लिए मुख्य डॉक्युमेंटेशन एक अच्छा संदर्भ है।
