theorem-proving - 精益中的有根据的递归

Question

我正在尝试将倾斜堆形式化为精益。我已经定义了简单的树类型：

inductive tree : Type
| leaf : tree
| node : tree -> nat -> tree -> tree

接下来，我想通过以下方式定义融合操作：

def fusion : arbre × arbre -> arbre
| (t1, leaf) := t1
| (leaf, t2) := t2
| (node g1 x1 d1, node g2 x2 d2) :=
    if x1 <= x2
    then (node (fusion (d1, node g2 x2 d2)) x1 g1)
    else (node (fusion (d2, node g1 x1 d1)) x2 g2)

但是，当然，Lean 不接受这个函数，因为它“未能证明递归应用是递减的、有根据的关系”。显然，它使用了树木大小的字典乘积……显然失败了。

我怎样才能告诉它使用大小的总和？

Answer 1