Ввести ранее доказанную теорему в качестве гипотезы

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