blob: 07f63a2ba8378d88a55ffee15675a82e2fae603e (
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
28
29
30
31
32
33
34
35
36
37
38
39
|
Variable A : Set.
Require Import JMeq.
Require Import List.
Require Import Coq.subtac.Utils.
Program Fixpoint take (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
match n with
| 0 => nil
| S p =>
match l with
| cons hd tl => let rest := take tl p in cons hd rest
| nil => _
end
end.
Require Import Omega.
Obligations.
Solve Obligations using (subtac_simpl ; subst ; auto with arith).
Obligations.
Obligation 3.
subtac_simpl.
destruct_call take ; subtac_simpl ; subst ; auto.
Defined.
Obligation 4.
subtac_simpl.
subst l x.
simpl in l0.
absurd (S p <= 0) ; omega.
Defined.
Print take.
Extraction take.
|
