well founded relation problem with 3 mutual recursion

Stream: general

[Sorawee Porncharoenwase]

inductive tree : Type
| node : list tree → tree

example := tree.node []

mutual def f, g, h
with f : tree → ℕ
| (tree.node children) := 1 + g children
with g : list tree → ℕ
| [] := 0
| (x :: xs) := f x + g xs
with h : ℕ → ℕ
| x := x

results in failed to prove recursive application is decreasing, well founded relation.

But that's weird, since for this particular program, it's really no different from:

inductive tree : Type
| node : list tree → tree

example := tree.node []

mutual def f, g
with f : tree → ℕ
| (tree.node children) := 1 + g children
with g : list tree → ℕ
| [] := 0
| (x :: xs) := f x + g xs

which works.

Just like https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Mutual.20recursion.2Finduction, I'm not sure how to use using_well_founded, and the workaround in that thread doesn't seem applicable for my case.

[Eric Wieser]

Just to check I read that correctly, h does not take part in the recursion at all?

[Sorawee Porncharoenwase]

This is a reduced example where h does not take part in the recursion at all, yes.

Though in my original program, h does take part in the recursion.

[Reid Barton]

Yes, this does look weird. Would you mind filing a bug report at https://github.com/leanprover-community/lean/issues with this information?

[Reid Barton]

I guess it's possible that adding h to the recursion disrupts whatever metric it's trying to use to prove that the translated version is well-founded

[Mario Carneiro]

This is expected. The rule that lean uses is that every function must call mutual functions at "smaller" arguments

[Mario Carneiro]

actually I misread the example, I thought you had something like h x := f x

[Reid Barton]

But there are no function calls to or from h

[Reid Barton]

yes, I misread the same way at first too

[Mario Carneiro]

The mwe works for me

[Reid Barton]

The top one?

[Mario Carneiro]

yes

[Reid Barton]

interesting, it fails for me

[Mario Carneiro]

lean.version = 3.23.0

[Mario Carneiro]

just updated to latest master, still works

[Reid Barton]

I'm on 3.21.0 so that could be the reason

[Mario Carneiro]

oh wait, no I'm just blind

[Mario Carneiro]

missed the squiggle on g

[Mario Carneiro]

If I replace the dec tac with assumption I can see the problem:

⊢ has_well_founded.r (psum.inr (psum.inl children)) (psum.inl (tree.node children))

The issue is that we have two constructors on each side, so they each add two and you get essentially n + 2 < n + 2

[Mario Carneiro]

This kind of sucks because it means that it is "more expensive" to call functions with large index in the list

[Reid Barton]

oh I see!

[Reid Barton]

and there isn't a problem with only two functions because the base case is inl and inr

[Mario Carneiro]

This compilation strategy has always been pretty dubious to me, but one way I could see us fixing it is to have the sizeof metric be sum.elim sizeof (sum.elim sizeof sizeof) instead of just sizeof

[Reid Barton]

I guess another way to make it more predictable would be to use a fresh inductive type with one constructor per recursive function

[Reid Barton]

but that might be awkward

[Mario Carneiro]

If we did that, we could skip the sizeof crap altogether

[Mario Carneiro]

in particular, it would allow for mutual structural recursion

[Mario Carneiro]

currently, everything has to have order type nat, which is less powerful than inductive types

[Mario Carneiro]

lean#496 implements the easy fix using sum.elim sizeof (sum.elim sizeof sizeof)