As reported by @simongregersen at https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Stack.20overflow.20in.20Qed.2E, lemmas involving
Pretty N could lead to stack overflow. I minimized his problem as follows:
Lemma test_no_stack_overflow p n : get n (pretty (N.pos p)) ≠ Some "_"%char → get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char. Proof. intros Hlem. apply Hlem. (* stack overflow *) Qed.
The problem is that Coq's conversion unfolds too much, and triggers the
wf_guard 32 in:
Definition pretty_N_go (x : N) : string → string := pretty_N_go_help x (wf_guard 32 N.lt_wf_0 x).
wf_guard is needed to make sure that computation of
pretty n for concrete numbers
n works (see tests in
tests/pretty.v). However, due to concrete number 32, which adds
2 ^ n
Acc_intro constructors to the opaque accessibility proof
N.lt_wf_0 for the well-founded recursion, Coq's conversion might unfold
wf_guard 32 too eagerly.
I hence changed the
S (N.size_nat x), which causes the tests in
tests/pretty.v to still work, and the stack overflow to disappear. The key idea is that
S (N.size_nat x) is not a concrete number if
x is an open term, thus preventing
wf_guard from unfolding.