पहले साबित प्रमेय का परिचय परिकल्पना

Question

मान लीजिए कि मैंने पहले से ही कॉक में कुछ प्रमेय साबित कर दिया है, और बाद में मैं इसे किसी अन्य प्रमेय के प्रमाण में एक परिकल्पना के रूप में पेश करना चाहता हूं। क्या ऐसा करने का एक संक्षिप्त तरीका है?

इसकी आवश्यकता आमतौर पर मेरे लिए उत्पन्न होती है जब मैं मामलों के सबूत की तरह कुछ करना चाहता हूं। और मैंने पाया है कि ऐसा करने का एक तरीका assert प्रमेय का बयान है, और फिर तुरंत साबित करें, लेकिन यह बहुत ही बोझिल लगता है। उदाहरण के लिए मैं जैसी चीजों के बारे में करते हैं:

Require Import Arith.EqNat. 

Definition Decide P := P \/ ~P. 

Theorem decide_eq_nat: forall x y: nat, Decide (x = y). 
Proof. 
    intros x y. remember (beq_nat x y) as b eqn:E. destruct b. 
    left. apply beq_nat_eq. assumption. 
    right. apply beq_nat_false. symmetry. assumption. Qed. 

Theorem silly: forall x y: nat, x = y \/ x <> y. 
Proof. 
    intros x y. 
    assert (Decide (x = y)) as [E|N] by apply decide_eq_nat. 
    left. assumption. 
    right. assumption. Qed. 

लेकिन वहाँ पूरे assert [statement] by apply [theorem] बात टाइप करने के लिए की तुलना में एक आसान तरीका है?

Answer 1

आप pose proof theorem_name as X. का उपयोग कर सकते हैं, जहां X वह नाम है जिसे आप पेश करना चाहते हैं।

---

आप अभी संहार करने जा रहे हैं, तो आप भी कर सकते हैं: destruct (decide_eq_nat x y).