## Stream: general

### Topic: well founded relation problem with 3 mutual recursion

#### Sorawee Porncharoenwase (Nov 04 2020 at 13:15):

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 (Nov 04 2020 at 13:19):

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

#### Sorawee Porncharoenwase (Nov 04 2020 at 13:26):

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 (Nov 04 2020 at 14:49):

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 (Nov 04 2020 at 14:55):

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 (Nov 04 2020 at 15:22):

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

#### Mario Carneiro (Nov 04 2020 at 15:24):

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

#### Reid Barton (Nov 04 2020 at 15:24):

But there are no function calls to or from h

#### Reid Barton (Nov 04 2020 at 15:24):

yes, I misread the same way at first too

#### Mario Carneiro (Nov 04 2020 at 15:24):

The mwe works for me

The top one?

yes

#### Reid Barton (Nov 04 2020 at 15:33):

interesting, it fails for me

#### Mario Carneiro (Nov 04 2020 at 15:33):

lean.version = 3.23.0

#### Mario Carneiro (Nov 04 2020 at 15:34):

just updated to latest master, still works

#### Reid Barton (Nov 04 2020 at 15:35):

I'm on 3.21.0 so that could be the reason

#### Mario Carneiro (Nov 04 2020 at 15:35):

oh wait, no I'm just blind

#### Mario Carneiro (Nov 04 2020 at 15:36):

missed the squiggle on g

#### Mario Carneiro (Nov 04 2020 at 15:38):

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 (Nov 04 2020 at 15:39):

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

oh I see!

#### Reid Barton (Nov 04 2020 at 15:40):

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

#### Mario Carneiro (Nov 04 2020 at 15:41):

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 (Nov 04 2020 at 15:43):

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 (Nov 04 2020 at 15:43):

but that might be awkward

#### Mario Carneiro (Nov 04 2020 at 15:43):

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

#### Mario Carneiro (Nov 04 2020 at 15:44):

in particular, it would allow for mutual structural recursion

#### Mario Carneiro (Nov 04 2020 at 15:44):

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

#### Mario Carneiro (Nov 04 2020 at 18:50):

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

Last updated: May 14 2021 at 12:18 UTC