विशेष रचनाकारों पर पैटर्न मैच

Question

मैं कुछ दिनों के लिए एक समस्या के खिलाफ अपने सिर को टक्कर लगी हूं, लेकिन मेरे एजडा कौशल बहुत मजबूत नहीं हैं।

मैं एक अनुक्रमित डेटा प्रकार पर एक फ़ंक्शन लिखने की कोशिश कर रहा हूं जिसे केवल एक विशेष अनुक्रमणिका में परिभाषित किया गया है। डेटा कन्स्ट्रक्टर के कुछ विशेषज्ञों के लिए यह केवल संभव है। मैं इस तरह के एक समारोह को परिभाषित करने के बारे में पता नहीं लगा सकता। मैंने अपनी समस्या को एक छोटे से उदाहरण में कम करने की कोशिश की है।

सेटअप में प्राकृतिक संख्या की सूचियां शामिल हैं, सूची के सदस्यों को देखने के लिए एक प्रकार के साथ, और सूची सदस्यों को हटाने के लिए एक समारोह शामिल है।

open import Data.Nat 
open import Relation.Binary.Core 

data List : Set where 
    nil : List 
    _::_ : (x : ℕ) -> (xs : List) -> List 

-- membership within a list 
data _∈_ (x : ℕ) : List -> Set where 
    here : forall {xs} -> x ∈ (x :: xs) 
    there : forall {xs y} -> (mem : x ∈ xs) -> x ∈ (y :: xs) 

-- delete 
_\\_ : forall {x} (xs : List) -> (mem : x ∈ xs) -> List 
_\\_ nil() 
_\\_ (_ :: xs) here = xs 
_\\_ (_ :: nil) (there()) 
_\\_ (x :: xs) (there p) = x :: (xs \\ p) 

बस एक त्वरित जांच कि एक सिंगलटन सूची के सिर तत्व को हटाने खाली सूची है:

check : forall {x} -> nil ≡ ((x :: nil) \\ here) 
check = refl 

अब मुझे लगता है कि सूचियों द्वारा अनुक्रमित कुछ आवरण डेटा प्रकार है

-- Our test data type 
data Foo : List -> Set where 
    test : Foo nil 
    test2 : forall {x} (xs : List) -> (mem : x ∈ xs) -> Foo (xs \\ mem) 

test2 कन्स्ट्रक्टर सूची से तत्व को हटाने के परिणामस्वरूप एक सूची और सदस्यता मूल्य लेता है और डेटा प्रकार को अनुक्रमणित करता है।

अब थोड़ा मैं कहाँ अटक कर रहा हूँ मैं निम्नलिखित हस्ताक्षर के एक समारोह चाहते हैं:

foo : Foo nil -> ℕ 
foo = {!!} 

अर्थात, nil को विशेष अपने सूचकांक के साथ एक Foo मूल्य लेने। यह test केस

foo test = 0 

दूसरा मामला मुश्किल है। मैं शुरू में की तरह कुछ कल्पना:

foo : Foo nil -> ℕ 
foo test = 0 
foo (test2 .(_ :: nil) .here) = 1 

लेकिन AGDA शिकायत है कि xs \\ mem != nil of type List when checking that the pattern test2 .(_ :: nil) .here has type Foo nil। तो मैं एक with -clause उपयोग करने की कोशिश:

foo : Foo nil -> ℕ 
foo test = 0 
foo (test2 xs m) with xs \\ m 
... | nil = 1 
... |() 

यह वही त्रुटि अर्जित करता है। मैंने विभिन्न क्रमपरिवर्तनों के साथ प्रयोग किया है, लेकिन हां, मैं इस बात का पता नहीं लगा सकता कि n \\ m = nil पैटर्न में वापस जानकारी का उपयोग कैसे करें। मैंने कई अन्य प्रकार की भविष्यवाणियों की कोशिश की है लेकिन एग्डा को यह बताना नहीं चाहिए कि उसे क्या जानना है। कुछ मदद की बहुत सराहना करेंगे! धन्यवाद।

---

अतिरिक्त: मैं AGDA में एक सबूत लिखा है कि दिए गए किसी भी xs : List और m : x \in xs कि (xs \\ m = nil) का तात्पर्य है कि xs = x :: nil और m = here है, जो की तरह यह प्रकार चेकर को देने के लिए उपयोगी हो सकता है, लेकिन मैं लगता है मुझे यकीन नहीं है कि यह कैसे करें।

data PiEq {A : Set} {B : A -> Set} : (a : A) -> (b : A) -> (c : B a) -> (d : B b) -> Set where 
    pirefl : forall {x : A} {y : B x} -> PiEq {A} {B} x x y y 

