coq
किसी मौजूदा तथ्य के लिए खोज और वेरिएंट के साथ खोज करना

वाक्य - विन्यास

• Search qualid. (* Coq 8.4 और नए संस्करणों के लिए *)
• SearchAbout qualid. (* पदावनत समानार्थी। *)

पैरामीटर

टिप्पणियों

किसी विशेष पहचानकर्ता के बारे में तथ्य

सभी को शामिल तथ्यों को देखने के लिए le प्रस्तावना से संबंध:

Coq < Search le.
le_n: forall n : nat, n <= n
le_S: forall n m : nat, n <= m -> n <= S m
...
max_l: forall n m : nat, m <= n -> Nat.max n m = n
max_r: forall n m : nat, n <= m -> Nat.max n m = m
...

संकेतन से जुड़े सभी तथ्यों के बारे में जानने के लिए < :

Coq < Search "<".
exists_lt: forall (Q : nat -> Prop) (k l : nat), exists_between Q k l -> k < l
in_int_intro: forall p q r : nat, p <= r -> r < q -> in_int p q r
in_int_lt: forall p q r : nat, in_int p q r -> p < q
...

एक पैटर्न के लिए खोज

एक परिकल्पना या निष्कर्ष में एक पैटर्न को शामिल करने वाले सभी तथ्यों की खोज करें:

Coq < Search (_ + O).
plus_n_O: forall n : nat, n = n + 0

_ वर्ण वाइल्डकार्ड के रूप में कार्य करता है, इसे कई बार उपयोग किया जा सकता है:

Coq < Search (S _ <= _).
le_S_n: forall n m : nat, S n <= S m -> n <= m
le_n_S: forall n m : nat, n <= m -> S n <= S m

आप गैर-रेखीय पैटर्न भी खोज सकते हैं:

Coq < Search (?x <= ?x).
le_n: forall n : nat, n <= n

एक लेम्मा के निष्कर्ष में एक पैटर्न की खोज

जब आप जानते हैं कि एक लेम्मा की खोज करें तो इसका निष्कर्ष क्या होना चाहिए:

Coq < SearchPattern (S _ <= _).
le_n_S: forall n m : nat, n <= m -> S n <= S m

आप आंशिक निष्कर्ष (निष्कर्ष और एक या कई अंतिम परिकल्पना) पर भी खोज कर सकते हैं।

Coq < Require Import Arith.
Coq < SearchPattern (?x <= ?y -> ?y <= _ -> ?x <= _).
Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p

चेतावनी: यदि आप परिकल्पना के क्रम को मिलाते हैं, तो आपको कुछ भी नहीं मिलेगा:

Coq < SearchPattern (?y <= _ -> ?x <= ?y -> ?x <= _).