It might be of more help if you post the proof. I had such issues before and I always found ways around them. The link Jason initially posted is currently the best resource of hints on this I am aware of.

Usually what made Qed slow for me was doing a `change`

in a hypothesis - using replace instead can result in astronomic speed up factors in Qed time. If a few rules are observed, Qed should not take longer than the construction of the proof term.

time to move to #Coq users? it's p clear that this isn't a bug in Coq

yeah I second Michael's suggestion. post code and we'll debug

This topic was moved here from #Coq devs & plugin devs > Coq hangs on Qed by Karl Palmskog.

Michael Soegtrop said:

It might be of more help if you post the proof. I had such issues before and I always found ways around them. The link Jason initially posted is currently the best resource of hints on this I am aware of.

do you mean proof object or proof script?

script

These are 2 lemmas where it happens: https://github.com/rems-project/cerberus/blob/80344228c91967743539abc41c030d1c93a365e4/coq/Proofs/Revocation.v#L950 and https://github.com/rems-project/cerberus/blob/80344228c91967743539abc41c030d1c93a365e4/coq/Proofs/Revocation.v#L1020

the project builds cleanly but requires some dependencies per `READEM-cheri.md`

in top level directory. May take awhile to install :(

@Jason Gross I've followed your debugging technique to find the place and the tactic slowing down Qed. I've narrowed it down to a single `destruct`

. Not sure where to go from here...

this is the exact line: https://github.com/rems-project/cerberus/blob/80344228c91967743539abc41c030d1c93a365e4/coq/Proofs/Revocation.v#L912C29-L912C45 (`break_let`

even without `repeat`

is the problem). I can show the proof state before and after if that helps.

What's the definition of `break_let`

?

Assuming it really is a single `destruct`

causing the issue: can you `remember term as var in *`

before `destruct var`

and still have the slowness show up on `destruct`

but not ` remember`

? If so, what is the type of the variable being destructed? If I recall correctly, `destruct`

uses `hnf`

which uses `simpl`

to determine the inductive type of the object being destructed, so it may be the case that you are hitting slowness of `simpl`

. If so, I would encourage you to write something like `let T := type of var in let T' := eval hnf in T in replace T with T' in var by reflexivity`

before doing destruct, or something like that. Or otherwise try to hand code the `destruct`

as a `refine match`

and see if you can avoid / diagnose the slowness that way

```
Ltac break_let :=
match goal with
| [ H : context [ (let (_,_) := ?X in _) ] |- _ ] => destruct X eqn:?
| [ |- context [ (let (_,_) := ?X in _) ] ] => destruct X eqn:?
end.
```

removing the break_let may remove the slowness but that doesn't mean it's the root cause

AFAIK doing `destruct X`

when `X`

appears in hypothesis `H`

will do something like `revert H; destruct X; intros H`

(ie create a term `match X with bla => fun H => ... end H`

)

if the type of H was modified (IIRC your script calls eg cbn on some hypotheses) this introduces a "use" of H which means the kernel will check `H : original type |- H : changed_type`

(`simpl in H; clear H`

or otherwise not using H is the same as just `clear H`

)

you can test this hypothesis by inserting "uses" of hypotheses with `pose proof H as _`

, if Qed is slow with those and without break_let then you can find which specific hypothesis (or plural hypotheses) is the problem

I've followed @Jason Gross suggestions. `remember`

did not cause slowness. Furthermore I've modified my `break_let`

tactics as follows:

```
Ltac break_let_hyp :=
match goal with
| [ H : context [ (let (_,_) := ?X in _) ] |- _ ] =>
let var := fresh "blet" in
remember X as var in *;
let T := type of var in
idtac T;
let T' := eval hnf in T in
replace T with T' in var by reflexivity
; destruct var eqn:?
end.
```

But it is still slow. The type of `var`

is `(CheriMemoryWithoutPNVI.mem_state * (memMError + CheriMemoryWithoutPNVI.storage_instance_id * AddressValue.t))%type`

I have more luck with @Gaëtan Gilbert hint. Adding `pose proof Heqp0 as _.`

even without `destruct`

causes a slowdown. The hypothesis has the following (abridged) shape:

```
Heqp0 : (let (s', s0) := .. in
match s0 with
| inl v => (s', inl v)
| inr x => ...
end) = (m0, inl m2)
```

It is however still unclear to me how to fix that.

I've narrowed down the problem to a single `cbn`

. The following is slow:

