blob: e3dbd127f95116afcae9c45a8be05fb604f40ab9 (
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
|
(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
Require Import List.
Require Import Coq.Program.Program.
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.
Obligations Tactic := unfold sub_list in * ;
program_simpl ; intuition.
Program Fixpoint map_rec ( l' : list U | sub_list l' l )
{ measure length l' } : { 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.
Next Obligation.
destruct_call map_rec.
simpl in *.
subst l'.
simpl ; auto with arith.
Qed.
Program Definition map : list V := map_rec l.
End Map_DependentRecursor.
Extraction map.
Extraction map_rec.
|
