Coq中的destruct和case_eq策略有什么区别？ [英] What is difference between `destruct` and `case_eq` tactics in Coq?

问题描述

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

I understood destruct as it breaks an inductive definition into its constructors. I recently saw case_eq and I couldn't understand what it does differently?

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 nm ，它将H分为真和假，而 case_eq（M.find nm）保留H不变，并添加单独的命题 M.find（elt：= nat）nm = Some v ，其中我可以重写以获得与销毁相同的效果。

In the above context, if I do destruct M.find n m it breaks H into true and false whereas case_eq (M.find n m) leaves H intact and adds separate proposition M.find (elt:=nat) n m = Some v, which I can rewrite to get same effect as destruct.

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

Can someone please explain me the difference between the two tactics and when which one should be used?

推荐答案

破坏和 case_eq 称为 case 。该策略仅修改结论。当您键入情况A 和 A 具有类型 T 时这是归纳法，系统将目标结论中的 A 替换为所有 T 类型的构造函数的实例，并添加通用如果需要，可以量化这些构造函数的参数。这将创建与 T 类型的构造函数一样多的目标。公式 A 从目标中消失，如果假设中有关于 A 的任何信息，则此信息之间的链接结论中所有替换它的新构造函数都将丢失。尽管如此， c是一个重要的原始策略。

The first basic tactic in the family of destruct and case_eq is called case. This tactic modifies only the conclusion. When you type case A and A has a type T which is inductive, the system replaces A in the goal's conclusion by instances of all the constructors of type T, adding universal quantifications for the arguments of these constructors, if needed. This creates as many goals as there are constructors in type T. The formula A disappears from the goal and if there is any information about A in an hypothesis, the link between this information and all the new constructors that replace it in the conclusion gets lost. In spite of this, case is an important primitive tactic.

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

Loosing the link between information in the hypotheses and instances of A in the conclusion is a big problem in practice, so developers came up with two solutions: case_eq and destruct.

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

Personnally, when writing the Coq'Art book, I proposed that we write a simple tactic on top of case that keeps a link between A and the various constructor instances in the form of an equality. This is the tactic now called case_eq. It does the same thing as case but adds an extra implication in the goal, where the premise of the implication is an equality of the form A = ... and where ... is an instance of each constructor.

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

At about the same time, the tactic destruct was proposed. Instead of limiting the effect of replacement in the goal's conclusion, destruct replaces all instances of A appearing in the hypotheses with instances of constructors of type T. In a sense, this is cleaner because it avoids relying on the extra concept of equality, but it is still incomplete because the expression A may be a compound expression f B, and if B appears in the hypothesis but not f B the link between A and B will still be lost.

插图

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

这里的额外等式非常有用。

the extra equality is very useful here.

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

In this question I suggested that the developer use case_eq (a == b) when (a == b) has type bool because this type is inductive and not very informative (constructors have no argument). But when (a == b) has type {a = b}+{a <> b} (which is the case for the string_dec function) the constructors have arguments that are proofs of interesting properties and the extra universal quantification for the arguments of the constructors are enough to give the relevant information, in this case a = b in a first goal and a <> b in a second goal.

这篇关于Coq中的destruct和case_eq策略有什么区别？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！