1(in-package "ACL2") 2 3 4#| 5 6 records.lisp 7 ~~~~~~~~~~~~ 8 9We define properties of a generic record accessor function and updater 10function. The basic functions are (g a r) and (s a v r) where a is an 11address/key, v is a value, r is a record, and (g a r) returns the 12value set to address a in record r, and (s a v r) returns a new record 13with address a set to value v in record r. 14 15We normalize the record structures (which allows the 'equal-ity based 16rewrite rules) as alists where the keys (cars) are ordered using 17Pete's total-order added to ACL2. We define a set of -aux functions 18which assume well-formed records -- defined by rcdp -- and then prove 19the desired properties using hypothesis assuming well-formed objects. 20 21We then remove these well-formed object hypothesis by defining a invertible 22mapping (acl2->rcd) from any ACL2 object to a well-formed records. We then 23prove the desired properties using the proper translations of the -aux 24functions to the acl2 objects, and subsequently remove the well-founded 25hypothesis. 26 27|# 28 29(include-book "apply-total-order") 30 31;; BEGIN records definitions. 32 33(defun rcdp (x) 34 (or (null x) 35 (and (consp x) 36 (consp (car x)) 37 (rcdp (cdr x)) 38 (cdar x) 39 (or (null (cdr x)) 40 (<< (caar x) (caadr x)))))) 41 42(defun ifrp (x) ;; ill-formed rcdp 43 (or (not (rcdp x)) 44 (and (consp x) 45 (null (cdr x)) 46 (consp (car x)) 47 (null (caar x)) 48 (ifrp (cdar x))))) 49 50(defun acl2->rcd (x) 51 (if (ifrp x) (list (cons nil x)) x)) 52 53(defun rcd->acl2 (x) 54 (if (ifrp x) (cdar x) x)) 55 56(defun g-aux (a x) 57 (cond ((or (endp x) 58 (<< a (caar x))) 59 nil) 60 ((equal a (caar x)) 61 (cdar x)) 62 (t 63 (g-aux a (cdr x))))) 64 65(defun g (a x) 66 (g-aux a (acl2->rcd x))) 67 68(defun s-aux (a v r) 69 (cond ((or (endp r) 70 (<< a (caar r))) 71 (if v (cons (cons a v) r) r)) 72 ((equal a (caar r)) 73 (if v (cons (cons a v) (cdr r)) (cdr r))) 74 (t 75 (cons (car r) (s-aux a v (cdr r)))))) 76 77(defun s (a v x) 78 (rcd->acl2 (s-aux a v (acl2->rcd x)))) 79 80(defun keys-aux (x) 81 (cond ((endp x) 82 ()) 83 (t (cons (caar x) 84 (keys-aux (cdr x)))))) 85 86(defun keys (x) 87 (keys-aux (acl2->rcd x))) 88 89 90 91;;;; basic property of records ;;;; 92 93(local 94(defthm rcdp-implies-true-listp 95 (implies (rcdp x) 96 (true-listp x)) 97 :rule-classes (:forward-chaining 98 :rewrite))) 99 100 101;;;; initial properties of s-aux and g-aux ;;;; 102 103(local 104(defthm s-aux-is-bounded 105 (implies (and (rcdp r) 106 (s-aux a v r) 107 (<< e a) 108 (<< e (caar r))) 109 (<< e (caar (s-aux a v r)))))) 110 111(local 112(defthm s-aux-preserves-rcdp 113 (implies (rcdp r) 114 (rcdp (s-aux a v r))))) 115 116(local 117(defthm g-aux-same-s-aux 118 (implies (rcdp r) 119 (equal (g-aux a (s-aux a v r)) 120 v)))) 121 122(local 123(defthm g-aux-diff-s-aux 124 (implies (and (rcdp r) 125 (not (equal a b))) 126 (equal (g-aux a (s-aux b v r)) 127 (g-aux a r))))) 128 129(local 130(defthm s-aux-same-g-aux 131 (implies (rcdp r) 132 (equal (s-aux a (g-aux a r) r) 133 r)))) 134 135(local 136(defthm s-aux-same-s-aux 137 (implies (rcdp r) 138 (equal (s-aux a y (s-aux a x r)) 139 (s-aux a y r))))) 140 141(local 142(defthm s-aux-diff-s-aux 143 (implies (and (rcdp r) 144 (not (equal a b))) 145 (equal (s-aux b y (s-aux a x r)) 146 (s-aux a x (s-aux b y r)))) 147 :rule-classes ((:rewrite :loop-stopper ((b a s)))))) 148 149(local 150(defthm s-aux-non-nil-cannot-be-nil 151 (implies (and v (rcdp r)) 152 (s-aux a v r)))) 153 154(local 155(defthm g-aux-is-nil-for-<< 156 (implies (and (rcdp r) 157 (<< a (caar r))) 158 (equal (g-aux a r) nil)))) 159 160(local 161(defthm g-keys-aux-relationship 162 (implies (rcdp r) 163 (iff (memberp a (keys-aux r)) 164 (g-aux a r))))) 165 166(local 167(defthm s-keys-aux-reduction 168 (implies (rcdp r) 169 (equal (keys-aux (s-aux a v r)) 170 (if v 171 (insert a (keys-aux r)) 172 (drop a (keys-aux r))))))) 173 174(local 175(defthm keys-aux-are-ordered 176 (implies (rcdp r) 177 (orderedp (keys-aux r))))) 178 179 180;;;; properties of acl2->rcd and rcd->acl2 ;;;; 181 182(local 183(defthm acl2->rcd-rcd->acl2-of-rcdp 184 (implies (rcdp x) 185 (equal (acl2->rcd (rcd->acl2 x)) 186 x)))) 187 188(local 189(defthm acl2->rcd-returns-rcdp 190 (rcdp (acl2->rcd x)))) 191 192(local 193(defthm acl2->rcd-preserves-equality 194 (iff (equal (acl2->rcd x) (acl2->rcd y)) 195 (equal x y)))) 196 197(local 198(defthm rcd->acl2-acl2->rcd-inverse 199 (equal (rcd->acl2 (acl2->rcd x)) x))) 200 201(local 202(defthm rcd->acl2-of-record-non-nil 203 (implies (and r (rcdp r)) 204 (rcd->acl2 r)))) 205 206(in-theory (disable acl2->rcd rcd->acl2)) 207 208 209;;;; final properties of record g(et) and s(et) ;;;; 210 211(defthm g-same-s 212 (equal (g a (s a v r)) 213 v)) 214 215(defthm g-diff-s 216 (implies (not (equal a b)) 217 (equal (g a (s b v r)) 218 (g a r)))) 219 220;;;; NOTE: I often use the following instead of the above rules 221;;;; to force ACL2 to do a case-split. In some cases, I will 222;;;; disable this rule ACL2 is sluggish or if the number of cases 223;;;; is unreasonable 224 225(defthm g-of-s-redux 226 (equal (g a (s b v r)) 227 (if (equal a b) v (g a r)))) 228 229(in-theory (disable g-of-s-redux)) 230 231(defthm s-same-g 232 (equal (s a (g a r) r) 233 r)) 234 235(defthm s-same-s 236 (equal (s a y (s a x r)) 237 (s a y r))) 238 239(defthm s-diff-s 240 (implies (not (equal a b)) 241 (equal (s b y (s a x r)) 242 (s a x (s b y r)))) 243 :rule-classes ((:rewrite :loop-stopper ((b a s))))) 244 245(defthm g-keys-relationship 246 (iff (memberp a (keys r)) 247 (g a r))) 248 249(defthm s-keys-reduction 250 (equal (keys (s a v r)) 251 (if v 252 (insert a (keys r)) 253 (drop a (keys r))))) 254 255(defthm keys-are-ordered 256 (orderedp (keys r))) 257 258(defthm g-of-nil-is-nil 259 (not (g a nil))) 260 261(defthm s-non-nil-cannot-be-nil 262 (implies v (s a v r)) 263 :hints (("Goal" 264 :in-theory (disable rcd->acl2-of-record-non-nil) 265 :use (:instance rcd->acl2-of-record-non-nil 266 (r (s-aux a v (acl2->rcd r))))))) 267 268(defthm non-nil-if-g-non-nil 269 (implies (g a r) r) 270 :rule-classes :forward-chaining) 271 272 273(defthm s-same-g-back-chaining 274 (implies (equal v (g a r)) 275 (equal (s a v r) r))) 276 277 278;; We disable s and g, assuming the rules proven in this book are sufficient to 279;; manipulate record terms which are encountered 280 281(in-theory (disable s g keys)) 282 283(defmacro <- (x a) `(g ,a ,x)) 284 285(defmacro -> (x a v) `(s ,a ,v ,x)) 286 287(defun update-macro (upds result) 288 (declare (xargs :guard (keyword-value-listp upds))) 289 (if (endp upds) result 290 (update-macro (cddr upds) 291 (list 's (car upds) (cadr upds) result)))) 292 293(defmacro update (old &rest updates) 294 (declare (xargs :guard (keyword-value-listp updates))) 295 (update-macro updates old)) 296 297 298 299 300