कोक में कस्टम प्रेरण सिद्धांत का उपयोग कैसे करें?

Question

मैंने पढ़ा है कि एक प्रकार के लिए प्रेरण सिद्धांत सिर्फ P प्रस्ताव के बारे में एक प्रमेय है। इसलिए मैंने दाएं (या रिवर्स) सूची कन्स्ट्रक्टर के आधार पर List के लिए एक प्रेरण सिद्धांत बनाया।

Definition rcons {X:Type} (l:list X) (x:X) : list X := 
    l ++ x::nil. 

प्रेरण सिद्धांत ही है:

Definition true_for_nil {X:Type}(P:list X -> Prop) : Prop := 
    P nil. 

Definition true_for_list {X:Type} (P:list X -> Prop) : Prop := 
    forall xs, P xs. 

Definition preserved_by_rcons {X:Type} (P: list X -> Prop): Prop := 
    forall xs' x, P xs' -> P (rcons xs' x). 

Theorem list_ind_rcons: 
    forall {X:Type} (P:list X -> Prop), 
    true_for_nil P -> 
    preserved_by_rcons P -> 
    true_for_list P. 
Proof. Admitted. 

लेकिन अब, मैं मुसीबत प्रमेय का उपयोग हो रहा है। मैं इसे induction रणनीति के रूप में प्राप्त करने के लिए कैसे आमंत्रित नहीं करता हूं।

उदाहरण के लिए, मैंने कोशिश की:

Theorem rev_app_dist: forall {X} (l1 l2:list X), rev (l1 ++ l2) = rev l2 ++ rev l1. 
Proof. intros X l1 l2. 
    induction l2 using list_ind_rcons. 

लेकिन अंतिम पंक्ति में, मुझे मिल गया:

Error: Cannot recognize an induction scheme. 

को परिभाषित करने और list_ind_rcons की तरह एक कस्टम प्रेरण सिद्धांत लागू करने के लिए सही क्या कदम उठाएँ?

धन्यवाद

Answer 1

आपने जो किया वह अधिकतर सही था। समस्या यह है कि कोक को मध्यस्थ परिभाषाओं के कारण, जो लिखा है वह एक प्रेरण सिद्धांत है। यह, उदाहरण के लिए, बस ठीक काम करता है:

Theorem list_ind_rcons: 
    forall {X:Type} (P:list X -> Prop), 
    P nil -> 
    (forall x l, P l -> P (rcons l x)) -> 
    forall l, P l. 
Proof. Admitted. 

Theorem rev_app_dist: forall {X} (l1 l2:list X), rev (l1 ++ l2) = rev l2 ++ rev l1. 
Proof. intros X l1 l2. 
    induction l2 using @list_ind_rcons. 

मैं अगर Coq स्वचालित रूप से मध्यवर्ती परिभाषाएँ एक बग या नहीं माना जाना चाहिए प्रकट करने में सक्षम नहीं किया जा रहा है पता नहीं है, लेकिन कम से कम वहाँ एक समाधान नहीं है।

Answer 2

एक मध्यवर्ती परिभाषाओं की रक्षा करना चाहते हैं, तो एक Section तंत्र इतना की तरह इस्तेमाल कर सकते हैं,:

Require Import Coq.Lists.List. Import ListNotations. 

Definition rcons {X:Type} (l:list X) (x:X) : list X := 
    l ++ [x]. 

Section custom_induction_principle.  
    Variable X : Type. 
    Variable P : list X -> Prop. 

    Hypothesis true_for_nil : P nil. 
    Hypothesis true_for_list : forall xs, P xs. 
    Hypothesis preserved_by_rcons : forall xs' x, P xs' -> P (rcons xs' x). 

    Fixpoint list_ind_rcons (xs : list X) : P xs. Admitted. 
End custom_induction_principle. 

Coq परिभाषाओं विकल्प और list_ind_rcons जरूरत के प्रकार और induction ... using ... काम करता है:

Theorem rev_app_dist: forall {X} (l1 l2:list X), 
    rev (l1 ++ l2) = rev l2 ++ rev l1. 
Proof. intros X l1 l2. 
    induction l2 using list_ind_rcons. 
Abort. 

वैसे, यह प्रेरण सिद्धांत मानक पुस्तकालय (List मॉड्यूल) में मौजूद है:

Coq < Check rev_ind. 
rev_ind 
    : forall (A : Type) (P : list A -> Prop), 
     P [] -> 
     (forall (x : A) (l : list A), P l -> P (l ++ [x])) -> 
     forall l : list A, P l