我明白了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 分解为真和假,而case_eq (M.find n m)
保持 H 不变并添加单独的命题M.find (elt:=nat) n m = Some v
,我可以重写它以获得与 destruct 相同的效果。
有人可以解释一下这两种策略之间的区别以及何时应该使用哪一种吗?
家族中的第一个基本战术destruct
and case_eq
叫做case
。这种策略仅修改结论。当您输入时case A
and A
有一个类型T
这是感应式的,系统取代A
在目标的结论中通过类型的所有构造函数的实例T
,如果需要的话,为这些构造函数的参数添加通用量化。这会创建与类型中的构造函数一样多的目标T
。公式A
从目标中消失,如果有任何关于A
在假设中,该信息与结论中替换它的所有新构造函数之间的联系会丢失。尽管如此,case
是一种重要的原始战术。
失去假设中的信息与实例之间的联系A
结论是实践中存在很大问题,因此开发者想出了两种解决方案:case_eq
and destruct
.
就我个人而言,在写 Coq'Art 书时,我建议我们在上面写一个简单的策略case
之间保持联系A
以及等式形式的各种构造函数实例。这就是现在所谓的战术case_eq
。它的作用与case
但在目标中添加了额外的蕴涵,其中蕴涵的前提是形式的相等性A = ...
以及哪里...
是每个构造函数的一个实例。
大约在同一时间,战术destruct
被提议。不是限制目标结论中替代的效果,destruct
替换所有实例A
出现在带有类型构造函数实例的假设中T
。从某种意义上说,这更干净,因为它避免了依赖额外的相等概念,但它仍然不完整,因为表达式A
可能是复合表达式f B
, 而如果B
出现在假设中但没有出现f B
之间的联系A
and 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
and
------------------
forall p, my_pred n = S p -> n <= 1 -> S p <= 0
额外的等式在这里非常有用。
In 这个问题我建议开发者使用case_eq (a == b)
when (a == b)
有类型bool
因为这种类型是归纳性的并且信息量不大(构造函数没有参数)。但当(a == b)
有类型{a = b}+{a <> b}
(情况就是这样的string_dec
函数)构造函数的参数是有趣属性的证明,并且构造函数参数的额外通用量化足以提供相关信息,在这种情况下a = b
在第一个进球和a <> b
在第二个进球中。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)