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