Giới thiệu Forall trong coq?

Question

Tôi đang cố gắng (theo kiểu cổ điển) chứng minh

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

trong Coq. Những gì tôi đang cố gắng làm là chứng minh điều đó một cách kỳ lạ:

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) 

Vấn đề của tôi là với các dòng (2) và (5). Tôi không thể tìm ra cách thức để chọn một phần tử tùy ý của U, chứng minh điều gì đó về số và kết thúc một forall.

Bất kỳ đề xuất nào (Tôi không cam kết sử dụng contrapositive)?

Answer 1

Để bắt chước bằng chứng không chính thức của bạn, tôi sử dụng tiên đề cổ điển ¬¬P → P (gọi là NNPP) [1]. Sau khi áp dụng, bạn cần chứng minh False với cả A: ¬ (∀ x: U, φ x) và B: ¬ (∃ x: U, φ x). A và B là vũ khí duy nhất của bạn để suy ra False. Hãy thử A [2]. Vì vậy, bạn cần chứng minh rằng ∀ x: U, φ x. Để làm được điều đó, chúng tôi lấy một tùy ý và cố gắng chứng minh rằng φ t₀ giữ [3]. Bây giờ, vì bạn đang ở trong thiết lập cổ điển [4], bạn biết rằng φ t₀ giữ (và nó kết thúc [5]) hoặc ¬ (φ t₀) giữ. Nhưng điều thứ hai là không thể vì nó mâu thuẫn với B [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.