我无法理解平等和本地定义之间的区别。例如,在阅读有关 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)中?
最佳答案
除了@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.
关于coq - Coq 中的逻辑(莱布尼茨)相等和局部定义有什么区别?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/38026220/