Coq 中的 `destruct` 和 `case_eq` 策略有什么区别？

Question

我理解destruct，因为它将归纳定义分解为其构造函数。我最近看到了case_eq，我不明白它有什么不同？

1 subgoals
n : nat
k : nat
m : M.t nat
H : match M.find (elt:=nat) n m with
    | Some _ => true
    | None => false
    end = true
______________________________________(1/1)
cc n (M.add k k m) = true

在上述上下文中，如果我确实 destruct M.find n m 它将 H 分为真假，而 case_eq (M.find n m) 保持 H 不变并添加单独的命题 M.find (elt:=nat) n m = Some v，我可以对其进行重写以获得与 destruct 相同的效果。

p>

谁能解释一下这两种策略的区别以及什么时候应该使用哪一种？

Answer 1

destruct 和case_eq 系列中的第一个基本策略称为case。这种策略只修改了结论。当您键入case A 并且A 具有一个归纳类型T 时，系统将目标结论中的A 替换为T 类型的所有构造函数的实例，并为这些参数添加通用量化构造函数，如果需要的话。这会创建与T 类型的构造函数一样多的目标。公式A 从目标中消失了，如果假设中有任何关于A 的信息，那么该信息与在结论中替换它的所有新构造函数之间的链接就会丢失。尽管如此，case 是一种重要的原始策略。

失去假设中的信息与结论中A 的实例之间的联系在实践中是一个大问题，因此开发人员提出了两种解决方案：case_eq 和destruct。

就个人而言，在编写 Coq'Art 书时，我建议我们在 case 之上编写一个简单的策略，以相等的形式保持 A 和各种构造函数实例之间的链接。这就是现在称为case_eq 的策略。它与case 做同样的事情，但在目标中增加了一个额外的含义，其中含义的前提是A = ... 形式的相等，其中... 是每个构造函数的一个实例。

大约在同一时间，提出了destruct的策略。 destruct 不是在目标结论中限制替换的效果，而是用 T 类型的构造函数实例替换假设中出现的所有 A 实例。从某种意义上说，这更干净，因为它避免依赖额外的相等概念，但它仍然不完整，因为表达式A可能是复合表达式f B，如果B出现在假设中而不是@ 987654350@ A 和 B 之间的链接仍然会丢失。

插图

Definition my_pred (n : nat) := match n with 0 => 0 | S p => p end.

Lemma example n :  n <= 1 -> my_pred n <= 0.
Proof.
case_eq (my_pred n).

给出两个目标

------------------
n <= 1 -> my_pred n = 0 -> 0 <= 0

和

------------------
forall p, my_pred n = S p -> n <= 1 -> S p <= 0

额外的相等在这里非常有用。

在this question 中，我建议开发人员在(a == b) 具有bool 类型时使用case_eq (a == b)，因为这种类型是归纳性的并且信息量不大（构造函数没有参数）。但是当(a == b) 具有{a = b}+{a <> b} 类型时（string_dec 函数就是这种情况），构造函数具有作为有趣属性证明的参数，并且构造函数参数的额外通用量化足以提供相关信息，在这种情况下，a = b 在第一个目标中，a <> b 在第二个目标中。