कॉक में अंतिम परिचय?

Question

मैं कोशिश कर रहा हूँ (प्रतिष्ठित) साबित

~ (forall t : U, phi) -> exists t: U, ~phi 

Coq में

। मुझे क्या करना कोशिश कर रहा हूँ यह contrapositively साबित है:

1. Assume there is no such t (so ~(exists t: U, ~phi)) 

2. Choose arbitrary t0:U 

3. If ~phi[t/t0], then contradiction with (1) 

4. Therefore, phi[t/t0] 

5. Conclude (forall t:U, phi) 

मेरे समस्या लाइनों के साथ है (2) और (5)। मैं यू के मनमानी तत्व को चुनने के लिए कैसे समझ सकता हूं, के बारे में कुछ साबित करता हूं, और एक निष्कर्ष निकाला जाता हूं।

कोई सुझाव (मैं contrapositive का उपयोग करने के लिए प्रतिबद्ध नहीं हूँ)?

Answer 1

अपने अनौपचारिक प्रमाण की नकल करने के लिए, मैं क्लासिक एक्सिसॉम ¬¬P → पी (जिसे एनएनपीपी कहा जाता है) [1] का उपयोग करता हूं। इसे लागू करने के बाद, आपको False दोनों को ए: ¬ (∀ x: U, φ x) और बी: ¬ (∃ x: U, φ x) के साथ साबित करने की आवश्यकता है। ए और बी False को कम करने के लिए आपके एकमात्र हथियार हैं। आइए ए [2] आज़माएं। तो आपको साबित करना होगा कि ∀ एक्स: यू, φ एक्स। ऐसा करने के लिए, हम एक मनमाना टी लेते हैं और यह साबित करने का प्रयास करते हैं कि φ t₀ [3] रखता है। अब, चूंकि आप शास्त्रीय सेटिंग में हैं [4], आप जानते हैं कि या तो φ t₀ रखता है (और यह समाप्त हो गया है [5]) या ¬ (φ t₀) धारण करता है। लेकिन उत्तरार्द्ध असंभव है क्योंकि यह बी [6] के खिलाफ होगा।

Require Import Classical. 

Section Answer. 
Variable U : Type. 
Variable φ : U -> Prop. 

Lemma forall_exists: 
    ~ (forall x : U, φ x) -> exists x: U, ~(φ x). 
intros A. 
apply NNPP.    (* [1] *) 
intro B. 
apply A.     (* [2] *) 
intro t₀.     (* [3] *) 
elim classic with (φ t₀). (* [4] *) 
trivial.     (* [5] *) 
intro H. 
elim B.     (* [6] *) 
exists t₀. 
assumption. 
Qed.