Well-founded recursion in Lean

Question

I am trying to to formalize Skew Heaps in Lean. I have defined the straightforward tree type:

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

Next, I want to define the fusion operation the following way:

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)

But, of course, Lean doesn't not accept this function, as it "failed to prove recursive application is decreasing, well founded relation". Apparently, it uses the lexicographical product of the sizes of the trees… and fails, obviously.

How can I tell it to use the sum of the sizes?

Answer 1

The following code works for me. There are docs on how well founded recursion works in lean at

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)⟩] }

The idea is that you have to give it a new relation, and a proof that the relation is well founded. This is the tuple ⟨_, measure_wf (λ t, tree.sizeof t.1 + tree.sizeof t.2)⟩ Any function to the natural numbers gives a well founded relation, the proof of this is measure_wf, and the _ is just a placeholder for the relation, since it can be inferred from the type of measure_wf (λ t, tree.sizeof t.1 + tree.sizeof t.2).