```
Axiom admit : forall {T}, T.
Lemma foo:
forall a b c d m s,
CheriMemoryWithoutPNVI.allocate_region a b c d m = (m, s) -> False.
Proof.
intros a b c d m s H.
cbn in H.
pose proof H as _.
exact admit.
Qed.
```

If there is a way to do a "safe" `cbn`

here?

As workaround, I managed to replace this `cbn`

with a combination of `unfold`

and `simpl`

but I would love to have a more generic solution.

I should have been clearer: doing any kind of change like tactics on hypothesis - that is tactics which replace hypothesis with convertible variants - is dangerous (not just change). You can replace this with a combination of eval and replace or assert an equality and rewrite with it. rewrite and replace in H are safe in my experience.

As far as I can tell, unrestricted cbv and lazy are the only "change like" tactics, which are safe on hypothesis. Everything else (change, simpl, cbn, restricted cbv and lazy, hnf, ...) should be avoided on hypothesis (in larger proofs).

I tried something like `let T := type of var in let T' := eval cbv in T in replace T with T' in var by reflexivity`

but it did not work.

It should work. E.g. this works:

```
Example Ex1: 1+1=2 -> True.
intros H.
let T:= type of H in
let T':= eval simpl in T in
replace T with T' in H by reflexivity.
```

What did not work? Did you get an error or didn't Qed become faster?

Michael Soegtrop has marked this topic as unresolved.

in my case it works for `simpl`

but for `cbv`

it hangs right there in `eval cbv`

.

That's not surprising, cbv will diverge on tons of stuff

As I read it, the point is that if you need cbv/lazy on hypotheses you're fine, if you need sth else you need such workarounds.

well, suprisingly if I just do `cbv in H`

instead of this, it works instantly but Qed will be slow later

What's the resulting H?

either the function is (almost) a normal form, or the result will be so huge to be a benchmark for the editor or for pretty-printing

We lack enough data but I'd already consider sealing CheryMemoryWithoutPNVI.allocate_region, since reduction for it *can* (effectively) diverge

the result of `cbn`

is unfolded and normalized function just 65 lines long.

I need to unfold and normalize `allocate_region`

for further proofs

FYI, the workaround is instead of `cbn in Heqp.`

to use `unfold CheriMemoryWithPNVI.allocate_region, WithPNVISwitches.get_switches, bind, ret in Heqp; simpl in Heqp`

which gives me about the same result (minus some non-essential unfolding)

the problem with this approach is that it is not generic and each time I need to look at the definition and see what I want to manually unforld and normalize. `cbn`

usually does it for me.

@Vadim Zaliva : can it be that you are mixing up `cbv`

and `cbn`

? They are very different tactics. `cbv`

does a full reduction, while `cbn`

is a newer variant of `simpl`

, which does only very limited reduction.

As far as I understand what is going on under the hood is this:

- if you do change like tactics in a hypothesis, this does not leave a cast or other information for the kernel, which would help the kernel to reconstruct the reduction result - this is different when such tactics are applied on the goal, there they leave a cast (or something).
- if you do partial reduction by simpl, cbn, change, cbv or lazy with restrictions in a hypothesis this might not be trivial to reproduce by the kernel. If the terms before and after are substantially different, it is not trivial to decide which side to unfold - one can't see easily which side to unfold first to come to the same term. What happens then is that the kernel unfolds both sides much more than the original tactic, which makes Qed slow.
- if you do full reduction (cbv or lazy without arguments) and this does not explode, it is trivial for the kernel to reproduce this since only one side of the unification problem can be reduced - the other side is already fully reduced
- the workaround via rewrite or replace leave a cast similar to a change in the goal, which helps the kernel to unify the terms

I just double-checked and `let T := type of Heqp in let T' := eval cbn in T in replace T with T' in Heqp by reflexivity`

hangs but `cbn in Heqp`

works.

And if you replace `reflexivity`

by `cbn; reflexivity`

?

the conjecture is that reflexivity calls unification, and there's no reason why unifying cbn's input with its output should be fast. Especially if cbn's output is 65 lines.

the following passed: `let T := type of Heqp in let T' := eval cbn in T in replace T with T' in Heqp by (cbn;reflexivity).`

need to check how it will affect Qed.

Qed is fast!

I guess I can define small tactics like this:

```
Ltac cbn_hyp H :=
let T := type of H in let T' := eval cbn in T in replace T with T' in H by (cbn;reflexivity).
```

and use it instead of `cbn in H`

everywhere? If that works, maybe worth suggesting in FAQ?

thanks!

