Welderに強い誘導の概念はありますか？

Question

溶接機での作業中に、私はその証拠に私がsitutationに直面：コンテンツ（L1）==コンテンツ（L2）及びfはべき等、連想と可換演算子次いで倍（F、Zである場合

倍（F：、L1）は、私は、フォームのxのリストL1のためにあることを示したかった私の証明の1つの段階で

）（F、Z、L2を折る:: XS = 、（x、xs）== fold（f、z、without（x、l2））

ここで、without（x ,.）は、リストからxの出現を削除します。したがって、without（x、xs）のサイズはx :: xsのサイズよりも小さいので、Welderで強力な誘導が許可されていれば、等価（コンテンツは等しい）になるはずです。

現在、システムは、without（x、xs）に対する帰納仮説がないと私に伝えます。それでは、どのようにWelderに強い誘導をしますか？

Answer 1

構造誘導の根底にある十分に発注された注文は、木のサイズの順序には対応せず、サブツリーの関係に対応します。すなわち、がys（たとえxs.size <= ys.sizeの場合でも）のサブ要素でない場合、xs < Cons(x, xs)が、xsとCons(x, ys)は比較できません。これはwithout(x,xs)の帰納仮説を仮定することができない理由は、​​というサブツリーであることが保証されていないためです。

溶接機は実際に強い誘導を可能にします。たとえば、帰納仮説はxs.tail,xs.tail.tailなどで定義されています。サイズに基づいて誘導を行う場合は、naturalInduction（これも強い）を使用する必要があります。