精益基础上的良好递归

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)

但是，当然，精益不接受此功能，因为它“未能证明递归应用程序正在减少，建立了良好的关系”。显然，它使用了树木大小的词典编纂产品……并且显然失败了。

如何告诉我使用大小总和？

Answer 1

以下代码对我有用。有关在lean上如何建立完善的递归的文档，请访问

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md

def fusion : tree × tree -> tree
| (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)
using_well_founded 
  { rel_tac := λ _ _, 
    `[exact ⟨_, measure_wf (λ t, tree.sizeof t.1 + tree.sizeof t.2)⟩] }

这个想法是，您必须给它一个新的关系，并证明该关系有充分的基础。这是元组⟨_, measure_wf (λ t, tree.sizeof t.1 + tree.sizeof t.2)⟩对自然数的任何函数都提供了良好的关系，其证明是measure_wf，并且_只是该关系的占位符，因为它可以从...的类型推断出来。 measure_wf (λ t, tree.sizeof t.1 + tree.sizeof t.2)。