इदरिस: विशिष्ट शब्दों असंभव है सबूत है कि

Question

इदरिस संस्करण: 0.9.16

---

मैं एक base मूल्य और एक दोहराया step समारोह से उत्पन्न निर्माण का वर्णन करने का प्रयास कर रहा हूँ:

namespace Iterate 
    data Iterate : (base : a) -> (step : a -> a) -> a -> Type where 
    IBase : Iterate base step base 
    IStep : Iterate base step v -> Iterate base step (step v) 

इस मैं यह कर सकते हैं का उपयोग करना Plus परिभाषित करें, jump के पुनरावृत्त परिवर्धन से संरचनाओं का वर्णन:

namespace Plus 
    Plus : (base : Nat) -> (jump : Nat) -> Nat -> Type 
    Plus base jump = Iterate base (\v => jump + v) 

सरल उदाहरण इस बात का उपयोग करता है:

namespace PlusExamples 
    Even : Nat -> Type; Even = Plus 0 2 
    even0 : Even 0; even0 = IBase 
    even2 : Even 2; even2 = IStep even0 
    even4 : Even 4; even4 = IStep even2 

    Odd : Nat -> Type; Odd = Plus 1 2 
    odd1 : Odd 1; odd1 = IBase 
    odd3 : Odd 3; odd3 = IStep odd1 

    Fizz : Nat -> Type; Fizz = Plus 0 3 
    fizz0 : Fizz 0; fizz0 = IBase 
    fizz3 : Fizz 3; fizz3 = IStep fizz0 
    fizz6 : Fizz 6; fizz6 = IStep fizz3 

    Buzz : Nat -> Type; Buzz = Plus 0 5 
    buzz0 : Buzz 0; buzz0 = IBase 
    buzz5 : Buzz 5; buzz5 = IStep buzz0 
    buzz10 : Buzz 10; buzz10 = IStep buzz5 

निम्नलिखित वर्णन करता है कि base नीचे मान असंभव हैं:

noLess : (base : Nat) -> 
      (i : Fin base) -> 
      Plus base jump (finToNat i) -> 
      Void 
    noLess Z  FZ  m  impossible 
    noLess (S b) FZ  IBase impossible 
    noLess (S b) (FS i) IBase impossible 

और base और jump + base के बीच मूल्यों के लिए निम्नलिखित:

noBetween : (base : Nat) -> 
       (predJump : Nat) -> 
       (i : Fin predJump) -> 
       Plus base (S predJump) (base + S (finToNat i)) -> 
       Void 
    noBetween b Z  FZ  m  impossible 
    noBetween b (S s) FZ  IBase impossible 
    noBetween b (S s) (FS i) IBase impossible 

---

मैं मुसीबत निम्नलिखित समारोह को परिभाषित कर रहा हूँ:

noJump : (Plus base jump n -> Void) -> Plus base jump (jump + n) -> Void 
noJump f m = ?noJump_rhs 

यही कारण है: अगर nbase नहीं है प्लस jump का एक स्वाभाविक कई है, तो न jump + n है।

अगर मैं m विभाजित करने के लिए इडिस से पूछता हूं तो यह केवल मुझे IBase दिखाता है - तो मैं अटक जाता हूं।

क्या कोई मुझे सही दिशा में इंगित करेगा?

---

संपादित करें 0: लागू करने inductionm करने के लिए मुझे निम्न संदेश देता है:

Induction needs an eliminator for Iterate.Iterate.Iterate 

---

संपादित करें 1: नाम अद्यतन और यहाँ स्रोत की एक प्रति है: http://lpaste.net/125873

Answer 1

करने के लिए संपादित करें 0:

%elim data Iterate = <your definition> 

मुख्य प्रश्न करने के लिए:: एक प्रकार पर शामिल करने, यह एक विशेष क्वालीफायर की जरूरत है खेद है कि मैं अपने सभी कोड के माध्यम से नहीं पढ़ा है, मैं सिर्फ कुछ सुझाव बनाना चाहते झूठी सबूत के लिए। मेरे अनुभव से (मैंने कुछ मदद जानने के लिए मानक लाइब्रेरी स्रोतों को भी हल किया), जब आपको Not a (a -> Void) साबित करने की आवश्यकता होती है, तो आप अक्सर Not b (b -> Void) का उपयोग कर सकते हैं और a से b को परिवर्तित करने का एक तरीका, फिर बस इसे पास कर सकते हैं दूसरे सबूत के लिए।उदाहरण के लिए, एक बहुत ही सरल सबूत एक सूची है कि एक और का उपसर्ग ही वे अलग सिर नहीं किया जा सकता है:

%elim data Prefix : List a -> List a -> Type where 
    pEmpty : Prefix Nil ys 
    pNext : Prefix xs ys -> Prefix (x :: xs) (x :: ys) 

prefixNotCons : Not (x = y) -> Not (Prefix (x :: xs) (y :: ys)) 
prefixNotCons r (pNext _) = r refl 

आपके मामले में, मैं तुम्हें कई प्रमाण और गठबंधन करने के लिए की जरूरत है लगता है।