4

我无法理解相等和本地定义之间的区别。例如，在阅读有关该set策略的文档时：

记住术语作为身份

这表现为 * 中的 set ( ident := term ) 并 使用逻辑（莱布尼茨）相等而不是局部定义

的确，

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

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

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

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

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

4

2 回答 2

2

您可以将set a := b + b in H重写H视为：

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

或者

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

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

事实上，remember 在某种意义上是 set 的一种变体，但它的含义却大不相同。在这种情况下，remember 将引入一个新的相等性证明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.
于 2016-06-25T08:46:55.477 回答
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.

而 with 的变体set没有（因为我们没有引入任何自由变量来使用）：

Goal ~ good 0.
  set (n := 0). intro contra.
  induction contra; try omega.
  Fail apply IHcontra; omega.
Abort.
于 2016-06-25T09:01:24.377 回答