मैं साबित करने के लिएकोक में समानता के दोनों किनारों पर एक फ़ंक्शन लागू करें?
Theorem evenb_n__oddb_Sn : ∀n : nat,
evenb n = negb (evenb (S n)).
कि मैं n पर प्रेरण उपयोग कर रहा हूँ कोशिश कर Coq में हूँ। आधार मामले तुच्छ है, इसलिए मैं आगमनात्मक मामले में हूँ और मेरा लक्ष्य लगता है:
k : nat
IHk : evenb k = negb (evenb (S k))
============================
evenb (S k) = negb (evenb (S (S k)))
अब निश्चित रूप से वहाँ है कि इस बात पर ज़ोर
a = b -> f a = f b
सभी कार्यों f : A -> B के लिए कार्यों की एक मौलिक स्वयंसिद्ध है। इसलिए मैं दोनों पक्षों, जो मुझे देना होगा करने के लिए आवेदन कर सकता है negb
k : nat
IHk : evenb k = negb (evenb (S k))
============================
negb (evenb (S k)) = negb (negb (evenb (S (S k))))
कौन सा मुझे दाएं से बाएं मेरी आगमनात्मक परिकल्पना का उपयोग करते हैं होता है, सही एक दूसरे को रद्द होगा, और evenb की defintion पर negations होगा सबूत पूरा करें।
अब, इस विशेष प्रमेय को साबित करने का एक बेहतर तरीका हो सकता है (संपादित करें: मैंने इसे एक और तरीका किया है), लेकिन जैसा कि सामान्य रूप से ऐसा करने के लिए उपयोगी चीज लगता है, समानता को संशोधित करने का तरीका क्या है दोनों पक्षों के लिए एक समारोह लागू करके Coq में लक्ष्य?
नोट: मुझे एहसास है कि यह किसी भी मनमाने ढंग से कार्य के लिए काम नहीं करेगा: उदाहरण के लिए, आप -1 = 1 को दोनों पक्षों को abs लागू करके साबित करने के लिए इसका उपयोग कर सकते हैं। हालांकि, यह किसी भी इंजेक्शन समारोह के लिए है (एक जिसके लिए f a = f b -> a = b), जो negb है। शायद पूछने के लिए एक बेहतर सवाल है, तो, एक प्रस्ताव दिया जाता है जो प्रस्ताव पर चलता है (उदाहरण के लिए, negb x = negb y -> x = y), मैं वर्तमान कार्य को संशोधित करने के लिए उस फ़ंक्शन का उपयोग कैसे कर सकता हूं?