Stream: new members

Topic: 3+ mutually recursive functions

Matija Pretnar (Sep 09 2019 at 09:08):

I'm working with multiple big mutually defined inductive types (I'm trying to formalize a language with up to 7 different syntactic sorts). This works okay, but when I try to define corresponding recursive functions, Lean informs me that it has failed to prove recursive application is decreasing, well founded relation. Here is a smaller counterexample:

inductive N : Type
| Z : N
| S : N -> N

mutual def f1, f2, f3
with f1 : N -> N
| N.Z := N.Z
| (N.S n) := f2 n
with f2 : N -> N
| N.Z := N.Z
| (N.S n) := f3 n
with f3 : N -> N
| N.Z := N.Z
| (N.S n) := f1 n


From the error message, I see that it tries to do lexicographic ordering, however this obviously fails. Is there a simple workaround? Thanks in advance!

Andrew Ashworth (Sep 09 2019 at 09:14):

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md

Matija Pretnar (Sep 09 2019 at 09:23):

I guess I am in the third case, where I need to define my own well-founded relation. The document suggests

The easiest way to define a well founded relation is using a function to the natural numbers.

This indeed solves the example above, but for my bigger example, the obvious candidate is the size of the term. However, for this I need to define 3+ mutually recursive functions, again causing the error above. What am I missing? I attach the full example. syntax.lean

Scott Morrison (Sep 09 2019 at 09:37):

Generally speaking, mutual def is pretty fragile, and things often go wrong. You're usually best off working out how to roll your own mutual definition (e.g. defining first f123 : N \to N \times N \times N, then later defining f1, f2, and f3 as projections).

Matija Pretnar (Sep 09 2019 at 09:52):

Thank you for the advice, but unfortunately, it does not generalize to my case. I guess the simple example I gave was misleading. What I have are say mutually recursive types T1, T2 and T3 and I need to define functions size1 : T1 \to N, size2 : T2 \to N, size3 : T3 \to N (as a first step in getting a well-founded relation). I tried avoiding mutual def by defining a single function size : T1 \oplus T2 \oplus T3 \to N, but I get the same error.

Keeley Hoek (Sep 09 2019 at 10:13):

If it was me, I would try defining size : T1 \times T2 \times T3 \to N \times N \times N, and then convincing lean that that is well-founded.

Matija Pretnar (Sep 09 2019 at 11:06):

Is there a better way of defining this function aside from listing all the possible 8 x 10 x 2 = 160 cases? I guess one can be smart with auxiliary functions, but probably that again leads to the well-foundedness issues?

Keeley Hoek (Sep 09 2019 at 11:26):

@Matija Pretnar Yes, the declaration is slightly more ugly than three separate functions, but you do not need any more cases than you would have otherwise.

Keeley Hoek (Sep 09 2019 at 11:27):

Just use a match statement to break off how to generate the three separate outputs

Keeley Hoek (Sep 09 2019 at 11:27):

Like, a match for each of T1, T2, and T3 (or however many there actually are).

Keeley Hoek (Sep 09 2019 at 11:27):

Definitely there should be no duplication like you proposed.

Keeley Hoek (Sep 09 2019 at 11:28):

Most of the time, for me anyway, writing everything like this just works out of the box.

Keeley Hoek (Sep 09 2019 at 11:28):

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md
is where you have to go to fix further problems you then have

Matija Pretnar (Sep 09 2019 at 11:56):

@Keeley Hoek Many thanks! You had me scared there for a moment :grinning: Do you by any chance have an example lying around so I can adapt it to my case?

Keeley Hoek (Sep 09 2019 at 12:00):

Sorry, not really. Here is sort-of an example:
https://github.com/leanprover-community/mathlib/pull/1274/files#diff-5d76d023ea3a78d10ca04f9fa501e572R187
Ideally le and lt would be defined mutually, but you can see in that case that they are defined together. A using_well_founded at the end there is in fact required to make things actually work, but this seems about the easiest way forward, for example.

Matija Pretnar (Sep 09 2019 at 12:07):

I'll give it a try, thanks again!

Žiga Lukšič (Sep 09 2019 at 18:05):

I have played around with it a bit and I would guess that the problem is in the fact that the type A + B + C is actually A + (B + C) (and the same problem probably persists with products?). As such, if you have b : B and cons b : A if you put them in the sum they become sum.inr (sum.inl b) and sum.inl (cons b), both having .sizeof (which is the default ordering it tries to use as far as I can tell) of 2 despite b being a subterm of cons b.

Example:

mutual inductive A, B, C
with A : Type u
| base : A
| cons : C → A
with B : Type u
| cons : A → B
with C : Type u
| cons : B → C

with adepth : A → ℕ
| A.base := 1
| (A.cons c) := 1 + cdepth c
with bdepth : B → ℕ
| (B.cons a) := 1 + adepth a
with cdepth : C → ℕ
| (C.cons b) := 1 + bdepth b


The above code complains that it cant prove 2 < 2 in the case | (A.cons c) := 1 + cdepth c .
This can then be kinda fixed by introducing a new type t(riple)sum.

inductive tsum
| first : A → tsum
| second : B → tsum
| third : C → tsum

def depth : tsum → ℕ
| (tsum.first A.base) := 1
| (tsum.first (A.cons c)) := 1 + depth (tsum.third c)
| (tsum.second (B.cons a)) := 1 + depth (tsum.first a)
| (tsum.third (C.cons b)) := 1 + depth (tsum.second b)


and the code seems to work for now.

But could one perhaps construct a better sizeof function for a specific sumtype?
So something like

def correct_size :  A+B+C → ℕ
| (sum.inl a) := A.sizeof a
| (sum.inr (sum.inl b)) := B.sizeof b
| (sum.inr (sum.inr c)) := C.sizeof c


and then use this as the measure? I have failed to find a way to insert this into the using_well_founded even with the help of
https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md

If I made any kind of wrong assumptions or conclusions please let me know.

Mario Carneiro (Sep 10 2019 at 06:56):

correct_size is not correct, because you are depending on the sizeof instance of A which is broken (you have to use correct_size to define it, meaning that this function is mutually recursive with a typeclass instance)

Mario Carneiro (Sep 10 2019 at 06:58):

The best way to solve this issue is to rewrite the mutual inductive as a regular inductive and use plain induction

Last updated: Dec 20 2023 at 11:08 UTC