blob: a6ce4de0f6ca8bd1f223607d987c0425fc6a786a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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 using 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.
|
