Zulip Chat Archive

Stream: general

Topic: well founded relation problem with 3 mutual recursion


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:24):

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

view this post on Zulip Reid Barton (Nov 04 2020 at 15:24):

But there are no function calls to or from h

view this post on Zulip Reid Barton (Nov 04 2020 at 15:24):

yes, I misread the same way at first too

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:24):

The mwe works for me

view this post on Zulip Reid Barton (Nov 04 2020 at 15:33):

The top one?

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:33):

yes

view this post on Zulip Reid Barton (Nov 04 2020 at 15:33):

interesting, it fails for me

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:33):

lean.version = 3.23.0

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:34):

just updated to latest master, still works

view this post on Zulip Reid Barton (Nov 04 2020 at 15:35):

I'm on 3.21.0 so that could be the reason

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:35):

oh wait, no I'm just blind

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:36):

missed the squiggle on g

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 04 2020 at 15:40):

oh I see!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 04 2020 at 15:43):

but that might be awkward

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:43):

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

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:44):

in particular, it would allow for mutual structural recursion

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:44):

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

view this post on Zulip 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