coq - 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

在上述上下文中，如果我解构 M.find n m ，它会将 H 分解为 true 和 false，而 case_eq (M.find nm) 使 H 保持不变并添加单独的命题 M.find (elt:=nat) n m = Some v，我可以重写它以获得与 destruct 相同的效果。

有人可以解释一下这两种策略之间的区别以及何时应该使用哪一种吗？

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 没有限制目标结论中替换的效果，替换 A 的所有实例出现在具有类型 T 的构造函数实例的假设中。从某种意义上说，这更干净，因为它避免了依赖额外的相等概念，但它仍然不完整，因为表达式 A可能是复合表达式 f B ，如果 B出现在假设中，但没有 f B 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我建议开发者使用case_eq (a == b)当(a == b)类型为bool因为这种类型是归纳性的并且信息量不大(构造函数没有参数)。但是当 (a == b)类型为{a = b}+{a <> b} (string_dec 函数就是这种情况)构造函数具有作为有趣属性证明的参数，并且构造函数参数的额外通用量化足以提供相关信息，在本例中 a = b第一个进球和 a <> b第二个进球。