Coq

Question

में तो किसी और प्रमाणन

मैं Coq पर नया हूँ और मैं कुछ बहुत बुनियादी साबित करने के लिए कोशिश कर रहा हूँ

लेम्मा eq_if_eq: A1, A2 forall, (यदि ए 1 ए 2 तब a2 बाकी a1 beq_nat) = A1 ।

मैंने नीचे पोस्ट किए गए एक समाधान के माध्यम से संघर्ष किया, लेकिन मुझे लगता है कि एक बेहतर तरीका होना चाहिए। आदर्श रूप में, मैं परिकल्पना की सूची में केस मान डालते समय beq_nat a1 a2 पर साफ़ रूप से केस करना चाहता हूं। क्या कोई रणनीति t है कि t (beq_nat a1 a2) का उपयोग दो उप-उपज उत्पन्न करता है, एक जहां beq_nat a1 a2 = true और दूसरा beq_nat a1 a2 = false? जाहिर है, induction बहुत करीब है लेकिन यह अपना इतिहास खो देता है।

यहाँ सबूत मैं के माध्यम से संघर्ष किया है:

Proof. 
Hint Resolve beq_nat_refl. 
Hint Resolve beq_nat_eq. 
Hint Resolve beq_nat_true. 
Hint Resolve beq_nat_false. 
intros. 
compare (beq_nat a1 a2) true. 
intros. assert (a1 = a2). auto. 
replace (beq_nat a1 a2) with true. auto. 
intros. assert (a1 <> a2). apply beq_nat_false. 
apply not_true_is_false. auto. 
assert (beq_nat a1 a2 = false). apply not_true_is_false. auto. 
replace (beq_nat a1 a2) with false. auto. 
Qed. 

Answer 1

यह आसान है remember रणनीति मुझे बस चाहिए था। remember (beq_nat a1 a2) as e; induction e; etc की लाइनों के साथ कुछ।

Answer 2

आम तौर पर चीजों की इस प्रकार के लिए, मैं विनाश की eqn संस्करण का उपयोग करें। यह इस तरह दिखेगा:

destruct (beq_nat a1 a2) as []_eqn. (* Coq <= 8.3 *) 

destruct (beq_nat a1 a2) as []eqn:? (* Coq >= 8.4 *) 

यह समानता को एक परिकल्पना के रूप में जोड़ देगा। 8.4 संस्करण में, आप परिकल्पना देने के लिए नाम के साथ प्रश्न चिह्न को प्रतिस्थापित कर सकते हैं।

Answer 3

जो रणनीति आप पूछ रहे हैं वह case_eq है। निम्न स्क्रिप्ट 8.4pl3:

intros. 
case_eq (beq_nat a1 a2). 
intuition. 
apply beq_nat_true_iff in H. 
intuition. 
intuition. 

में लेम्मा साबित करती है