Stream: Coq users

Topic: Equations: "Functional induction principle could not be..."


view this post on Zulip Joshua Grosso (Nov 14 2020 at 06:01):

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")?

view this post on Zulip Joshua Grosso (Nov 14 2020 at 06:04):

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....

view this post on Zulip Li-yao (Nov 14 2020 at 18:26):

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

view this post on Zulip Matthieu Sozeau (Nov 16 2020 at 13:26):

Indeed, it shouldn't fail

view this post on Zulip Joshua Grosso (Feb 27 2021 at 07:14):

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....)

view this post on Zulip Matthieu Sozeau (Mar 01 2021 at 09:50):

Yes, it's still considered a bug :)

view this post on Zulip Joshua Grosso (Mar 01 2021 at 19:42):

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.)

view this post on Zulip Joshua Grosso (Mar 02 2021 at 03:04):

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

view this post on Zulip Joshua Grosso (Mar 02 2021 at 05:28):

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

view this post on Zulip Paolo Giarrusso (Mar 02 2021 at 05:30):

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

view this post on Zulip Joshua Grosso (Mar 05 2021 at 18:19):

@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

view this post on Zulip Joshua Grosso (Mar 05 2021 at 18:20):

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

view this post on Zulip Joshua Grosso (Mar 05 2021 at 18:23):

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"
*)

view this post on Zulip Joshua Grosso (Mar 05 2021 at 18:26):

(I've updated the bug report accordingly.)

view this post on Zulip Matthieu Sozeau (Mar 05 2021 at 18:58):

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

view this post on Zulip Matthieu Sozeau (Mar 05 2021 at 18:59):

You can know what exactly was defined using the Inspect 10 command (10 is for displaying the last 10 declarations in the global environment)

view this post on Zulip Matthieu Sozeau (Mar 05 2021 at 18:59):

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

view this post on Zulip Matthieu Sozeau (Mar 05 2021 at 19:00):

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

view this post on Zulip Matthieu Sozeau (Mar 05 2021 at 19:04):

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)

view this post on Zulip Joshua Grosso (Mar 05 2021 at 19:06):

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.

view this post on Zulip Joshua Grosso (Mar 05 2021 at 19:07):

Matthieu Sozeau said:

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

It seems to be missing :-(

view this post on Zulip Joshua Grosso (Mar 05 2021 at 19:10):

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

view this post on Zulip Joshua Grosso (Mar 05 2021 at 20:59):

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?

view this post on Zulip Joshua Grosso (Mar 05 2021 at 23:15):

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

view this post on Zulip Joshua Grosso (Mar 05 2021 at 23:19):

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.

view this post on Zulip Matthieu Sozeau (Mar 05 2021 at 23:52):

Yes, master follows closely Coq's master

view this post on Zulip Matthieu Sozeau (Mar 05 2021 at 23:57):

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

view this post on Zulip Joshua Grosso (Mar 06 2021 at 00:01):

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)

view this post on Zulip Joshua Grosso (Mar 11 2021 at 22:24):

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

view this post on Zulip Matthieu Sozeau (Mar 12 2021 at 10:00):

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

view this post on Zulip Matthieu Sozeau (Mar 16 2021 at 15:45):

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

view this post on Zulip Joshua Grosso (Mar 16 2021 at 15:52):

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!

view this post on Zulip Matthieu Sozeau (Mar 16 2021 at 16:01):

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 :)

view this post on Zulip Matthieu Sozeau (Mar 16 2021 at 17:10):

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

view this post on Zulip Joshua Grosso (Mar 16 2021 at 17:15):

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

view this post on Zulip Matthieu Sozeau (Mar 16 2021 at 17:33):

Happy birthday then!


Last updated: Jan 29 2023 at 01:02 UTC