I'm getting this error when using `Equations`

*: "Warning: Solve Obligations tactic returned error: Proof is not complete. This will become an error in the future [solve_obligation_error,tactics] Warning: Functional induction principle could not be proved automatically, it is left as an obligation."

Is this bug-report-worthy, or is it a legitimate issue on my end (i.e. should I proceed by manually proving the functional induction principle, despite "This will become an error in the future")?

- Specifically, the message shows up after I execute
`Qed.`

on the last obligation.

Possibly worth noting: If I use `Equations?`

instead, I get "Anomaly 'Uncaught exception Not_found'", which makes me wonder if this is a deeper issue with `Equations`

than I had hoped....

That seems worth reporting even if it's not clear on whose end the problem needs fixing. And report all anomalies. :)

Indeed, it shouldn't fail

Sorry for the delay on this thread—I just ran into this issue again (in a different context), with the latest(?) version of Equations. (The good news is that I don't get the aforementioned anomaly anymore!)

Is "failure to automatically prove the functional induction principle" still considered bug-report-worthy? /cc @Matthieu Sozeau (If so, I'll actually submit a bug report this time—sorry for being lazy last time....)

Yes, it's still considered a bug :)

Thank you—I'll try to find a minimal example and file a report.

(Relatedly, I only just realized: Is using Equations with the inspect pattern strictly more powerful than the convoy pattern? I feel like I'm getting less "cannot generalize ..." errors, but I might just be misunderstanding something.)

(Issue opened: https://github.com/mattam82/Coq-Equations/issues/349)

this is embarrassing :-P That was supposed to just be the close paren, thank you (edited)!

Nothing to be embarrassed about, but almost nobody needs to know, we can almost keep this "in the family" :-D

@Matthieu Sozeau Hmm, my issue has gotten more bizarre... after I updated Equations to the latest version, I still get the same error message—but now, there are no more obligations left to solve :-O

Is there maybe a recommended way to prove the principle manually (e.g. manually defining an instance of `FunctionalElimination`

)?

If I ignore the error and try to use `funelim`

:

```
Program Lemma reify_finite_tree__top :
forall (T : 𝒯__f) (H : (fst T) [] = Some top),
reify_finite_tree T = ftg_top.
Proof.
intros.
funelim (reify_finite_tree T).
(* Error occurs here:
Error:
Unable to satisfy the following constraints:
In environment:
T : 𝒯__f
H : proj1_sig (fst (proj1_sig T)) [] = Some top
?FunctionalElimination : "FunctionalElimination T ?fun_elim_ty ?n"
*)
```

(I've updated the bug report accordingly.)

What you might be getting is a different variant of the issue where the obligation is simply not accessible anymore (I experienced that too).

You can know what exactly was defined using the `Inspect 10`

command (10 is for displaying the last 10 declarations in the global environment)

If the instance is missing it certainly says that the proof still failed.

Also, when you say you updated, you're still using the opam package right, not any of the git branches?

I think the inspect pattern is stronger than the convoy pattern. IIRC the convoy pattern is about using only substitution to get well-typed instances, which might require complicated generalizations, whereas inspect/generalization by equalities does not need to find a generalization a priori (it does not touch the goal/return type) but uses equality reasoning a posteriori (so casts appear in the the proof terms)

Matthieu Sozeau said:

Also, when you say you updated, you're still using the opam package right, not any of the git branches?

At least to my knowledge, yup.

Matthieu Sozeau said:

If the instance is missing it certainly says that the proof still failed.

It seems to be missing :-(

Just for fun, I'll try to use the latest version of Equations from Git and see what happens.

oof, when I try to build `Coq-Equations/master`

I get `Unbound constructor: Tacred.EvalConstRef`

(no matter if I install it through `opam`

or clone and build manually). Does Equations currently support Coq 8.13.1, out of curiosity?

~~(is this worthy of a bug report too, or should I not worry about since it's a development build anyway?)~~

ah, does https://travis-ci.org/github/mattam82/Coq-Equations/jobs/687047616 imply that y'all are building against development Coq? maybe that's the reason it's not working for me :-P I'll try using dev Coq next.

Yes, master follows closely Coq's master

Hmm, I just checked and I can reproduce with the current master, so the bug was not fixed in the last batch, I'll have a look next week hopefully

Matthieu Sozeau said:

What you might be getting is a different variant of the issue where the obligation is simply not accessible anymore (I experienced that too).

Thanks! In the meantime, is there a way to make the obligation re-accessible so I can fiddle with it manually? (I tried searching GitHub issues but unfortunately couldn't find anything related to the "no obligations remaining" error)

@Matthieu Sozeau just curious if there are any updates (or if it might take more time than expected to resolve)

Not yet, I'll try to have a look today

Hmm, this is a unification problem in the proof search, when trying to apply one of the well-founded measure obligations unification fails. Should be easy to fix

Super-excited to hear that—Equations is awesome, so I'm glad I'll be able to use it more now :-) Thanks so much for looking into the issue!

The error boils down to proof search succeeding under the hypothesis:

```
fst (proj1_sig (fst (proj1_sig pr1)), snd (proj1_sig pr1)) [] =
Some arrow
```

but failing under the simplified version... interesting :)

Once the fix passes CI I'll make a new point release, there's a bunch of useful bugfixes there.

(Incidentally, today's my 21st birthday, so this is an awesome birthday present :stuck_out_tongue:) Many thanks for the help!

Happy birthday then!

Last updated: Jun 24 2024 at 14:01 UTC