coq - 在 Coq 中，如何将假设中的变量引入环境中？

Question

假设我做了一个 Hypothesis关于值(value)的存在。如何在环境中命名该变量？

例子:

Require Import ZArith.
Open Scope Z.
Hint Resolve Zred_factor0 Zmult_assoc_reverse Z.mul_comm Z.mul_add_distr_l
             Z.mul_1_l Z.mul_0_r Z.mul_0_l Z.abs_nonneg.

Definition divides d n := exists c, d*c = n.
Section divisor.

  Variables (d n a:Z).
  Hypothesis H: divides d n.

现在我要介绍c以及d*c = n的事实进入环境，所以我不必通过破坏 H 来开始我的证明每次，像这样:

  Lemma div4: divides (a*d) (a*n).
    destruct H as [c H'].   (*** Here I would like to already have c and H' *) 
    subst; exists c; auto.  
  Qed.

End divisor.

Answer 1

据我所知，没有办法做你想做的事。我认为由于 Prop 消除的限制，实现起来会有点复杂。

在这种特殊情况下，您可以做的一件事是在您的上下文中将 n/d 命名为 c，然后使用您的假设证明一个辅助引理，表示 n = c * d。那么你在引理的陈述中仍然会有你的假设，但不必一直破坏它。