From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/2083.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 test-suite/bugs/closed/2083.v (limited to 'test-suite/bugs/closed/2083.v') diff --git a/test-suite/bugs/closed/2083.v b/test-suite/bugs/closed/2083.v new file mode 100644 index 00000000..5f17f7af --- /dev/null +++ b/test-suite/bugs/closed/2083.v @@ -0,0 +1,27 @@ +Require Import Program Arith. + +Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) + (H : forall (i : { i | i < n }), i < p -> P i = true) + {measure (n - p)} : + Exc (forall (p : { i | i < n}), P p = true) := + match le_lt_dec n p with + | left _ => value _ + | right cmp => + if dec (P p) then + check_n n P (S p) _ + else + error + end. + +Require Import Omega. + +Solve Obligations with program_simpl ; auto with *; try omega. + +Next Obligation. + apply H. simpl. omega. +Defined. + +Next Obligation. + case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst. + revert H0. clear_subset_proofs. auto. + apply H. simpl. assumption. Defined. -- cgit v1.2.3