Önceden kanıtlanmış teoremi hipotez olarak tanıtın

Question

Zaten coq'da bazı teoremleri kanıtladığımı varsayalım ve sonra bunu bir başka teoremin kanıtında bir hipotez olarak tanıtmak istiyorum. Bunu yapmanın özlü bir yolu var mı?

Bu durumun gereği, vakalara ispat gibi bir şey yapmak istediğimde genelde benim için ortaya çıkar. Ve bunu yapmanın bir yolunun teorem ifadesinin assert olduğunu keşfettim ve hemen kanıtladım, ama bu biraz hantal gibi görünüyor. Mesela ben gibi şeyler yazma eğilimi:

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. 

Ama bütün assert [statement] by apply [theorem] şeyi yazmak zorunda daha kolay bir yolu var mı?

Answer 1

pose proof theorem_name as X.'u, X tanıtmak istediğiniz addır.

---

şifrenizi hemen imha etmek gidiyoruz, şunları da yapabilirsiniz: destruct (decide_eq_nat x y).