Hi,

Retrying with the most recent version of Equations, I still have the same issues as in https://github.com/mattam82/Coq-Equations/issues/577 where after solving the last obligation, I get `Functional induction principle could not be proved automatically: Couldn't rewrite`

.

It seems the obligation function_name_graph_correct is where it is stuck.

The first example works if I use a regular match case instead of the `with`

clause.

I couldn't find a workaround for the second example.

I'm not sure how to debug or what alternative to try.

I don't know why, but it seems like using `Equations?`

rather than `Equation`

seems to solve the issue?

I don't know about the internals of Equations, but this probably has to do with how automation is called internally, which differs slightly between the two variants?

Indeed it works for those minimal examples but it does not for my real use-case:

I do not get the `couldn't rewrite`

anymore error but instead two obligations have warning: `unresolved existential variable`

followed by `The proof has remaining shelved goals [remaining-shelved-goals,tactics,default]`

and `Solve Obligations tactic returned error: Some unresolved existential variables remain This will become an error in the future [solve_obligation_error,tactics,default]`

which finally leads to the unproven functional induction principle.

Térence Clastres said:

Indeed it works for those minimal examples but it does not for my real use-case:

I do not get the`couldn't rewrite`

anymore error but instead two obligations have warning:`unresolved existential variable`

followed by`The proof has remaining shelved goals [remaining-shelved-goals,tactics,default]`

and`Solve Obligations tactic returned error: Some unresolved existential variables remain This will become an error in the future [solve_obligation_error,tactics,default]`

which finally leads to the unproven functional induction principle.

I got it to work by a combination of specifying the parameters of the function which contains the recursive call as well as replacing the `with clause`

with the match. However, to prove termination, using `inspect`

doesn't work on the regular match, so I lose the information I need...

Last updated: Oct 13 2024 at 01:02 UTC