Stream: Coq users

Topic: Stack overflow in Qed.


view this post on Zulip Simon Gregersen (Jun 22 2021 at 15:00):

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

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Jun 22 2021 at 15:31):

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

view this post on Zulip 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!!! *)

view this post on Zulip Gaëtan Gilbert (Jun 23 2021 at 15:27):

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

view this post on Zulip Simon Gregersen (Jun 24 2021 at 08:20):

@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

view this post on Zulip Robbert Krebbers (Jun 24 2021 at 08:30):

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: Feb 01 2023 at 13:03 UTC