Przedstawiono wcześniej udowodnione twierdzenie jako hipotezę

Question

Załóżmy, że już udowodniłem pewne twierdzenie w coq, a później chcę wprowadzić je jako hipotezę w dowodzie innego twierdzenia. Czy istnieje zwięzły sposób na zrobienie tego?

Potrzeba tego zazwyczaj powstaje, gdy chcę zrobić coś jak dowód przez przypadki. Odkryłem, że jednym ze sposobów, aby to zrobić, jest assert twierdzenie o twierdzeniu, a następnie natychmiast je udowodnić, ale wydaje się to nieporęczne. Na przykład staram się pisać takie rzeczy jak:

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. 

Ale czy istnieje prostszy sposób niż konieczności wpisywania całego assert [statement] by apply [theorem] rzecz?

Answer 1

Możesz użyć pose proof theorem_name as X., gdzie X to nazwa, którą chcesz wprowadzić.

---

Jeśli masz zamiar go zniszczeniu od razu, można również: destruct (decide_eq_nat x y).