I have the following minimized example that gives me an `Error: Stack overflow`

when trying to perform the `Qed.`

in the lemma. Is this a bug in Coq that should be reported or can anyone point to where things are going wrong for me?

```
From stdpp Require Import pretty.
From Coq Require Import Ascii.
Definition StringOfZ (x : Z) :=
match x with
| 0%Z => "0"
| Z.pos x0 => pretty (N.pos x0)
| Z.neg x0 => "-" +:+ pretty (N.pos x0)
end.
Lemma StringOfZ_no_underscore z n :
(forall n p, get n (pretty (N.pos p)) ≠ Some "_"%char) →
get n (StringOfZ z) ≠ Some "_"%char.
Proof.
intros Hlem.
destruct z; [by destruct n| |].
- apply Hlem.
- destruct n; [done|].
apply Hlem.
Qed. (* Stack overflow!!! *)
```

That looks almost surely like a bug. Can you try to inline the part of stdpp that is used in order to make the example self-contained?

You can also try Jason's bug minimizer: https://github.com/JasonGross/coq-tools/blob/master/find-bug.py

Jason's tool sadly didn't really help but I manually extracted the parts from stdpp to make the example self-contained:

```
From Coq Require Import Ascii BinNat BinInt String.
Definition wf_guard {A} `{R : A -> A -> Prop} (n : nat) (wfR : well_founded R) : well_founded R :=
Acc_intro_generator n wfR.
Definition pretty_N_char (x : N) : ascii :=
match x with
| 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4"
| 5 => "5" | 6 => "6" | 7 => "7" | 8 => "8" | _ => "9"
end%char%N.
Program Definition decideNlt (x y : N) : {N.lt x y} + {not (N.lt x y)} :=
match N.compare x y with Lt => left _ | _ => right _ end.
Next Obligation. rewrite <-N.compare_lt_iff. auto. Qed.
Fixpoint pretty_N_go_help (x : N) (acc : Acc (N.lt)%N x) (s : string) : string :=
match decideNlt 0 x with
| left H => pretty_N_go_help (N.div x 10)%N
(Acc_inv acc (N.div_lt x 10 H eq_refl))
(String (pretty_N_char (N.modulo x 10)) s)
| right _ => s
end.
Definition pretty_N_go (x : N) : string -> string :=
pretty_N_go_help x (wf_guard 32 N.lt_wf_0 x).
Definition pretty_N :=
fun x => if N.eq_dec x 0 then "0"%string else pretty_N_go x "".
Definition StringOfZ (x : Z) :=
match x with
| 0%Z => "0"%string
| Z.pos x0 => pretty_N (N.pos x0)
| Z.neg x0 => append "-" (pretty_N (N.pos x0))
end.
Lemma StringOfZ_no_underscore z n :
(forall n p, get n (pretty_N (N.pos p)) <> Some "_"%char) ->
get n (StringOfZ z) <> Some "_"%char.
Proof.
intros Hlem.
destruct z; [destruct n; intros [=]| |].
- apply Hlem.
- destruct n; [intros [=]|].
apply Hlem.
Qed. (* Stack overflow!!! *)
```

it's getting confused by that `wf_guard`

thing, which here seems completely useless

@Robbert Krebbers pinned it down to Coq unfolding the constant `wf_guard 32`

too eagerly: https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/286

Gaëtan Gilbert said:

it's getting confused by that

`wf_guard`

thing, which here seems completely useless

It's not useless. The problem is that termination proofs (proofs of `Acc`

or `well_founded`

) are typically Opaque. So, to make computation work, you need to make sure there's enough `Acc_intro`

constructors: `wf_guard`

(which is an alias for Coq's https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Wf.html#Acc_intro_generator) is doing exactly that.

An alternative is to make all `Acc`

proofs `Defined`

, but that also means that you need to make all lemmas these proof depend on `Defined`

, which is a no-go.

Last updated: Jun 20 2024 at 13:02 UTC