After finishing an obligation from an equations definition I got this warning:
Solve Obligations tactic returned error: Proof is not complete. This will become an error in the future [solve_obligation_error,tactics] Functional induction principle could not be proved automatically, it is left as an obligation.
However there are no obligations left and everything seems to work fine. Should I be worried?
It's probably the functional induction principle that it doesn't manage to derive.
If you add the
(noind) option (I'm not sure this is the name), does it work?
The options are:
If you set either or both to
no, it might work.
Nice that worked!
What is going on though?
After you finish a definition, Equations will try to derive equalities corresponding to your clauses (the
equations option) and a functional elimination principle (which you would use with tactics
apply_funelim). Sometimes, it fails at doing either of those and thus you have to deactivate it.
Ah ok thanks. I guess adding an informative error message is TODO
I mean the error does say
Functional induction principle could not be proved automatically, it is left as an obligation.
But it is not left as an obligation it seems.
Ping @Matthieu Sozeau
Last updated: May 28 2023 at 16:30 UTC