~~Hi, it's my first time using coq-equations in order to prove termination of mutually recursive functions.

Inside them, I use a fold_left_2 I defined that returns empty if lists aren't the same size. I have a recursive call in the function used by it. Equations generates the following goal :

```
term_size arg < S (fold_left (fun (s : nat) (a : fsl_term) => s + term_size a) args 0)
```

This should be easy to prove as long as arg is part of args but I don't see this information in the hypothesis.

What can I do?~~

Térence Clastres has marked this topic as resolved.

Térence Clastres has marked this topic as resolved.

Is it a bug that the functional induction principle cannot be proved after solving all the obligations ?

I'd say yes, unless you get a good error message; but I'd try defining fold_left using Equations, since that might make the problem easier

To generate the functional induction principle, Equations probably needs to understand fold_left; reusing fold_left's functional induction principle, or other generated info, would be a nice way to do it, but no idea if it's actually possible.

Paolo Giarrusso said:

I'd say yes, unless you get a good error message; but I'd try defining fold_left using Equations, since that might make the problem easier

It just says "couldn't rewrite". I tried the debug mode but it's too overwhelming for me to understand anything.

I'll try to make once again a minimal example of the issue.

Last updated: Jun 13 2024 at 21:01 UTC