가설로 이전에 증명 된 정리를 소개합니다.

Question

이미 coq에서 정리를 증명했으며, 나중에 다른 정리의 증명에서 가설로 소개하고자한다고 가정합니다. 이 작업을 수행하는 간결한 방법이 있습니까?

사례에 대한 증명과 같은 것을하고 싶을 때 일반적으로이 문제에 대한 필요성이 제기됩니다. 그리고 이것을 수행하는 한 가지 방법은 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).