3+ mutually recursive functions

Stream: new members

[Matija Pretnar]

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]

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

[Matija Pretnar]

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]

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]

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]

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]

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]

@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]

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

[Keeley Hoek]

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

[Keeley Hoek]

Definitely there should be no duplication like you proposed.

[Keeley Hoek]

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

[Keeley Hoek]

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]

@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]

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]

I'll give it a try, thanks again!

[Žiga Lukšič]

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]

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]

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