≡-तर्क और 'साथ' पैटर्न

Question

मैं filter और map के कुछ गुण साबित कर रहा था, जब तक मैं इस संपत्ति पर ठोकर नहीं डालता तब तक सब कुछ ठीक हो गया: filter p (map f xs) ≡ map f (filter (p ∘ f) xs)। यहाँ कोड है कि प्रासंगिक है का एक हिस्सा है:

open import Relation.Binary.PropositionalEquality 
open import Data.Bool 
open import Data.List hiding (filter) 

import Level 

filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A 
filter _ [] = [] 
filter p (x ∷ xs) with p x 
... | true = x ∷ filter p xs 
... | false = filter p xs 

अब, क्योंकि मैं ≡-Reasoning मॉड्यूल का उपयोग कर सबूत लेखन से प्यार है, पहली बात मैंने कोशिश की थी:

open ≡-Reasoning 
open import Function 

filter-map : ∀ {a b} {A : Set a} {B : Set b} 
      (xs : List A) (f : A → B) (p : B → Bool) → 
      filter p (map f xs) ≡ map f (filter (p ∘ f) xs) 
filter-map []  _ _ = refl 
filter-map (x ∷ xs) f p with p (f x) 
... | true = begin 
    filter p (map f (x ∷ xs)) 
    ≡⟨ refl ⟩ 
    f x ∷ filter p (map f xs) 
-- ... 

लेकिन अफसोस, कि काम नहीं किया । एक घंटे के लिए कोशिश कर के बाद, मैं अंत में छोड़ दिया और इस तरह से यह साबित हो:

filter-map (x ∷ xs) f p with p (f x) 
... | true = cong (λ a → f x ∷ a) (filter-map xs f p) 
... | false = filter-map xs f p 

फिर भी क्यों ≡-Reasoning माध्यम से जा रहा काम नहीं किया के बारे में उत्सुक है, मैं बहुत तुच्छ कुछ करने की कोशिश की:

filter-map-def : ∀ {a b} {A : Set a} {B : Set b} 
       (x : A) xs (f : A → B) (p : B → Bool) → T (p (f x)) → 
       filter p (map f (x ∷ xs)) ≡ f x ∷ filter p (map f xs) 
filter-map-def x xs f p _ with p (f x) 
filter-map-def x xs f p() | false 
filter-map-def x xs f p _ | true = -- not writing refl on purpose 
    begin 
    filter p (map f (x ∷ xs)) 
    ≡⟨ refl ⟩ 
    f x ∷ filter p (map f xs) 
    ∎ 

लेकिन टाइपशेकर मुझसे सहमत नहीं है। ऐसा लगता है कि वर्तमान लक्ष्य filter p (f x ∷ map f xs) | p (f x) बनी हुई है और भले ही मैं पैटर्न p (f x) पर मेल खाता हूं, filter बस f x ∷ filter p (map f xs) तक कम नहीं होगा।

क्या इस काम को ≡-Reasoning के साथ बनाने का कोई तरीका है?

धन्यवाद!

Answer 1

with -clauses के साथ समस्या यह है कि Agda पैटर्न मिलान से सीखी जानकारी को भूल जाता है जब तक कि आप इस जानकारी को संरक्षित रखने के लिए पहले से व्यवस्थित नहीं करते हैं।

दरअसल, जब AGDA एक with expression खंड देखता है, यह वर्तमान संदर्भ और एक ताजा चर w साथ लक्ष्य में expression के सभी आवृत्तियां बदल देता है और फिर आप के साथ-खंड में अद्यतन संदर्भ और लक्ष्य के साथ कि चर देता है, भूल इसकी उत्पत्ति के बारे में सब कुछ।

आपके मामले में, आप अंदर filter p (map f (x ∷ xs)) लिखने के साथ-ब्लॉक, तो यह बाद AGDA तो AGDA पहले से ही इस तथ्य भूल गया है कि p (f x)true है और अवधि को कम नहीं करता, नए सिरे से लिखना प्रदर्शन किया है दायरे में चला जाता है।

आप मानक पुस्तकालय से "निरीक्षण" -पंथियों में से एक का उपयोग कर समानता के प्रमाण को संरक्षित कर सकते हैं, लेकिन मुझे यकीन नहीं है कि यह आपके मामले में उपयोगी कैसे हो सकता है।