精益中的有充分根据的递归
精益中的有充分根据的递归
提问于 2019-11-28 08:19:47
我正试图正规化倾斜堆在精益。我定义了简单的树类型：
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)但是，当然，精益不接受这个函数，因为它“未能证明递归应用正在减少，有充分的基础”。显然，它使用了树形(…)的大小的字典积。显然失败了。
我如何告诉它使用大小之和？
回答 1
Stack Overflow用户
回答已采纳
发布于 2019-11-28 14:11:51
下面的代码适用于我。有关于精益中有充分基础的递归工作的文档。
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)的类型中推断出来。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/59084403
复制相关文章
相似问题
腾讯云开发者
