2010-08-10 21 views
8

में सिर मैं एग्डा में एक साधारण लेम्मा साबित करने की कोशिश कर रहा हूं, जो मुझे लगता है कि सच है।दिखा रहा है (सिर। Init) = अंगडा

एक वेक्टर दो से अधिक तत्वों, init लेने के बाद अपने head लेने है, तो इसकी head तुरंत लेने के समान है।

मैं इसे तैयार की इस प्रकार है:

lem-headInit : ∀{l} (xs : Vec ℕ (suc (suc l))) 
        -> head (init xs) ≡ head xs 
lem-headInit (x ∷ xs) = ? 

कौन सा मुझे देता है;

.l : ℕ 
x : ℕ 
xs : Vec ℕ (suc .l) 
------------------------------ 
Goal: head (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) ≡ x 

एक प्रतिक्रिया के रूप में।

मैं पूरी तरह से समझ नहीं पा रहा हूं कि (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) घटक कैसे पढ़ा जाए। मुझे लगता है कि मेरे प्रश्न हैं; क्या यह संभव है, उस शब्द का अर्थ और कैसे अर्थ है।

बहुत धन्यवाद।

उत्तर

8

मुझे पूरी तरह से समझ नहीं आता कि (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) घटक को कैसे पढ़ा जाए। मैं मान लीजिए मेरे प्रश्न हैं; क्या यह संभव है, का अर्थ यह कैसे और कैसे होता है।

यह आपको बताता है कि मूल्य init (x ∷ xs)| के अधिकार के लिए सब कुछ के मूल्य पर निर्भर करता है। जब आप आगाडा में किसी फ़ंक्शन में कुछ साबित करते हैं तो आपके सबूत को मूल परिभाषा की संरचना होनी चाहिए।

इस मामले में आपको initLast के परिणाम पर मामला होना है क्योंकि initLast की परिभाषा किसी भी परिणाम देने से पहले यह करती है।

init : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n 
init xs   with initLast xs 
       -- ⇧ The first thing this definition does is case on this value 
init .(ys ∷ʳ y) | (ys , y , refl) = ys 

तो यहां हम लीमा लिखते हैं।

module inithead where 

open import Data.Nat 
open import Data.Product 
open import Data.Vec 
open import Relation.Binary.PropositionalEquality 

lem-headInit : {A : Set} {n : ℕ} (xs : Vec A (2 + n)) 
      → head (init xs) ≡ head xs 

lem-headInit (x ∷ xs) with initLast xs 
lem-headInit (x ∷ .(ys ∷ʳ y)) | ys , y , refl = refl 

मैं Vec A करने के लिए अपने लेम्मा सामान्यीकरण की स्वतंत्रता ले लिया क्योंकि लेम्मा वेक्टर की सामग्री पर निर्भर नहीं करता है।

3

ठीक है। मुझे यह धोखा देकर मिला है और मुझे उम्मीद है कि किसी के पास बेहतर समाधान होगा। मैंने init से प्राप्त सभी अतिरिक्त जानकारी को initLast के संदर्भ में परिभाषित किया और अपना स्वयं का बेवकूफ संस्करण बनाया।

initLazy : ∀{A l} → Vec A (suc l) → Vec A l 
initLazy (x ∷ []) = [] 
initLazy (x ∷ (y ∷ ys)) = x ∷ (initLazy (y ∷ ys)) 

अब लेम्मा मामूली है।

कोई अन्य ऑफर?

संबंधित मुद्दे