check' : forall {x xs m} {eq : xs \\ m ≡ nil} -> (PiEq {List} {\xs -> x ∈ xs} xs (x :: nil) m here) 
check' {xs = nil} {()} 
-- The only case that works 
check' {xs = ._ :: nil} {here} = pirefl 
-- Everything else is refuted 
check' {xs = ._ :: (_ :: xs)} {here} {()} 
check' {xs = ._ :: nil} {there()} 
check' {xs = ._} {there here} {()} 
check' {xs = ._} {there (there m)} {()} 

Answer 1

तरह से आप अपने डेटा प्रकार की स्थापना के साथ

, तुम सच में नहीं कर सकते किसी भी सार्थक तरीके से गैर-तुच्छ सूचकांक वाले मानों पर पैटर्न मिलान। समस्या यह है कि Agda (सामान्य रूप से) xs \\ mem और nil के एकीकरण को हल नहीं कर सकता है।

जिस तरह से पैटर्न मिलान स्थापित किया गया है, आप वास्तव में एकीकरण एल्गोरिदम की सहायता के लिए कोई प्रमाण प्रदान नहीं कर सकते हैं। हालांकि, आप यह सुनिश्चित कर सकते हैं कि इंडेक्स को अप्रतिबंधित छोड़कर और वास्तविक प्रतिबंध का वर्णन करने वाले प्रमाण के साथ एक और पैरामीटर का उपयोग करके पैटर्न मिलान कार्य करता है। इस तरह, आप पैटर्न पैटर्न कर सकते हैं और फिर असंभव मामलों को खत्म करने के लिए सबूत का उपयोग कर सकते हैं।

तो, बजाय केवल foo होने के, हम अतिरिक्त पैरामीटर के साथ एक और समारोह (माना foo-helper) होगा:

foo-helper : ∀ {xs} → xs ≡ nil → Foo xs → ℕ 
foo-helper p test = 0 
foo-helper p (test2 ys mem) with ys \\ mem 
foo-helper p (test2 _ _) | nil = 1 
foo-helper () (test2 _ _) | _ :: _ 

आप तो बस एक सबूत उपलब्ध कराने के द्वारा मूल कार्य ठीक हो सकता है कि nil ≡ nil:

foo : Foo nil → ℕ 
foo = foo refl 

---

आप अक्सर मिलान पैटर्न इस तरह का कर रही आशा, तो इसके बजाय बदलने के लिए फायदेमंद हो सकता है डेटा प्रकार की परिभाषा:

data Foo′ : List → Set where 
    test′ : Foo′ nil 
    test2′ : ∀ {x} xs ys → (mem : x ∈ xs) → ys ≡ xs \\ mem → Foo′ ys 

इस तरह, आप हमेशा पैटर्न मैच है क्योंकि आप जटिल सूचकांक की जरूरत नहीं है और अभी तक किसी भी असंभव मामलों शामिल सबूत के लिए धन्यवाद समाप्त कर सकते हैं। हम इस परिभाषा के साथ foo लिखना चाहते हैं, तो हम भी एक सहायक समारोह की जरूरत नहीं है:

foo′ : Foo′ nil → ℕ 
foo′ test′ = 0 
foo′ (test2′ xs .nil mem _) with xs \\ mem 
foo′ (test2′ _ ._ _ _) | nil = 1 
foo′ (test2′ _ ._ _()) | _ :: _ 

---

और पता चलता है कि इन दो डेटा प्रकार के होते हैं (तार्किक) बराबर:

to : ∀ {xs} → Foo xs → Foo′ xs 
to test = test′ 
to (test2 xs mem) = test2′ xs (xs \\ mem) mem refl 

from : ∀ {xs} → Foo′ xs → Foo xs 
from test′ = test 
from (test2′ xs .(xs \\ mem) mem refl) = test2 xs mem 

Answer 2

foo

foo : Foo nil -> ℕ 
foo _ = 0 

से क्यों परिभाषित नहीं: मैं अनुकरणीय प्रकार पर एक pointwise समानता है कि निर्भरता जो मामलों पेचीदा का सम्मान करता है लागू करने के लिए था?

नोट: AGDA की वर्तमान विकास संस्करण (https://github.com/agda/agda/commit/06fe137dc7d7464b7f8f746d969250bbd5011489) का उपयोग करना मैं त्रुटि

I'm not sure if there should be a case for the constructor test2, 
because I get stuck when trying to solve the following unification 
problems (inferred index ≟ expected index): 
    xs \\ mem ≟ nil 
when checking the definition of foo 

मिला जब मैं लिखने

foo test = 0