我理解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,我可以重写以获得与破坏相同的效果.
有人可以解释一下这两种策略之间的区别以及应该使用哪种策略？
Yve*_*ves 13
在家庭中的第一个基本战术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
额外的平等在这里非常有用.
在这个问题中,我建议开发人员case_eq (a == b)在(a == b)有类型时使用,bool因为这种类型是归纳的而且信息量不大(构造函数没有参数).但是当(a == b)有类型{a = b}+{a <> b}(string_dec函数的情况)时,构造函数的参数是有趣属性的证明,并且构造函数的参数的额外通用量化足以提供相关信息,在这种情况下a = b是第一个目标,a <> b在第二个目标.