← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/system/cantor-pairing-bijective.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/system/cantor-pairing-bijective.lisp
 
1
;; The following proof shows that the cantor pairing function, hl-nat-combine,
 
2
;; is bijective. The crux of the proof is an explicit definition of the inverse
 
3
;; of the cantor pairing function.
 
4
;; - harshrc [2014-12-27 Sat] -- adapted from proof dating May 2010.
 
5
;; [2015-1-3] Added sum-inverse bounds to fill gap in given proof (pointed by Grant Passmore).
 
6
 
 
7
(in-package "ACL2")
 
8
 
 
9
(local (include-book "arithmetic-5/top" :dir :system))
 
10
 
 
11
; The cantor pairing function uses n*(n+1)/2, which is the sum of numbers upto n.
 
12
; Rather than working with *,/ arith ops, I prefer +, 1- and recursion.
 
13
(defun sum (n)
 
14
  "find sum of first n numbers"
 
15
  (if (zp n)
 
16
      0
 
17
    (+ (nfix n) (sum (- n 1)))))
 
18
 
 
19
(defthm sum-natp
 
20
  (implies (natp n)
 
21
           (and (integerp (sum n))
 
22
                (>= (sum n) 0)))
 
23
  :rule-classes (:type-prescription :rewrite))
 
24
 
 
25
(defthm sum-bound
 
26
  (implies (natp n)
 
27
           (>= (sum n) n))
 
28
  :rule-classes (:linear :rewrite))
 
29
 
 
30
; If (sum n) = M, then (sum-inverse M M) = n
 
31
(defun sum-inverse (M x)
 
32
  "return greatest number n <= x such that (sum n) <= M"
 
33
  (if (zp x)
 
34
      0
 
35
    (if (>= M (sum x))
 
36
        x
 
37
      (sum-inverse M (1- x)))))
 
38
 
 
39
 
 
40
;(encapsulate ; 
 
41
; nil
 
42
 (local (include-book "ordinals/lexicographic-ordering-without-arithmetic" :dir :system))
 
43
 
 
44
;explicit induction hint used below
 
45
 (local
 
46
  (defun sum-inverse-ind-hint (n y i)
 
47
    (declare (xargs :measure (llist n y)
 
48
                    :well-founded-relation l<))
 
49
    (if (or (zp n) (zp y))
 
50
        i
 
51
      (if (< n (sum y))
 
52
          (sum-inverse-ind-hint n (1- y) i)
 
53
        (if (equal n (sum y))
 
54
            y
 
55
          (sum-inverse-ind-hint (1- n) y (1- i))))))
 
56
  )
 
57
 
 
58
 (local
 
59
  (defthm sum-inverse-is-inverse-of-sum-helper
 
60
    (implies (and (natp y)
 
61
                  (natp p)
 
62
                  (< (sum y) (sum (+ 1 p)))
 
63
                  (<= p y))
 
64
             (equal (equal y p) t)))
 
65
  )
 
66
 
 
67
 (local
 
68
  (defthm sum-inverse-is-inverse-of-sum
 
69
    (implies (and (natp i)
 
70
                  (natp y)
 
71
                  (natp p)
 
72
                  (<= p y)
 
73
                  (<= i p)
 
74
                  (equal n (+ i (sum p))))
 
75
             (equal (sum-inverse n y) p))
 
76
    :hints (("Goal" :induct (sum-inverse-ind-hint n y i))))
 
77
  )
 
78
 
 
79
 (defthm sum-inverse-sum-corollary
 
80
   (implies (and (natp i)
 
81
                 (natp p)
 
82
                 (<= i p))
 
83
            (equal (sum-inverse (+ i (sum p)) (+ i (sum p)))
 
84
                   p)))
 
85
 
 
86
 
 
87
 
 
88
 (defthm sum-sum-inverse-bound1
 
89
  (implies (and (natp n)
 
90
                (natp y)
 
91
                (>= y n))
 
92
           (<= (sum (sum-inverse n y)) n))
 
93
  :hints (("Goal" :induct (sum-inverse-ind-hint n y i)))
 
94
  :rule-classes (:linear :rewrite))
 
95
 
 
96
 (defthm sum-sum-inverse-bound2
 
97
  (implies (and (natp n)
 
98
                (natp y)
 
99
                (>= (sum y) n)
 
100
                )
 
101
           (>= (sum (sum-inverse n y)) (- n (sum-inverse n y))))
 
102
  :hints (("Goal" :induct (sum-inverse n y))
 
103
          ("Subgoal *1/3" :cases ((> (sum (- y 1)) n))))
 
104
  :rule-classes (:linear :rewrite))
 
105
 
 
106
 ;)
 
