blob: 7ab720f6b626e48a98045b002c2167a7e64bad2c (
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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
Require Import List.
Require Import Coq.subtac.Utils.
Set Implicit Arguments.
Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l.
Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'.
Proof.
intros.
inversion H.
split.
intros.
apply H0.
auto with datatypes.
auto with arith.
Qed.
Section Map_DependentRecursor.
Variable U V : Set.
Variable l : list U.
Variable f : { x : U | In x l } -> V.
Program Fixpoint map_rec ( l' : list U | sub_list l' l )
{ measure l' length } : { r : list V | length r = length l' } :=
match l' with
nil => nil
| cons x tl => let tl' := map_rec tl in
f x :: tl'
end.
Obligation 1.
intros.
destruct tl' ; simpl ; simpl in e.
subst x0 tl0.
rewrite <- Heql'.
rewrite e.
auto.
Qed.
Obligation 2.
simpl.
intros.
destruct l'.
simpl in Heql'.
destruct x0 ; simpl ; try discriminate.
inversion Heql'.
inversion s.
apply H.
auto with datatypes.
Qed.
Obligation 3 of map_rec.
simpl.
intros.
rewrite <- Heql'.
simpl ; auto with arith.
Qed.
Obligation 4.
simpl.
intros.
destruct l'.
simpl in Heql'.
destruct x0 ; simpl ; try discriminate.
inversion Heql'.
subst x tl.
apply sub_list_tl with u ; auto.
Qed.
Obligation 5.
intros.
rewrite <- Heql' ; auto.
Qed.
Program Definition map : list V := map_rec l.
Obligation 1.
split ; auto.
Qed.
End Map_DependentRecursor.
Extraction map.
Extraction map_rec.
|
