# Zulip Chat Archive

## 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 mutual def adepth, bdepth, cdepth 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: May 08 2021 at 10:12 UTC