blob: b8d13fe6bcd9915c9b772b0242e3b2f32a8fe87b (
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
|
(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
Require Import Coq.subtac.Utils.
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 ; subtac_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 ; 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.
inversion l0.
Defined.
End Nth.
|