Giới thiệu định lý đã được chứng minh trước đây là giả thuyết

Question

Giả sử rằng tôi đã chứng minh một số định lý trong coq, và sau đó tôi muốn giới thiệu nó như một giả thuyết trong bằng chứng của định lý khác. Có cách nào ngắn gọn để làm điều này không?

Sự cần thiết cho điều này thường phát sinh đối với tôi khi tôi muốn làm điều gì đó giống như bằng chứng của các trường hợp. Và tôi đã phát hiện ra rằng một cách để làm điều này là để assert tuyên bố của định lý, và sau đó ngay lập tức chứng minh nó, nhưng điều này có vẻ hơi cồng kềnh. Ví dụ: tôi có xu hướng viết những thứ như:

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. 

Nhưng có cách nào dễ hơn là nhập toàn bộ điều assert [statement] by apply [theorem] không?

Answer 1

Bạn có thể sử dụng pose proof theorem_name as X., trong đó X là tên bạn muốn giới thiệu.

---

Nếu bạn đang đi để hủy nó ngay lập tức, bạn cũng có thể: destruct (decide_eq_nat x y).