引入先前證明的定理作爲假設

Question

假設我已經在coq中證明了一些定理，後面我想將它作爲另一個定理的證明中的一個假設。有沒有一個簡潔的方法來做到這一點？

對於我來說，當我想通過案例做一些類似的證明時，通常會出現這種需求。我發現有一種方法可以做到這一點，即定理的陳述，然後立即證明它，但這看起來有點麻煩。例如，我傾向於寫的東西，如：

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).