blob: 69fe8ab2d8e8cbfb966188fc2b57b1afdad8882d (
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
|
(defun member-if-over-1 (x)
(cond ((endp x) nil)
((< 1 (car x)) x)
(t (member-if-over-1 (cdr x)))))
(defun sum (x)
(if (endp x)
0
(+ (car x)
(sum (cdr x)))))
(defthm pigeonhole
(implies (< (len x) (sum x))
(member-if-over-1 x)))
(defun list-count (e x)
(cond ((endp x) 0)
((equal e (car x)) (1+ (list-count e (cdr x))))
(t (list-count e (cdr x)))))
(defthm member-remove
(implies (not (equal x y))
(iff (member x (remove y z))
(member x z))))
(defthm no-duplicatesp-remove
(implies (no-duplicatesp x)
(no-duplicatesp (remove e x))))
(defun map-list-count (x s)
(if (endp s)
nil
(cons (list-count (car s) x)
(map-list-count (remove (car s) x) (cdr s)))))
(defthm len-map-list-count
(equal (len (map-list-count x s))
(len s)))
(defthm len-remove
(equal (len (remove e x))
(- (len x) (list-count e x))))
(defthm not-subsetp-remove
(implies (not (subsetp (remove e x) y))
(not (subsetp x (cons e y)))))
(defthm sum-map-list-count
(implies (and (no-duplicatesp s)
(subsetp x s))
(equal (sum (map-list-count x s))
(len x)))
:hints (("Goal" :induct (map-list-count x s))))
(defthm not-no-duplicatesp-list-count
(implies (< 1 (list-count e x))
(not (no-duplicatesp x))))
(defthm not-no-duplicatesp-remove
(implies (not (no-duplicatesp (remove e x)))
(not (no-duplicatesp x))))
(defthm member-if-over-1-map-list-count-is-duplicated
(implies (and (no-duplicatesp s)
(subsetp x s)
(member-if-over-1 (map-list-count x s)))
(not (no-duplicatesp x)))
:hints (("Goal" :induct (map-list-count x s))))
(defthm pigeonhole-for-list
(implies (and (no-duplicatesp s)
(subsetp x s)
(< (len s) (len x)))
(not (no-duplicatesp x))))
|
