Proving recursion is well-founded

Stream: general

[Julian Sutherland]

Hey All,

I am trying to define the semantics of a programming language in Lean. To do so, I have a bunch of mutually inductive types defining the different term types of the language:
mutual inductive CBlockList, Block, SwitchBody, CExpr, CStatement
with CBlockList : FTContext → set Identifier -> set Identifier -> Type
....
with Block : FTContext → set Identifier → Type
...
with SwitchBody : FTContext → set Identifier → Type
...
with CExpr : FTContext → set Identifier → ℕ → Type
...
with CStatement : FTContext → set Identifier → set Identifier → Type
...

Note that in particular, the different term types take a function typing context and a set of identifier in scope as arguments. Terms that can introduce new variables into scope have a second such argument, defining the set of arguments after the term is evaluated.

However, when defining mutually recursive functions over this mutually recursive data type, lean complains that for some of the recursive calls, it is unable to infer well-foundedness. This occurs in particular when there are calls between functions with different numbers of arguments (because of the different number of arguments of the associated types). Lean seems to try to define the well-founded order over the sum of the dependent product of each function's arguments, but when they have different number of arguments, it, I assume, does not give any order to these elements of the set, hence the problem I have encountered.

I have tried to define a mutually recursive depth function that traverse the mutually inductive data types and returns a limit to the possible depth of recursion to be able to prove well-foundedness myself, however, this function definition runs into the same problem. It seems I'm stuck in a catch-22.

How would I go about solving such a problem?

Thanks in advance!

[Huỳnh Trần Khanh]

this question is quite interesting... but first could you post a #mwe?

[Huỳnh Trần Khanh]

the way you define the language matters a lot, you should post the whole semantics

[Huỳnh Trần Khanh]

the way you define the language matters a lot, you should post the whole semantics

[Jannis Limperg]

Mutual inductives are very broken in Lean 3. You can try to define your depth function or wf relation directly via the recursors, e.g. CBlockList.rec. I think those might be strong enough. Coq and Agda are better at this.

[Huỳnh Trần Khanh]

(deleted)

[Huỳnh Trần Khanh]

(deleted)