blob: 2aabfed797ba77e7bf6c4b52f647dcc5d736ec4a (
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
102
103
104
105
106
|
(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)))))
(defmacro finite-natp (x n)
`(and (natp ,x) (< ,x ,n)))
(defun finite-nat-listp (x n)
(if (endp x)
(null x)
(and (finite-natp (car x) n)
(finite-nat-listp (cdr x) n))))
(defun duplicatedp (x)
(cond ((endp x) nil)
((member (car x) (cdr x)) t)
(t (duplicatedp (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)))))
(defun map-count/list (x n)
(if (zp n)
nil
(cons (count/list (1- n) x)
(map-count/list (remove-equal (1- n) x) (1- n)))))
(defthm finite-nat-listp-remove-equal
(implies (and (not (zp n))
(finite-nat-listp x n))
(and (finite-nat-listp (remove-equal (1- n) x) (1- n))
(finite-nat-listp (remove-equal (1- n) x) n))))
(defthm len-map-count/list
(implies (natp n)
(equal (len (map-count/list x n)) n)))
(defthm sum-map-count/list-nil
(equal (sum (map-count/list nil n)) 0))
(defun sum-map-count/list-induction (x n)
(declare (xargs :measure (nfix n)))
(if (zp n)
x
(sum-map-count/list-induction (remove-equal (1- n) x) (1- n))))
(defthm len-remove-equal
(equal (len (remove-equal e x))
(- (len x) (count/list e x))))
(defthm sum-map-count/list
(implies (and (natp n)
(finite-nat-listp x n))
(equal (sum (map-count/list x n))
(len x)))
:hints (("Goal" :induct (sum-map-count/list-induction x n))))
(defun map-count/list* (x n)
(if (zp n)
nil
(cons (count/list (1- n) x)
(map-count/list* x (1- n)))))
(defun nat-induction (n)
(if (zp n)
1
(nat-induction (- n 1))))
(defthm duplicatedp-count/list
(implies (< 1 (count/list e x))
(duplicatedp x)))
(defthm member-remove-equal
(implies (not (equal x y))
(iff (member x (remove-equal y z))
(member x z))))
(defthm duplicatedp-remove-equal
(implies (duplicatedp (remove-equal e x))
(duplicatedp x)))
(defthm member-if-over-1-map-count/list-is-duplicated
(implies (and (natp n)
(finite-nat-listp x n)
(member-if-over-1 (map-count/list x n)))
(duplicatedp x))
:hints (("Goal" :induct (sum-map-count/list-induction x n))))
(defthm pigeonhole-for-finite-nat-list
(implies (and (natp n)
(finite-nat-listp x n)
(< n (len x)))
(duplicatedp x)))
|
