coq - Coq 中的逻辑(莱布尼茨)相等和局部定义有什么区别？

Question

我无法理解平等和本地定义之间的区别。例如，在阅读有关 set 的文档时战术:

remember term as ident

This behaves as set ( ident := term ) in * and using a logical (Leibniz’s) equality instead of a local definition

的确，

set (ca := c + a) in *.例如生成 ca := c + a : Z在上下文中，而

remember (c + a ) as ca.生成 Heqca : ca = c + a在上下文中。

在情况 2. 我可以使用生成的假设，如 rewrite Heqca. ，而在情况 1. 中，我不能使用 rewrite ca .

案例 1. 的目的是什么，它与案例 2. 在实际使用方面有何不同？

另外，如果两者之间的区别是根本的，为什么 remember描述为 set 的变体在文档(8.5p1)中？

Answer 1

除了@ejgallego 的回答。

是的，你不能rewrite一个(本地)定义，但您可以 unfold它:

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

至于它们在实际使用中的差异——它们完全不同。例如，参见 this answer来自@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 的变体没有(因为我们没有引入 any free variables 来使用):

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