Joshua Grosso (Nov 14 2020 at 06:01): 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")?
Qed. on the last obligation. 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....
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. :)
Matthieu Sozeau (Nov 16 2020 at 13:26):Indeed, it shouldn't fail
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....)
Matthieu Sozeau (Mar 01 2021 at 09:50):Yes, it's still considered a bug :)
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.)
Joshua Grosso (Mar 02 2021 at 03:04):(Issue opened: https://github.com/mattam82/Coq-Equations/issues/349)
Joshua Grosso (Mar 02 2021 at 05:28):this is embarrassing :-P That was supposed to just be the close paren, thank you (edited)!
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
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
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)?
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"
*)
(I've updated the bug report accordingly.)
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).
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)
Matthieu Sozeau (Mar 05 2021 at 18:59):If the instance is missing it certainly says that the proof still failed.
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?
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)
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.
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 :-(
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.
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?
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?)
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.
Matthieu Sozeau (Mar 05 2021 at 23:52):Yes, master follows closely Coq's master
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
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)
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)
Matthieu Sozeau (Mar 12 2021 at 10:00):Not yet, I'll try to have a look today
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
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!
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 :)
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.
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!
Matthieu Sozeau (Mar 16 2021 at 17:33):Happy birthday then!
Last updated: Oct 13 2024 at 01:02 UTC