可以重命名 coq 术语吗？

Question

抱歉，我不确定标题是否是适当的问题。

我一直在学习逻辑基础。在引理“double_plus”中，我用这个解决方案解决了它：

Lemma double_plus : forall n, double n = n + n .
Proof.
  induction n.
  - simpl. reflexivity.
  - simpl. rewrite <- plus_n_Sm. rewrite IHn. reflexivity.
  Qed.

在归纳步骤中，我的目标是：

double (S n) = S n + S n

。

我想知道是否可以假设

(S n)

是

k

并以此做类似的事情：

(* double k = k + k *)

rewrite IH. (*k + k = k + k*)
reflexivity.

Answer 1

您可以使用

set

策略。

比如说

set (k := S n) in *.

将更改所有出现的

S n

并将其替换为

k

。请注意，这仍然会保留上下文中

k := S n

的信息。 您可以使用 clearbody k

忘记

此信息。

类似的策略包括

remember

和

generalize

。

关于您的标题，请注意

rename

也是您可以使用的一种策略，但仅用于重命名，eg.

n

为

k

（ie.）您可以更改名称，而不是条款）。