blob: e5f42defb93fc78e934e28b01c3270746d0bd452 (
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
96
97
98
99
100
101
|
Require Import Coq.subtac.Utils.
Require Import List.
Require Import Arith.
Variable A : Set.
Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
Extraction Inline proj1_sig.
Notation "'forall' { x : A | P } , Q" :=
(forall x:{x:A|P}, Q)
(at level 200, x ident, right associativity).
Require Import Omega.
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.
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.
rewrite Heql ; auto.
simpl.
rewrite (subset_simpl (append tl0 l')).
unfold tl0 ; unfold hd0.
rewrite Heql.
simpl ; auto.
Defined.
Extraction append.
Lemma append_app' : forall l : list A, (`append nil l) = l.
Proof.
simpl ; auto.
Qed.
Lemma append_app : forall l : list A, (`append l nil) = l.
Proof.
intros.
induction l ; simpl ; auto.
simpl in IHl.
rewrite IHl.
reflexivity.
Qed.
|
