Coq中逻辑（莱布尼兹）相等和局部定义的区别是什么？

Question

我不太理解“相等性”和“本地定义”的区别。例如，在阅读与set策略相关的文档时：

记住term为ident

在 * 中，这将表现为设置(ident := term)，并且使用逻辑（莱布尼兹）相等性而不是本地定义。

实际上，

1. set (ca := c + a) in *. 例如，在上下文中生成ca := c + a：Z，而 2. remember (c + a ) as ca. 会在上下文中生成Heqca : ca = c + a。

在第二种情况中，我可以使用生成的假设，如rewrite Heqca。，而在第一种情况中，我不能使用rewrite ca。那么第1种的用途是什么？在实际使用中它与第2种有何不同？

此外，如果两者之间的区别是基本的，为什么在文档（8.5p1）中将remember描述为set的变体？

- thor

Answer 1

你可以将 set a := b + b in H 理解为将 H 重写为：

(fun a => H[b+b/a]) (b+b)

或者

let a := b + b in
H[b+b/a]

也就是说，它通过一个新的变量 a 来替换所有匹配模式 b+b，然后将其实例化为模式的值。在这方面，通过“转换”，H 和重写的假设仍然保持相等。

事实上，记忆在某种意义上是 set 的一种变体，但其影响非常不同。在这种情况下，记忆会引入一个新的等式证明 eq_refl: b + b = b + b，然后将左部分抽象出来。这对于在模式匹配中具有足够的自由非常方便... 这是更原子策略的记忆：

Lemma U b c : b + b = c + c.
Proof.
assert (b + b = b + b). reflexivity.
revert H.
generalize (b+b) at 1 3.
intros n H.

- ejgallego

Answer 2

除了@ejgallego的答案之外，你不能 rewrite（改写）一个（局部）定义，但是你可以unfold（展开）它：

set (ca := c + a) in *.    
unfold ca. 

关于它们实际使用的差异 - 它们非常不同。例如，请参见@eponier的这个答案。它依赖于“remember”策略，以使归纳按我们所希望的方式工作。但是，如果我们将“remember”替换为“set”，它将失败。

Inductive good : nat -> Prop :=
  | g1 : good 1
  | g3 : forall n, good n -> good (n * 3)
  | g5 : forall n, good n -> good (n + 5).

Require Import Omega.

变量使用remember可以工作：

Goal ~ good 0.
  remember 0 as n.
  intro contra. induction contra; try omega.
  apply IHcontra; omega.
Qed.

使用set的变量不会产生结果（因为我们没有引入任何自由变量来处理）：

Goal ~ good 0.
  set (n := 0). intro contra.
  induction contra; try omega.
  Fail apply IHcontra; omega.
Abort.

- Anton Trunov