107
 
 
108
 
 
109
; Main Proof
 
110
 
 
111
; (cantor-pairing a b) = (+ b (/ (* (+ a b) (+ a b 1)) 2))
 
112
(defun cantor-pairing (a b)
 
113
    (+ b (sum (+ a b))))
 
114
 
 
115
; the inverse of above -- this is the crux of the proof
 
116
(defun cantor-pairing-inverse (n)
 
117
  (if (equal 0 n)
 
118
    (list 0 0)
 
119
    (let* ((j (- n (sum (sum-inverse n n))))
 
120
           (i  (- (sum-inverse n n) j)))  
 
121
      (list i j))))
 
122
 
 
123
 
 
124
 
 
125
; Cantor pairing is surjective
 
126
; To show: \forall n \exists a,b \in N s.t. (cantor-pairing a b) = n 
 
127
; = { Skolemization }
 
128
; \forall n (cantor-pairing (f1 n) (f2 n)) = n
 
129
; Since ACL2 is first-order, we manually find such f1 and f2.
 
130
(defthm cantor-pairing-onto
 
131
  (let ((a (car (cantor-pairing-inverse n)))
 
132
        (b (cadr (cantor-pairing-inverse n))))
 
133
    (implies (natp n)
 
134
             (and (natp a)
 
135
                  (natp b)
 
136
                  (equal (cantor-pairing a b) n))))
 
137
  :rule-classes nil)
 
138
 
 
139
 
 
140
(defthm cantor-pairing-inverse-is-an-inverse
 
141
  (implies (and (natp a)
 
142
                (natp b))
 
143
           (equal (cantor-pairing-inverse (cantor-pairing a b)) 
 
144
                  (list a b))))
 
145
          
 
146
; Cantor pairing is injective
 
147
(defthm cantor-pairing-one-one
 
148
  (implies (and (natp a1)
 
149
                (natp b1)
 
150
                (natp a2)
 
151
                (natp b2)
 
152
                (equal (cantor-pairing a1 b1) (cantor-pairing a2 b2)))
 
153
           (equal (list a1 b1) (list a2 b2)))
 
154
  :rule-classes nil
 
155
  :hints (("Goal" :in-theory (disable cantor-pairing cantor-pairing-inverse)
 
156
                  :use ((:instance cantor-pairing-inverse-is-an-inverse (a a1) (b b1))
 
157
                        (:instance cantor-pairing-inverse-is-an-inverse (a a2) (b b2))))))#|ACL2s-ToDo-Line|#
 
158
 
 
159
 
 
160
 
 
161
 
 
162
 
 
163
 
 
164
 
 
165
#|
 
166
; The following just shows that cantor-pairing is the same function as hl-nat-combine
 
167
(local (include-book "system/hl-addr-combine" :dir :system))
 
168
 
 
169
(local
 
170
 (defthm sum-closed-form
 
171
   (implies (natp n)
 
172
            (equal (sum n)
 
173
                   (/ (* n (+ n 1)) 2))))
 
174
;:hints (("Goal" :in-theory (disable FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-LEFT))))
 
175
 )
 
176
 
 
177
(local
 
178
 (defthm hl-nat-combine-is-same-as-cantor-pairing
 
179
   (implies (and (natp a)
 
180
                 (natp b))
 
181
            (equal (hl-nat-combine a b)
 
182
                   (cantor-pairing a b)))
 
183
   :hints (("Goal" :in-theory (e/d (hl-nat-combine) (sum)))))
 
184
 )
 
185
|#
 
186