I must also say that I don't quite understand the reason why reduction tactics applied in hypothesis don't leave a cast as they do when applied to the goal. @Gaëtan Gilbert : do you know why this is as it is?

you can't just do `refine (_ : oldt)`

when it's the hypothesis

you could try `refine (let H := H : newt in _)`

but then the conversion is in the wrong direction (rtl vs ltr)

to keep the conversion in the right direction I think you would have to do something like `refine ((fun H : newt => _) H)`

(not sure that even works)

tldr leaving a cast in the hypothesis isn't as trivial as leaving a cast in the goal

@Gaëtan Gilbert : my question was more: why do Coq users don't have to bother when using cbn on the goal but do have to bother when using cbn in a hypothesis? Is there some deeper reason for this?

In case it has to be like this, it would indeed help if someone with deeper insight into the kernel reduction machinery would suggest an efficient work around. One issue with the workaround suggested above is that cbn is called twice on the original term and once on the already simplified term, which might not be that fast.

Sorry, I just understood on third read of your post that you explained what the problem is - I thought you are discussing more efficient workarounds.

Obviously the 3x cbv solution discussed by Paolo and Vadim does solve the problem. The question is: can one come up with a solution which calls cbn only once. And if so, why can't this be the default when doing cbn in a hypothesis.

The main issue with this is that it likely works > 99.99% to use cbn in a hypothesis and usually fails only in large deep automation cases, where it is a nightmare to debug this - especially because the problem happens at Qed time. I think I spent several weeks debugging such cases in Princeton VST - down to running coqtop in the OCaml debugger and printing terms in the kernel reduction engine and going through GBs of logs. IMHO everybody using Coq in the large stumbles over this one day, so that this a largish road blocker for using Coq in the large.

If you use Coq in the large you must seal definitions, indeed.

and indeed, the performance problems only show up too late when rewriting code is painful, *and* figuring out what to seal is hard (don't take my word, take Jason's or look at math-comp https://stackoverflow.com/a/46138499/53974 )

I agree we'd want a smarter reduction on hyps, but that won't fix divergence on simpl/apply/... which also arise in such cases. At least for apply for this is only common for failing invocations

@Paolo Giarrusso : I tend to use a different approach, reduction with tailored, usually computed delta reduction symbol lists. It is not that feasible to introduce sealing in e.g. VST after the facts, and with this method I got very good and reliable speed ups. I could do dynamic sealing - actually Andrew does this to a certain extend - but this is too slow for my purposes. But this does not help for reductions in hypothesis - I would really appreciate a solution for this - or at least a Coq kernel expert approved work around.

@Gaëtan Gilbert @Michael Soegtrop I believe there's a recipe in the wiki / FAQ for reversing the direction of conversion.

@Jason Gross : do you have a link?

is there a bottom line for regular Coq users on how to keep their Qed time short? Are heuristics like "don't run `simpl`

in a hypothesis if you can avoid it" meaningful?

I personally never had any Qed time issues (that Qed was substantially slower than creating the proof script) other than doing simplification, reduction or change tactics on a hypothesis. But Jason suggested that there are other cases around simpl on the goal. I might have escaped these because I hardly every use simpl in automation. I am not sure if for cbv and lazy with explicit delta lists the casts are sufficiently expressive or if I have just been lucky so far.

@Michael Soegtrop

Link: the code block right above https://github.com/coq/coq/wiki/Troubleshooting#an-explosion-of-universes and the paragraph above that

As far as explicit delta links: you've mostly been lucky, but not unreasonably so. You should expect to hit a Qed issue if you have two separate calls to CBV/lazy with different lists such that if you replaced either list with the other the call to CBV/lazy would take a very long time. In general any call to CBV/lazy can be made fast by issuing a `Strategy`

command that tells the kernel to unfold constants in the same order. However, each `Qed`

processes the entire proof term with a single set of constant strategy levels, so if you need different subterms to be checked with different strategy level assignments, you'll be sad. There might be some relevant examples in the test-suite for `with_strategy`

@Karl Palmskog indeed the bottom line is roughly "don't use `simpl`

, don't use reduction tactics in hypotheses unless you revert and reintroduce them after, don't use `change ... with ...`

only `change`

"

Also, don't use `change`

on a goal with existential variables.

perhaps coq should issue warnings (which could be disabled by user) in such known problematic cases?

Even better would be to by default use one of the discussed work arounds by default and provide a separate variant of the tactic which works as today.

Last updated: Jun 13 2024 at 19:02 UTC