Есть ли в Welder понятие сильной индукции?

При работе с Welder я столкнулся с ситуацией, когда мне нужно доказать, что:

если content(l1) == content(l2) и f является идемпотентным, ассоциативным и коммутативным оператором, то fold(f,z,l1) = fold(f,z,l2)

На одном этапе доказательства я хотел показать, что для списка l1 вида x::xs:

свернуть (f, z, без (x, xs)) == свернуть (f, z, без (x, l2))

Где with(x,.) удаляет вхождения x из списка. Поэтому ясно, что размер без (x, xs) меньше, чем размер x:: xs, и поэтому, если бы в Welder была разрешена сильная индукция, я должен был бы получить равенство (содержимое равно).

В настоящее время система просто говорит мне, что нет гипотез индукции для без (x, xs). Так как же сделать сильную индукцию на Welder?


scala leon
person Rodrigo    schedule 25.03.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Хорошо обоснованное упорядочение, лежащее в основе структурной индукции, соответствует не упорядочению размеров деревьев, а соотношению поддеревьев. А именно, xs < Cons(x, xs), но xs и Cons(x, ys) несопоставимы, если xs не является подэлементом ys (даже если xs.size <= ys.size). Вот почему вы не можете принять индуктивную гипотезу относительно without(x,xs), так как не гарантируется, что это поддерево x :: xs.

Сварщик действительно допускает сильную индукцию. Например, индуктивная гипотеза определяется на основе xs.tail, xs.tail.tail и т. д. Если вам нужна индукция, основанная на размерах, вам придется использовать naturalInduction (что также является сильным).

person Nicolas Voirol    schedule 25.03.2017