Ana de Almeida Borges (Sep 27 2020 at 21:12): Ana de Almeida Borges (Sep 27 2020 at 21:12):I defined a term using Program Fixpoint that takes about 3 minutes to type-check and automatically prove one obligation. There is one obligation remaining, which I proved. However, the Qed doesn't seem to terminate (I waited for about one hour). Eventually I gave up and Admitted the obligation, but this also doesn't seem to terminate. The Admit Obligations command suffers from the same problem.
I know that solving this without access to the code is probably impossible, so I will try to come up with an example that suffers from the same issue and doesn't depend on 1k lines of code.
That said, I'd never heard of a non-terminating Admitted. Are there known situations leading to this, or specific steps that could help with debugging?
Emilio Jesús Gallego Arias (Sep 27 2020 at 21:36):Hi Ana, indeed it could be some of several bugs; it should be reported in the bug tracker. A couple of things got tweaked recently on master so you may want to try master to see if the problem has gone away.
Emilio Jesús Gallego Arias (Sep 27 2020 at 21:36):If you feel adventurous you could also get a backtrace from gdb to see where Coq has hanged
Emilio Jesús Gallego Arias (Sep 27 2020 at 21:38):Let us know if you need any help with that
Ana de Almeida Borges (Sep 27 2020 at 21:44):Ok, I will try to use master and see what happens. (I've never used gdb before, but if nothing else works I can also give it a try). In the mean time I've discovered that there is a simpler definition for which Admitted does terminate, taking a couple of minutes to do so. This leads me to think that it is possible that the original Admitted would terminate eventually, if I let it run for more than one hour. I'd still like not to have that in my development, however. :)
Emilio Jesús Gallego Arias (Sep 27 2020 at 21:53):Yeah I'm quite scared of Program for that same reason, once you get a problem things are too huge to debug
Emilio Jesús Gallego Arias (Sep 27 2020 at 21:53):not to say that to wait 2 minutes removes quite a lot of the fun with Coq
Paolo Giarrusso (Sep 27 2020 at 23:26):defining big fixpoints using Program in one go is indeed dangerous. IIRC Program does some post-processing after the last obligation is done, and maybe that is causing trouble?
Paolo Giarrusso (Sep 27 2020 at 23:26):And IIRC sometimes Program demands that certain obligations are Defined so it can “look into” them, for instance when proving well-foundedness.
Paolo Giarrusso (Sep 27 2020 at 23:28):In addition, Program comes with a quadratic blow-up when compiling pattern matches, especially when dealing with wildcards — Unset Program Cases. avoids that (and disables certain conveniences)
Paolo Giarrusso (Sep 27 2020 at 23:32):splitting matches in subfunctions is also helpful — a bad example is https://github.com/Blaisorblade/minidot/blob/silr/ecoop17/dot_wfrel.v#L211, while a better example is https://gitlab.mpi-sws.org/iris/examples/-/blob/master/theories/logrel/F_mu_ref_conc/logrel_unary.v#L26-86 (where Program isn’t even needed in the main definition)
Ana de Almeida Borges (Sep 27 2020 at 23:56):Paolo Giarrusso said:
defining big fixpoints using Program in one go is indeed dangerous. IIRC Program does some post-processing after the last obligation is done, and maybe that is causing trouble?
Yes, most likely. The messages
f_obligation_1 is declared
No more obligations remaining
appear immediately, but the computation doesn't stop after that.
Ana de Almeida Borges (Sep 27 2020 at 23:59):Using the branch master didn't seem to help. Nor did Unset Program Cases.
I have to say that this doesn't look like a big definition to me, except possibly for the fact that it receives many arguments. The body is exactly one match.
Paolo Giarrusso (Sep 28 2020 at 03:57):do you have sources that you could easily link, even if not minimized? People might notice something useful.
Paolo Giarrusso (Sep 28 2020 at 04:00):Or at least, their suggestions might related to your code rather than their personal bad experiences (as for my suggestions above) ;-)
Ana de Almeida Borges (Sep 28 2020 at 09:09):I'll have to ask for permission to share the code, but yeah, that's probably a good idea :)
By the way, I left it to compile overnight and it finished! In about two hours and a half. It sucks, but at least I can use the term in later modules for now.
Ana de Almeida Borges (Sep 28 2020 at 09:46):(The code will be public eventually, but for now if you would like to help me and take a look at it please PM me.)
Karl Palmskog (Sep 28 2020 at 09:49):the general recommended approach when secret code is involved is to distill an abstract example that captures the problem but doesn't refer to any other code.
Ana de Almeida Borges (Sep 28 2020 at 09:53):Yeah, I know. I spent some time trying to do that, but since a successful example is necessarily a piece of code that takes a long time to compile, doing so is very time-consuming. Maybe an example that takes two or three minutes is sufficiently enlightening. I will post that as soon as I have it.
Karl Palmskog (Sep 28 2020 at 09:59):and to add to the discussion, I think manual use of the refine tactic can serve as a replacement for Program Fixpoint. It is extremely hands on, but I have never had the problems with refine that I have had with Program. Example: https://github.com/palmskog/fitch/blob/master/coq/fitch_decidable.v#L754-806
Ana de Almeida Borges (Sep 28 2020 at 10:08):I would be happy with refine if I knew how to use it with a measure instead of structural recursion. Is that a thing?
Karl Palmskog (Sep 28 2020 at 10:14):refine doesn't support measure, but you can easily get the same proof goals and terminating function via the well_founded_induction or well_founded_induction_type recursors
Ana de Almeida Borges (Sep 28 2020 at 10:18):Perfect, this probably solves my problem! I didn't know about those recursors. Thank you very much!
Karl Palmskog (Sep 28 2020 at 10:20):@Ana de Almeida Borges here is a minimal example of using well_founded_induction_type and refine: https://gist.github.com/palmskog/60d6ad8840b907ceb1063204b75a802b
Karl Palmskog (Sep 28 2020 at 10:21):note that the general approach is discussed in the Coq'Art book in Chapter 15
Karl Palmskog (Sep 28 2020 at 10:30):I also agree with Xavier Leroy that refine has the drawback of putting executable code inside Proof...Defined, which will force people to look inside proof scripts for important definitions. Sophisticated documentation generation will not even display such code by default.
Ana de Almeida Borges (Sep 28 2020 at 10:33):I see. Well, in this case my term is actually an induction principle, so I (think I) only care about its type and it should only be relevant during proofs
Paolo Giarrusso (Sep 28 2020 at 10:34):Somebody can correct me, but isn’t well-founded induction one of the cases where obligations must be (somewhat) transparent?
Paolo Giarrusso (Sep 28 2020 at 10:35):*some obligations
Paolo Giarrusso (Sep 28 2020 at 10:35):I don’t remember if this applies just to the proof of well-foundedness, or also to the proofs that input1 < input2
Karl Palmskog (Sep 28 2020 at 10:38):yeah I don't remember details on transparency, so you may be right. Almost all my use cases will extract code to OCaml anyway, whence transparency is a non-issue.
Paolo Giarrusso (Sep 28 2020 at 10:38):ah, for docs, search for transparent in http://adam.chlipala.net/cpdt/html/GeneralRec.html (relevant to well-founded recursion in general) and in https://coq.inria.fr/refman/addendum/program.html (relevant to Program in particular)
Paolo Giarrusso (Sep 28 2020 at 10:39):@Karl Palmskog do you know if extraction drops the “recurse on Acc” part?
Paolo Giarrusso (Sep 28 2020 at 10:39):(Warning: this is already OT)
Karl Palmskog (Sep 28 2020 at 10:41):@Paolo Giarrusso I'm pretty sure it always does this, for example, here is what the extracted code looks like for the Gist above:
let alternate_F r alternate_rec =
match r.fls with
| Nil -> r.sls
| Cons (a, l0) -> Cons (a, (alternate_rec { fls = r.sls; sls = l0 } __))
let rec alternate x =
alternate_F x (fun y _ -> alternate y)
compare to:
Definition alternate_F : forall r : lr, (forall r' : lr, lrlt r' r -> alternate_t r') -> alternate_t r.
rewrite /alternate_t.
refine
(fun (r : lr) alternate_rec =>
match (fls r) as l return (fls r = l -> alternate_t r) with
| nil => fun (H_eq : fls r = nil) => exist _ (sls r) _
| a :: l0 => fun (H_eq : fls r = a :: l0) =>
match alternate_rec (mk_lr (sls r) l0) _ with
| exist _ l' H_ex => exist _ (a :: l') _
end
end (refl_equal (fls r))).
(* ... prove goals ... *)
Definition alternate : forall (r : lr), alternate_t r :=
@well_founded_induction_type lr lrlt lrlt_well_founded alternate_t alternate_F.
looks good
Paolo Giarrusso (Sep 28 2020 at 10:58):BTW, the actual proofs could maybe be done with abstract, for the benefit of clients (tho it won’t affect extraction)
Karl Palmskog (Sep 28 2020 at 11:00):@Paolo Giarrusso I don't even use abstract, but I guess this would reduce checking time and ensure proof terms are not viewable by default?
Paolo Giarrusso (Sep 28 2020 at 11:02):I’m sure of the latter, and maybe of checking time for clients
Paolo Giarrusso (Sep 28 2020 at 11:03):And is qed-time superlinear?
Paolo Giarrusso (Sep 28 2020 at 11:03):I’d have expected alternate_F typechecking to take negligible time
Karl Palmskog (Sep 28 2020 at 11:03):yes, my example takes negligible time
Paolo Giarrusso (Sep 28 2020 at 11:04):Separately: does well_founded_induction_type have some unfolding lemma?
Karl Palmskog (Sep 28 2020 at 11:05):hmm, I have to look, but I think there is a general fixpoint unfolding equality
Karl Palmskog (Sep 28 2020 at 11:06):there are a bunch of unfolding lemmas here below the definition of Fix_F, I'm pretty sure I have used Fix_eq: https://coq.inria.fr/library/Coq.Init.Wf.html
Matthieu Sozeau (Sep 30 2020 at 08:23):Paolo Giarrusso said:
Somebody can correct me, but isn’t well-founded induction one of the cases where obligations must be (somewhat) transparent?
Nope, they must be transparent only for regular structural recursion, where the guard checker must be able to look into them to check recursive calls are ok. That's one of the benefits of well-founded recursion: it doesn't rely on guard checking anymore so you can make more terms opaque
Matthieu Sozeau (Sep 30 2020 at 08:26):W.r.t. to the very long time taken by Program, I can't think of a reason why it happens. The processing done after all obligations have been proven is pretty trivial (basically just a substitution of obligation names for variables in the original term).
Ana de Almeida Borges (Oct 12 2020 at 14:30):In case someone is curious, I finally got around to using well_founded_induction and not only was it incredibly easy to do, it also completely solved the problem. Thank you very much for all the help!
Emilio Jesús Gallego Arias (Oct 12 2020 at 16:51):Great @Ana de Almeida Borges , please don't hesitate to add the example to the documentation if you think I'd be useful for others
Last updated: Sep 25 2023 at 12:01 UTC