Test case for 3164

Closed in 69c4d0fd7b8325187e8da697a9c283594047d.

I used [Timeout 2] to distinguish between stack overflow and immediate
return.

1 files changed, 49 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3164.v b/test-suite/bugs/closed/3164.v
new file mode 100644
index 000000000..3c9af8d0f
--- /dev/null
+++ b/test-suite/bugs/closed/3164.v
@@ -0,0 +1,49 @@
+(* Before 31a69c4d0fd7b8325187e8da697a9c283594047d, [case] would stack overflow *)
+Require Import Arith.
+
+Section Acc_generator.
+  Variable A : Type.
+  Variable R : A -> A -> Prop.
+
+  (* *Lazily* add 2^n - 1 Acc_intro on top of wf.
+     Needed for fast reductions using Function and Program Fixpoint
+     and probably using Fix and Fix_F_2
+   *)
+  Fixpoint Acc_intro_generator n (wf : well_founded R)  :=
+    match n with
+        | O => wf
+        | S n => fun x => Acc_intro x (fun y _ => Acc_intro_generator n (Acc_intro_generator n wf) y)
+    end.
+
+
+End Acc_generator.
+
+Definition pred_F : (forall x : nat,
+        (forall y : nat, y < x -> (fun _ : nat => nat) y) ->
+        (fun _ : nat => nat) x).
+Proof.
+  intros x.
+  simpl.
+  case x.
+  exact (fun _ => 0).
+  intros n h.
+  apply (h n).
+  constructor.
+Defined.
+
+Definition my_pred :=  Fix lt_wf (fun _ => nat) pred_F.
+
+
+Lemma my_pred_is_pred : forall x, match my_pred x with | 0 => True | S n => False end.
+Proof.
+  intros x.
+  case x.
+Abort.
+
+Definition my_pred_bad :=  Fix (Acc_intro_generator _ _ 100 lt_wf) (fun _ => nat) pred_F.
+
+Lemma my_pred_is_pred : forall x, match my_pred_bad x with | 0 => True | S n => False end.
+Proof.
+  intros x.
+  Timeout 2 case x.
+Admitted.