Qed and Defined treat abstract proofs differently

[andres-erbsen]

Version

The Coq Proof Assistant, version 8.8.1 (July 2018)
compiled on Jul 5 2018 7:25:50 with OCaml 4.06.0

Description of the problem

Using abstract in a proof and ending it with Qed inlines the abstract-ed proofs (and spends a bunch of time doing that). Using abstract in a proof ended with Defined does not inline the subproofs but pollutes the namespace where the proof is used with the names of the abstracted subterms (and disallows async compilation of reverse-dependencies), so it is not a real alternative. Further, this strange action at a distance does not seem to be documented anywhere.

As an immediate workaround, Qed should stop inlining the abstract-ed subterms and instead rename them into totally unpredictable names starting with __do_not_use_this_. If it's easy, -mangle-names should affect them. A more principled solution would probably be somewhat similar to Local Definitions.

[JasonGross]

cc @gares (and maybe @ejgallego?)

[JasonGross]

See also #3442 (@andres-erbsen is this a duplicate of #3442?)

[JasonGross]

See also #4357

[andres-erbsen]

3442 and this issue are indeed about the same problem. I would prefer to keep this one open and close #3442 because I think the solution requested in #3442 does not go far enough.

[gares]

The reason why abstract does not play well with asynchronous proofs is, well, clear I hope. All that follows the Qed has already been processed before one discovers that the ltac scripts calls abstract, hence things are type checked in an environment that does not contain the abstracted sub proofs.

What is the real problem? I see what the problem of using Defined is. I don't see what is the problem of having these abstracted proofs being inlined (given that #4357 is solved I hope).

[andres-erbsen]

The real problem is performance, in both cases. I do not understand how #4357 can be fixed given that Qed still inlines proofs. https://github.com/andres-erbsen/coq-experiments/blob/master/experiments/bench/multiple_abstract_qed.v takes 5x longer to do Qed (inlining abstract proofs) than to just re-check the proof term without inlining the abstracted proofs, and even much longer than using Defined (https://github.com/andres-erbsen/coq-experiments/blob/master/experiments/bench/multiple_abstract_defined.v#L9). This is bad enough to necessitate using "Defined" to close opaque proofs and then creating Qed-closed wrappers for them. The situation is kind-of workable under that policy, but this policy (most importantly) requires cargo-cult boilerplate, pollutes the namespace, and completely gives up parallel processing.

Edit: I do not have a good test for this yet, but real requirement for the framework I am building is that on a 1.5GB RAM machine I should be able to abstract a 1GB proof object and then abstract another 1GB proof object and then Qed the proof without touching these abstracted proof objects again (if necessary, by swapping to the disk on OS-level).

I understand that we want abstracted proofs under Qed not to be available under outside use, and that is necessary for knowing how to process later proofs before the one with abstract. It is not clear that sticking the abstracted proofs in the environment anyway, with painfully long random names, would cause an issue in practice.

[mattam82]

Could it be that the performance hit is due to using letin’s instead of a beta-redex encoding? Le sam. 11 août 2018 à 14:42, Andres Erbsen notifications@github.com a écrit :

The real problem is performance, in both cases. I do not understand how

4357 https://github.com/coq/coq/issues/4357 can be fixed given that

Qed still inlines proofs. https://github.com/andres-erbsen/coq-experiments/blob/master/experiments/bench/multiple_abstract_qed.v takes 5x longer to do Qed (inlining abstract proofs) than to just re-check the proof term without inlining the abstracted proofs, and even much longer than using Defined ( https://github.com/andres-erbsen/coq-experiments/blob/master/experiments/bench/multiple_abstract_defined.v#L9). This is bad enough to necessitate using "Defined" to close opaque proofs and then creating Qed-closed wrappers for them. The situation is kind-of workable under that policy, but this policy (most importantly) requires cargo-cult boilerplate, pollutes the namespace, and completely gives up parallel processing.

I understand that we want abstracted proofs under Qed not to be available under outside use, and that is necessary for knowing how to process later proofs before the one with abstract. It is not clear that sticking the abstracted proofs in the environment anyway, with painfully long random names, would cause an issue in practice.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/coq/coq/issues/8234#issuecomment-412272711, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARQqsaZMDwKz_Mtk8C3WMt0ByiDhjks5uPtEdgaJpZM4V41h_ .

[andres-erbsen]

I think the inlining is done using beta-redexes. It is mostly cut off at the comment at https://github.com/andres-erbsen/coq-experiments/blob/master/experiments/bench/multiple_abstract_qed.v#L46 but you can see one layer.

[gares]

I do not understand how #4357 can be fixed given that Qed still inlines proofs

What abstract is used, in the use case mentioned in the bug, is to "cache" a long computation that one want to do only once at proof construction time.

The abstracted proof in inlined, but Coq should be able to remember that it was already checked. In this case the bodies of the bunch of let-in/beta coming from inlining are not type checked again at Qed time.

IIRC abstracted proofs generate a beta redex, while elimination principles generated on the fly are inlined as let-in. So it should not be the case that the abstracted proof terms, even if inlined, are available when type checking the rest of the proof term (they are variables bound by lambdas).

