24

假设我已经在 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]呢？

4

1 回答 1

23

您可以使用pose proof theorem_name as X.,X您要介绍的名称在哪里。

如果您要立即销毁它，您还可以：destruct (decide_eq_nat x y).

于 2013-02-15T23:45:37.333 回答