将先前证明的定理作为假设引入

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