Stream: Equations devs & users

Topic: Solve Obligations tactic returned error: Proof is not com...


view this post on Zulip 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?

view this post on Zulip Théo Winterhalter (Nov 25 2021 at 18:05):

It's probably the functional induction principle that it doesn't manage to derive.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Nov 25 2021 at 18:21):

Nice that worked!

view this post on Zulip Ali Caglayan (Nov 25 2021 at 18:21):

What is going on though?

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Nov 25 2021 at 19:02):

Ah ok thanks. I guess adding an informative error message is TODO

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Nov 25 2021 at 19:09):

But it is not left as an obligation it seems.
Ping @Matthieu Sozeau


Last updated: Jan 29 2023 at 15:02 UTC