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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
my_list_induction[X:TYPE] : THEORY
BEGIN
less(l1,l2: list[X]) : bool = length(l1) < length(l2)
less_wf: LEMMA well_founded?(less) % :-)
list_length_induction :LEMMA % :-)
(FORALL (p:pred[list[X]]):
(FORALL (g:list[X]):
(FORALL (s:list[X]):
less(s,g) IMPLIES p(s))
IMPLIES p(g))
IMPLIES (FORALL (l:list[X]): p(l)))
END my_list_induction
my_list_props[X:TYPE] : THEORY
BEGIN
occ(x:X,l:list[X]) : RECURSIVE nat =
CASES l
OF null : 0 ,
cons(y,l) : IF x=y THEN occ(x,l)+1 ELSE occ(x,l) ENDIF
ENDCASES
MEASURE length(l)
occ_nth: LEMMA
FORALL(l:list[X]): FORALL(x:X): occ(x,l) > 0 IMPLIES
EXISTS(i:nat): i<length(l) AND nth(l,i) = x
nth_occ: LEMMA
FORALL(l:list[X]): FORALL(i:nat): i<length(l) IMPLIES occ(nth(l,i),l) > 0
perm?( l1,l2 : list[X]) : bool = FORALL(x:X): occ(x,l1) = occ(x,l2)
perm_null: LEMMA % :-)
FORALL(l:list[X]): perm?(null, l) IMPLIES l = null
perm_commutative: LEMMA % :-)
FORALL(l1,l2: list[X]):perm?(l1,l2) IMPLIES perm?(l2,l1)
append_occ: LEMMA % :-)
FORALL( l1,l2:list[X] ): FORALL(x:X): occ(x,append(l1,l2)) = occ(x,l1)+occ(x,l2)
length_append: LEMMA % :-)
FORALL( l1,l2:list[X] ):length(append(l1,l2)) = length(l1) + length(l2)
nth_append: LEMMA % :-( to be done
FORALL( l1,l2:list[X] ): FORALL(i:nat): i < length(l1)+length(l2) IMPLIES
nth(append(l1,l2),i) = IF i < length(l1) THEN nth(l1,i) ELSE nth(l2,i-length(l1)) ENDIF
END my_list_props
SPLIT : THEORY
BEGIN
IMPORTING my_list_props
split (m: nat, l : list[nat]) : RECURSIVE [list[nat], list[nat]] =
CASES l OF
null : (null, null),
cons(h,t) : LET
(l,r) = split (m, t)
IN
IF h < m
THEN (cons(h,l),r)
ELSE (l,cons(h,r))
ENDIF
ENDCASES
MEASURE (length(l))
split_length: LEMMA % :-)
FORALL( m:nat, l:list[nat] ): LET s = split(m,l) IN length(l) = length(s`1) + length(s`2)
split_occ: LEMMA % :-)
FORALL( n: nat, l:list[nat] ): LET s = split(n, l) IN FORALL(x:nat):occ(x,l) = occ(x,s`1)+occ(x,s`2)
upb( g:nat, l:list[nat] ): bool =
FORALL(i:nat): i < length(l) IMPLIES nth(l,i) < g
lwb( s:nat, l:list[nat] ): bool =
FORALL(i:nat): i < length(l) IMPLIES NOT nth(l,i) < s
split_lwb_upb: LEMMA % :-( to be done
FORALL( m:nat, l:list[nat] ): LET s = split(m,l) IN upb(m,s`1) AND lwb(m,s`2)
END SPLIT
QS : THEORY
BEGIN
IMPORTING SPLIT
qs (l : list[nat]) : RECURSIVE list[nat] =
CASES l OF
null : null,
cons(h,t) : LET
(l,r) = split (h, t)
IN
append(qs(l),cons(h,qs(r)))
ENDCASES
MEASURE (length(l))
END QS
SORTED: THEORY
BEGIN
IMPORTING my_list_props[nat]
IMPORTING SPLIT
sorted?(l:list[nat]) : bool =
FORALL (i,j: nat): i < j AND j < length(l) IMPLIES nth(l,i) <= nth(l,j)
sorted_append: LEMMA % :-( to be done
FORALL( m:nat, l1,l2:list[nat] ):
sorted?(l1) AND sorted?(l2) and upb(m,l1) AND lwb(m,l2)
IMPLIES sorted?(append(l1,l2))
END SORTED
QS_props : THEORY
BEGIN
IMPORTING QS, SORTED
IMPORTING my_list_props[nat], my_list_induction[nat]
qs_perm: LEMMA % :-( to be done
FORALL(l:list[nat]):perm?(qs(l),l)
occ_upb: LEMMA % :-)
FORALL( n: nat, l:list[nat] ): upb(n,l) IMPLIES
(FORALL(x:nat):occ(x,l) > 0 IMPLIES x < n)
occ_lwb: LEMMA % :-)
FORALL( n: nat, l:list[nat] ): lwb(n,l) IMPLIES
(FORALL(x:nat):occ(x,l) > 0 IMPLIES NOT x < n)
upb_perm: LEMMA % :-)
FORALL(l, lp: list[nat]): perm?(l,lp) IMPLIES
FORALL(n:nat): upb(n,l) IMPLIES upb(n,lp)
lwb_perm: LEMMA % :-)
FORALL(l, lp: list[nat]): perm?(l,lp) IMPLIES
FORALL(n:nat): lwb(n,l) IMPLIES lwb(n,lp)
qs_sorted :LEMMA % :-( to be done
FORALL (l:list[nat]): sorted?(qs(l))
% tl : VAR list[nat]
% test : LEMMA
% qs ((:4,3,6,2,5:)) = tl
END QS_props
|
