Coq जटिल पैटर्न-मिलान लिखने की अनुमति देता है, लेकिन फिर यह उन्हें विघटित कर देता है ताकि इसका कर्नेल उन्हें संभाल सके।

उदाहरण के लिए, आइए निम्नलिखित कोड पर विचार करें।

Require Import List. Import ListNotations.

Inductive bar := A | B | C.

Definition f (l : list bar) :=
  match l with
  | _ :: A :: _ => 1
  | _ => 2
  end.

हम सूची और दूसरे तत्व दोनों पर पैटर्न-मिलान करते हैं। मुद्रण f से पता चलता है कि Coq इसका अधिक जटिल संस्करण संग्रहीत करता है।

Print f.
(* f = fun l : list bar => match l with
                        | [] => 2
                        | [_] => 2
                        | _ :: A :: _ => 1
                        | _ :: B :: _ => 2
                        | _ :: C :: _ => 2
                        end
     : list bar -> nat
*)

समस्या यह है कि, f में हेर-फेर करने वाले सबूतों में, मुझे केवल २ के बजाय ५ मामलों से निपटना पड़ता है, और उनमें से ४ बेमानी हैं।

इससे निपटने का सबसे अच्छा तरीका क्या है? क्या पैटर्न-मिलान के साथ तर्क करने का कोई तरीका है जैसे कि यह बिल्कुल परिभाषित किया गया हो?

coq
2
eponier 17 सितंबर 2019, 16:45

1 उत्तर

सबसे बढ़िया उत्तर

आप सही हैं कि Coq वास्तव में पैटर्न-मिलान को सरल बनाता है जिससे बहुत सारी अतिरेक दिखाई देती हैं। हालांकि, मामले के विश्लेषण पर तर्क करने के कुछ तरीके हैं जिनका आप मतलब विरोध करते हैं जो Coq समझता है।

  • Function और फंक्शन इंडक्शन एक तरीका है।
  • अभी हाल ही में, समीकरण आपको पैटर्न-मिलान को परिभाषित करने की भी अनुमति देता है जिसके लिए यह स्वचालित रूप से प्रेरण सिद्धांतों को प्राप्त करता है ( कि आप funelim) का उपयोग करके आह्वान कर सकते हैं। यह समझाने के लिए कि coq मामलों को कारक बनाया जा सकता है, आपको दृष्टिकोण की धारणा का उपयोग करना होगा। उनका वर्णन समीकरणों के संदर्भ में किया गया है उदाहरणों में। मैं विस्तार से बताऊंगा कि आपके उदाहरण को इसके लिए कैसे अनुकूलित किया जाए।
From Equations Require Import Equations.
Require Import List. Import ListNotations.

Inductive bar := A | B | C.

Equations discr (b : list bar) : Prop :=
  discr (_ :: A :: _) := False ;
  discr _ := True.

Inductive view : list bar -> Set :=
| view_foo : forall x y, view (x :: A :: y)
| view_other : forall l, discr l -> view l.

Equations viewc l : view l :=
    viewc (x :: A :: y) := view_foo x y ;
    viewc l := view_other l I.

Equations f (l : list bar) : nat :=
    f l with viewc l := {
    | view_foo _ _ => 1 ;
    | view_other _ _ => 2
    }.

Goal forall l, f l < 3.
Proof.
    intro l.
    funelim (f l).
    - repeat constructor.
    - repeat constructor.
Qed.

जैसा कि आप देख सकते हैं, funelim केवल दो उप-लक्ष्य उत्पन्न करता है।

यह थोड़ा भारी हो सकता है इसलिए यदि आप फ़ंक्शन के समीकरणों का उपयोग नहीं करना चाहते हैं, तो आपको अपने स्वयं के प्रेरण सिद्धांतों को हाथ से साबित करना पड़ सकता है:

Require Import List. Import ListNotations.

Inductive bar := A | B | C.

Definition f (l : list bar) :=
  match l with
  | _ :: A :: _ => 1
  | _ => 2
  end.

Definition discr (l : list bar) : Prop :=
    match l with
    | _ :: A :: _ => False
    | _ => True
    end.

Lemma f_ind :
    forall (P : list bar -> nat -> Prop),
        (forall x y, P (x :: A :: y) 1) ->
        (forall l, discr l -> P l 2) ->
        forall l, P l (f l).
Proof.
    intros P h1 h2 l.
    destruct l as [| x [|[] l]].
    3: eapply h1.
    all: eapply h2.
    all: exact I.
Qed.

Goal forall l, f l < 3.
Proof.
    intro l.
    eapply f_ind.
    - intros. repeat constructor.
    - intros. repeat constructor.
Qed.
5
Théo Winterhalter 17 सितंबर 2019, 14:29