Stack overflow in Qed. · Coq users

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!!! *)

Christian Doczkal (Jun 22 2021 at 15:25):

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?

Ali Caglayan (Jun 22 2021 at 15:31):

Simon Gregersen (Jun 22 2021 at 19:59):

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!!! *)

Gaëtan Gilbert (Jun 23 2021 at 15:27):

it's getting confused by that wf_guard thing, which here seems completely useless

Simon Gregersen (Jun 24 2021 at 08:20):

Robbert Krebbers (Jun 24 2021 at 08:30):

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.

Stream: Coq users