scala - Welder 中有强感应的概念吗？

Question

在与 Welder 合作时，我遇到了必须证明的情况：

如果 content(l1) == content(l2) 并且 f 是幂等、关联和交换运算符，则 fold(f,z,l1) = fold(f,z,l2)

在我证明的一个阶段，我想证明对于 x::xs 形式的列表 l1：

折叠(f,z,不带(x,xs)) == 折叠(f,z,不带(x,l2))

where without(x,.) 从列表中删除 x 的出现。因此很明显 without(x,xs) 的大小小于 x::xs 的大小，因此如果 Welder 中允许强归纳，我应该得到相等（内容相等）。

目前，系统只是告诉我没有没有（x，xs）的归纳假设。那么如何对 Welder 进行强感应呢？

Answer 1

结构归纳基础的有根据的排序不对应于树大小的排序，而是对应于子树关系。即，如果不是（即使是）的子元素，xs < Cons(x, xs)则xs和Cons(x, ys)是不可比较的。这就是为什么你不能假设归纳假设，因为这不能保证是.xsysxs.size <= ys.sizewithout(x,xs)x :: xs

焊机实际上确实允许强感应。例如，归纳假设在 , 等上定义xs.tail。xs.tail.tail如果您想要基于大小的归纳，则必须使用naturalInduction（这也很强大）。