blob: a29cd039649b73255908b4508ad81ca444d28b3e (
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
87
88
89
90
91
92
93
94
95
|
Require Import Coq.subtac.Utils.
Require Import List.
Variable A : Set.
Program Definition myhd : forall { l : list A | length l <> 0 }, A :=
fun l =>
match l with
| nil => _
| hd :: tl => hd
end.
Proof.
destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
Defined.
Extraction myhd.
Extraction Inline proj1_sig.
Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
fun l =>
match l with
| nil => _
| hd :: tl => tl
end.
Proof.
destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
Defined.
Extraction mytail.
Variable a : A.
Program Definition test_hd : A := myhd (cons a nil).
Proof.
simpl ; auto.
Defined.
Extraction test_hd.
(*Program Definition test_tail : list A := mytail nil.*)
Program Fixpoint append (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 :: (append tl l')
end.
simpl.
subst ; auto.
simpl ; rewrite (subset_simpl (append tl0 l')).
simpl ; subst.
simpl ; auto.
Defined.
Extraction append.
Program Lemma append_app' : forall l : list A, l = append nil l.
Proof.
simpl ; auto.
Qed.
Program Lemma append_app : forall l : list A, l = append l nil.
Proof.
intros.
induction l ; simpl ; auto.
simpl in IHl.
rewrite <- IHl.
reflexivity.
Qed.
|
