Stream: Coq users

Topic: ✔ Solving equations obligations


view this post on Zulip Térence Clastres (Dec 13 2023 at 21:30):

~~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?~~

view this post on Zulip Notification Bot (Dec 13 2023 at 21:50):

Térence Clastres has marked this topic as resolved.

view this post on Zulip Notification Bot (Dec 15 2023 at 02:07):

Térence Clastres has marked this topic as resolved.

view this post on Zulip Térence Clastres (Dec 16 2023 at 14:05):

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

view this post on Zulip Paolo Giarrusso (Dec 16 2023 at 15:03):

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

view this post on Zulip Paolo Giarrusso (Dec 16 2023 at 15:05):

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.

view this post on Zulip Térence Clastres (Dec 16 2023 at 15:09):

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