假设我已经在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]
thing?
您可以使用pose proof theorem_name as X.
, where X
是您要介绍的名字。
如果您要立即销毁它,您还可以:destruct (decide_eq_nat x y).
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)