介绍先前证明的定理为假设 [英] Introduce previously proved theorem as hypothesis

问题描述

假设我已经在coq中证明了一个定理，后来我想将其作为假设在另一个定理的证明中进行介绍。

Suppose that I have already proved some theorem in coq, and later I want to introduce it as a hypothesis in the proof of another theorem. Is there a succinct way to do this?

当我想做类似案例的证明时，通常需要这样做。而且我发现，做到这一点的一种方法是 assert 定理的陈述，然后立即证明它，但这似乎很麻烦。例如，我倾向于写这样的东西：

The need for this typically arises for me when I want to do something like a proof by cases. And I've discovered that one way to do this is to assert the statement of the theorem, and then immediately prove it, but this seems kind of cumbersome. For example I tend to write things like:

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 [语句更简单的方法吗？ ]通过应用[定理] 来完成？

But is there an easier way than having to type the whole assert [statement] by apply [theorem] thing?

推荐答案

您可以使用 pose证明定理名称为X。，其中 X 是要引入的名称。

You can use pose proof theorem_name as X., where X is the name you want to introduce.

如果要立即销毁它，也可以：销毁（decide_eq_nat xy）。

If you're going to destruct it right away, you can also: destruct (decide_eq_nat x y).

这篇关于介绍先前证明的定理为假设的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！