diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/3164.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3164.v')
-rw-r--r-- | test-suite/bugs/closed/3164.v | 49 |
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 00000000..3c9af8d0 --- /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. |