[gares]

To be sure that the "caching" kicks in in your case, you can add a print here to see if something is actually skipped: https://github.com/coq/coq/blob/master/kernel/term_typing.ml#L200

[gares]

To be sure that the "caching" kicks in in your case, you can add a print here to see if something is actually skipped: https://github.com/coq/coq/blob/master/kernel/term_typing.ml#L200

[andres-erbsen]

Yes, https://github.com/coq/coq/blob/master/kernel/term_typing.ml#L209 is reached 10 times during the test I gave.

Fixpoint deep (n : nat) : Set :=
  match n with
  | O => unit
  | S n => option (deep n)
  end.

Goal deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300.
  Time
  assert (H0: deep 300) by (clear; abstract (repeat constructor));
  assert (H1: deep 300) by (clear; abstract (repeat constructor));
  assert (H2: deep 300) by (clear; abstract (repeat constructor));
  assert (H3: deep 300) by (clear; abstract (repeat constructor));
  assert (H4: deep 300) by (clear; abstract (repeat constructor));
  assert (H5: deep 300) by (clear; abstract (repeat constructor));
  assert (H6: deep 300) by (clear; abstract (repeat constructor));
  assert (H7: deep 300) by (clear; abstract (repeat constructor));
  assert (H8: deep 300) by (clear; abstract (repeat constructor));
  assert (H9: deep 300) by (clear; abstract (repeat constructor)).
  (* Finished transaction in 2.603 secs (2.587u,0.s) (successful) *)
  exact (H0, H1, H2, H3, H4, H5, H6, H7, H8, H9).
  (* Set Printing Implicit. Show Proof. *)
  Time Check
  (let H0 := Unnamed_thm_subproof in
   let H1 := Unnamed_thm_subproof0 in
   let H2 := Unnamed_thm_subproof1 in
   let H3 := Unnamed_thm_subproof2 in
   let H4 := Unnamed_thm_subproof3 in
   let H5 := Unnamed_thm_subproof4 in
   let H6 := Unnamed_thm_subproof5 in
   let H7 := Unnamed_thm_subproof6 in
   let H8 := Unnamed_thm_subproof7 in
   let H9 := Unnamed_thm_subproof8 in
   (H0, H1, H2, H3, H4, H5, H6, H7, H8, H9))
  : deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300 * deep 300.
  (* Finished transaction in 0.141 secs (0.141u,0.s) (successful) *)
Time Qed.
(* HERE HERE HERE HERE HERE HERE HERE HERE HERE HERE *)
(* Finished transaction in 0.637 secs (0.634u,0.s) (successful) *)

[gares]

How many abstracted sub proofs do you have?

[andres-erbsen]

10. Here is an example with just 1:

Fixpoint deep (n : nat) : Set :=
  match n with
  | O => unit
  | S n => option (deep n)
  end.

Goal deep 1000.
  assert (deep 1000) by (abstract (repeat constructor)).
  assumption.
Time Qed.

fiat@ashryn ~/coq-experiments/experiments/bench (git)-[master] % /home/fiat/coq/bin/coqc abstarct.v
HEREFinished transaction in 0.623 secs (0.618u,0.003s) (successful)

[gares]

Since the cache kicks in, it means that the slowdown is not coming from the fact that inlined sub proofs get re-checked. Indeed it takes 2.6s to build them, and Qed takes 0.6.

Still checking the proof term takes 0.1, so Qed spends 0.5s doing other things we still have to identify.

Someone has to put profiling prints in the kernel to measure each step. Maybe given that you have term_typing at hand you could sprinkle Printf and Unix.gettimeofday here: https://github.com/coq/coq/blob/master/kernel/term_typing.ml#L277-L284 (I'm at the eutypes school, I've hard times working on something for more than 10 minutes, sorry)

[ppedrot]

In general, the culprit is hashconsing. Even if the cache works, you still have to hashcons a potentially huge term and term hashconsing is known to be pretty slow in Coq.

EDIT: I just had a look and it is definitely the case on your artificial examples.

[SkySkimmer]

Aside from the performance issue I think we wanted to have some sort of constant private to another constant to avoid having to do the inlining. Is there an issue open for that?

[ppedrot]

@SkySkimmer Not that I remember of. That said, while opening a bug is a good thing to point at our external users, it will not make the implementation of that feature happen any sooner, and is going to join the ranks of the ever growing set of bugs-from-the-limbo.

[andres-erbsen]

I still don't understand why making a not-actually-private constant is not an acceptable and expedient solution. Sure, somebody could technically reference it, but if they had to type "dont_use_this" and a dozen random characters to do that, and still did it, may they deal with the consequences.

[JasonGross]

I believe the issue is that the current implementation of workers does not support sending back multiple named terms which depend on each other. (Someone should correct me if I'm wrong.) So either this would have to be fixed, or the code path and behavior would be different depending on whether or not Coq is running in async mode or not

[ejgallego]

Does this bug still happen in master? For @andres-erbsen example I get identical timings.