Ali Caglayan (Nov 25 2021 at 17:59): Ali Caglayan (Nov 25 2021 at 17:59):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?
Théo Winterhalter (Nov 25 2021 at 18:05):It's probably the functional induction principle that it doesn't manage to derive.
Théo Winterhalter (Nov 25 2021 at 18:06):If you add the (noind) option (I'm not sure this is the name), does it work?
Théo Winterhalter (Nov 25 2021 at 18:07):The options are:
#[derive(equations=yes,no, eliminator=yes|no)]
If you set either or both to no, it might work.
Ali Caglayan (Nov 25 2021 at 18:21):Nice that worked!
Ali Caglayan (Nov 25 2021 at 18:21):What is going on though?
Théo Winterhalter (Nov 25 2021 at 18:49):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 funelim or apply_funelim). Sometimes, it fails at doing either of those and thus you have to deactivate it.
Ali Caglayan (Nov 25 2021 at 19:02):Ah ok thanks. I guess adding an informative error message is TODO
Théo Winterhalter (Nov 25 2021 at 19:09):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