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
87
88
89
90
91
92
93
94
95
96
97
98
99
|
(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
Require Import Coq.Program.Program.
Require Import List.
Set Implicit Arguments.
Section Accessors.
Variable A : Set.
Program Definition myhd : forall (l : list A | length l <> 0), A :=
fun l =>
match l with
| nil => !
| hd :: tl => hd
end.
Program Definition mytail (l : list A | length l <> 0) : list A :=
match l with
| nil => !
| hd :: tl => tl
end.
End Accessors.
Program Definition test_hd : nat := myhd (cons 1 nil).
(*Eval compute in test_hd*)
(*Program Definition test_tail : list A := mytail nil.*)
Section app.
Variable A : Set.
Program Fixpoint app (l : list A) (l' : list A) { struct l } :
{ r : list A | length r = length l + length l' } :=
match l with
| nil => l'
| hd :: tl => hd :: (tl ++ l')
end
where "x ++ y" := (app x y).
Next Obligation.
intros.
destruct_call app ; program_simpl.
Defined.
Program Lemma app_id_l : forall l : list A, l = nil ++ l.
Proof.
simpl ; auto.
Qed.
Program Lemma app_id_r : forall l : list A, l = l ++ nil.
Proof.
induction l ; simpl in * ; auto.
rewrite <- IHl ; auto.
Qed.
End app.
Extraction app.
Section Nth.
Variable A : Set.
Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A :=
match n, l with
| 0, hd :: _ => hd
| S n', _ :: tl => nth tl n'
| _, nil => !
end.
Next Obligation.
Proof.
simpl in *. auto with arith.
Defined.
Next Obligation.
Proof.
inversion H.
Qed.
Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A :=
match l, n with
| hd :: _, 0 => hd
| _ :: tl, S n' => nth' tl n'
| nil, _ => !
end.
Next Obligation.
Proof.
simpl in *. auto with arith.
Defined.
Next Obligation.
Proof.
intros.
inversion H.
Defined.
End Nth.
|
