Stream: Coq users

Topic: Non-terminating Admitted


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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:38):

Let us know if you need any help with that

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Karl Palmskog (Sep 28 2020 at 10:21):

note that the general approach is discussed in the Coq'Art book in Chapter 15

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

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

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

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 10:35):

*some obligations

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

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

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

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 10:39):

@Karl Palmskog do you know if extraction drops the “recurse on Acc” part?

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 10:39):

(Warning: this is already OT)

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

view this post on Zulip Karl Palmskog (Sep 28 2020 at 10:43):

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.

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 10:43):

looks good

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

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

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 11:02):

I’m sure of the latter, and maybe of checking time for clients

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 11:03):

And is qed-time superlinear?

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 11:03):

I’d have expected alternate_F typechecking to take negligible time

view this post on Zulip Karl Palmskog (Sep 28 2020 at 11:03):

yes, my example takes negligible time

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 11:04):

Separately: does well_founded_induction_type have some unfolding lemma?

view this post on Zulip Karl Palmskog (Sep 28 2020 at 11:05):

hmm, I have to look, but I think there is a general fixpoint unfolding equality

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

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

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

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

view this post on Zulip 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: Jan 28 2023 at 06:30 UTC