मैं वर्तमान में उलझन में हूं कि निम्नलिखित प्रमेय को कैसे सिद्ध किया जाए: Theorem excluded_middle2 : (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P). मैं यहाँ फंस गया हूँ: Theorem excluded_middle2 : (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P). Proof. i....
25 पद 2021, 13:17
आगमनात्मक प्रस्तावों पर तार्किक नींव के अध्याय में, अभ्यास exp_match_ex1 में निम्नलिखित परिभाषाएं शामिल हैं: Inductive reg_exp (T : Type) : Type := | EmptySet | EmptyStr | Char (t : T) | App (r1 r2 : reg_exp T) | Union (r1 r2 : reg_exp T) | Star (r : reg_exp T). Arguments EmptySet {T}. ....
11 सितंबर 2021, 18:21
मैं Logical Foundations' से अभ्यासों की श्रृंखला le_exercises को पूरा करने का प्रयास कर रहा हूं। आगमनात्मक प्रस्तावों पर अध्याय। यह श्रृंखला ज्यादातर आगमनात्मक संबंध le पर आधारित है, जिसे इस प्रकार परिभाषित किया गया है: Inductive le : nat -> nat -> Prop := | le_n (n : nat) : le n n....
5 सितंबर 2021, 17:27
2 मैं सॉफ्टवेयर नींव के माध्यम से जा रहा हूँ और एक त्रुटि में भाग गया। (https://softwarefoundations.cis.upenn.edu/lf-current/Maps .html) From Coq Require Import Arith.Arith. From Coq Require Import Bool.Bool. Require Export Coq.Strings.String. From Coq Require Import Logic.FunctionalExtensional....
6 अप्रैल 2021, 13:58
लॉजिकल फ़ाउंडेशन से IndProp.v में हमारे पास निम्नलिखित प्रेरक गुण हैं: Inductive nostutter {X:Type} : list X -> Prop := | nos_nil : nostutter [] | nos_one : forall x, nostutter [x] | nos_cons : forall x h l, nostutter (h :: l) -> (x <> h) -> (nostutter (x :: h :: l)). क्या इसे हल करना संभव है....
23 मार्च 2021, 00:18
मैं यह पता लगाने की कोशिश कर रहा हूं कि टर्मिनल से चलने पर एलएफ टेस्ट स्क्रिप्ट मैन्युअल रूप से ग्रेडेड असाइनमेंट कैसे आउटपुट करती है। उदाहरण के लिए, यदि आप Induction.v को देखते हैं, तो plus_comm_informal नामक एक अभ्यास है, मैं अपने द्वारा लिखी गई टिप्पणियों या सामग्री को लेने के लिए परीक्षण स्क्रि....
28 अक्टूबर 2020, 19:59
सॉफ्टवेयर फाउंडेशन से क्विक चिक कोर्स पास करना मैं निम्नलिखित प्रमेय पर अटका हुआ हूं: Class Eq A := { eqb: A -> A -> bool; }. Instance eqBoolArrowA {A : Type} `{Eq A} : Eq (bool -> A) := { eqb f1 f2 := (andb (eqb (f1 false) (f2 false)) (eqb (f1 true) (f2 true))) }. Theorem eqBool....
10 अक्टूबर 2020, 10:26
कार्य: प्राकृतिक संख्याओं को बाइनरी संख्याओं में बदलने के लिए एक फ़ंक्शन लिखें। Inductive bin : Type := | Z | A (n : bin) | B (n : bin). (* Division by 2. Returns (quotient, remainder) *) Fixpoint div2_aux (n accum : nat) : (nat * nat) := match n with | O => (accum, O) | S O => (accum, ....
12 अगस्त 2020, 23:18
सॉफ्टवेयर फाउंडेशन "क्विकचिक" के खंड 4 में हमारे पास निम्नलिखित अभ्यास है: Class Ord A `{Eq A} : Type := { le : A -> A -> bool }. (* Define [Ord] instances for options and pairs. *) (* So I am trying to do it *) Instance optionOrd {A : Type} `{Ord A} `{Eq (option A)} : Ord (option A) := { le....
7 अगस्त 2020, 00:11
काम। मान लीजिए हम Coq को निम्नलिखित परिभाषा देते हैं: Inductive R2 : nat -> list nat -> Prop := | c1 : R2 0 [] | c2 : forall n l, R2 n l -> R2 (S n) (n :: l) | c3 : forall n l, R2 (S n) l -> R2 n l. निम्नलिखित में से कौन से प्रस्ताव सिद्ध हैं? मैंने 3 में से 2 साबित किया। Example Example_R21 : R2 2....
30 जुलाई 2020, 19:31
Theorem ev_ev__ev_full : forall n m, even (n+m) <-> (even n <-> even m). Proof. intros n m. split. - intros H. split. + intros H1. apply (ev_ev__ev n m H H1). + intros H1. rewrite plus_comm in H. apply (ev_ev__ev m n H H1). - intros H. आउटपुट: n, m : nat H : even n <-> even m ....
29 जुलाई 2020, 00:25
Theorem ev_plus_plus : forall n m p, even (n+m) -> even (n+p) -> even (m+p). Proof. intros n m p Hnm Hnp. हमें यह मिलता है: 1 subgoal (ID 189) n, m, p : nat Hnm : even (n + m) Hnp : even (n + p) ============================ even (m + p) इसके अलावा हमारे पास पहले से सिद्ध प्रमेय है....
28 जुलाई 2020, 23:13
तार्किक नींव से रिले अध्याय। मुझे उस एक्सर्साइज़ का समाधान दिया गया था जिसे मैं समझने की कोशिश कर रहा हूँ: Definition antisymmetric {X: Type} (R: relation X) := forall a b : X, (R a b) -> (R b a) -> a = b. Theorem le_antisymmetric : antisymmetric le. Proof. unfold antisymmetric. intros a b [....
21 अक्टूबर 2019, 01:41
मैं इस बिंदु पर आया: Theorem le_antisymmetric : antisymmetric le. Proof. unfold antisymmetric. intros a b H1 H2. generalize dependent a. induction b as [|b' IH]. - intros. inversion H1. reflexivity. - intros. आउटपुट: b' : nat IH : forall a : nat, a <= b' -> b' <= a -> a = b' a : nat H1 : ....
16 सितंबर 2019, 00:22
नोस्टटर एक्सर्साइज़ के साथ खेलते हुए मुझे एक और अजीब व्यवहार मिला। यहाँ कोड है: Inductive nostutter {X:Type} : list X -> Prop := | ns_nil : nostutter [] | ns_one : forall (x : X), nostutter [x] | ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t). Examp....
2 जुलाई 2019, 01:48
@keep_learning के उत्तर को समझने की कोशिश करते हुए मैंने इस कोड को चरण दर चरण पढ़ा: Inductive nostutter {X:Type} : list X -> Prop := | ns_nil : nostutter [] | ns_one : forall (x : X), nostutter [x] | ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t). Ex....
1 जुलाई 2019, 02:21
test_nostutter_1 एक्सर्साइज़ में गहराई से गोता लगाने से मुझे इसे बिना दोहराए हल करने का एक तरीका मिल गया: Example test_nostutter_1: nostutter [3;1;4;1;5;6]. Proof. constructor 3. (* This will apply the tactics to the 2-nd subgoal *) 2: {apply eqb_neq. auto. } constructor 3. 2: {apply eqb_n....
27 जून 2019, 17:41
किताब के लेखकों ने कुछ यूनिट परीक्षणों के लिए नोस्टटर अभ्यास के लिए सबूत प्रदान किए हैं। दुर्भाग्य से, उन्होंने स्पष्टीकरण नहीं दिया कि वे कैसे काम करते हैं। मैं सभी सबूतों को समझने में सक्षम था लेकिन एक: Inductive nostutter {X:Type} : list X -> Prop := | ns_nil : nostutter [] | ns_one : forall (x....
26 जून 2019, 14:45
Lemma re_not_empty_correct : forall T (re : @reg_exp T), (exists s, s =~ re) <-> re_not_empty re = true. Proof. split. - admit. (* I proved it myself *) - intros. induction re. + simpl in H. discriminate H. + exists []. apply MEmpty. + exists [t]. apply MChar. + simpl in H. r....
21 जून 2019, 13:10
IndProp से leb_complete प्रमेय के साथ खेलने पर मुझे निम्नलिखित विचित्रताएँ मिलीं: Theorem leb_complete : forall n m, n <=? m = true -> n <= m. Proof. induction n as [|n']. - intros. apply O_le_n. - induction m as [| m'] eqn:Em. + intros H. discriminate H. + intros H. apply n_le_m__Sn....
10 जून 2019, 00:41
मैं निम्नलिखित लेम्मा साबित करने की कोशिश कर रहा हूँ: Inductive even : nat → Prop := | ev_0 : even 0 | ev_SS (n : nat) (H : even n) : even (S (S n)). Lemma even_Sn_not_even_n : forall n, even (S n) <-> not (even n). Proof. intros n. split. + intros H. unfold not. intros H1. induction H1 as ....
29 मई 2019, 00:59
(** **** Exercise: 3 stars, standard, optional (ev_plus_plus) This exercise just requires applying existing lemmas. No induction or even case analysis is needed, though some of the rewriting may be tedious. *) Theorem ev_plus_plus : forall n m p, even (n+m) -> even (n+p) -> even (m+....
25 मई 2019, 23:16
यहाँ पुस्तक से कार्य है: सामान्य बहिष्कृत मध्य स्वयंसिद्ध के साथ Coq की संगति साबित करना जटिल तर्क की आवश्यकता होती है जिसे Coq . के भीतर नहीं किया जा सकता है अपने आप। हालांकि, निम्नलिखित प्रमेय का तात्पर्य है कि यह हमेशा सुरक्षित रहता है एक निर्णायकता स्वयंसिद्ध मानने के लिए (यानी, बहिष्क....
22 मई 2019, 01:18
सॉफ्टवेयर फाउंडेशन की ओर से यह 5 सितारा अभ्यास है। Lemma pumping : forall T (re : @reg_exp T) s, s =~ re -> pumping_constant re <= length s -> exists s1 s2 s3, s = s1 ++ s2 ++ s3 /\ s2 <> [] /\ forall m, s1 ++ napp m s2 ++ s3 =~ re. Proof. intros T re s Hmatch. induction Hmatch....
6 मई 2019, 20:23
Theorem evenb_double_conv : forall n, exists k, n = if evenb n then double k else S (double k). Proof. (* Hint: Use the [evenb_S] lemma from [Induction.v]. *) intros n. induction n as [|n' IHn']. - simpl. exists O. simpl. reflexivity. - rewrite -> evenb_S. destruct (evenb n....
5 मई 2019, 18:56