From 2e3d30de9209a9affd6225cba5f60a9b6ac935e4 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 22 Aug 2021 18:03:09 +0900
Subject: Update.

---
 blackjack.lisp | 259 ++++++++++++++++++++++++++-------------------------------
 1 file changed, 119 insertions(+), 140 deletions(-)

diff --git a/blackjack.lisp b/blackjack.lisp
index 91a055d..4789912 100644
--- a/blackjack.lisp
+++ b/blackjack.lisp
@@ -1,174 +1,153 @@
-(defconst *aces* '(A))
-(defconst *faces* '(J Q K))
-
-(defun acep (x)
-  (declare (xargs :guard t))
-  (and (member x *aces*) t))
-
-(defun facep (x)
-  (declare (xargs :guard t))
-  (and (member x *faces*) t))
-
-(defun rankp (x)
-  (declare (xargs :guard t))
-  (or (acep x)
-      (facep x)
-      (and (natp x)
-           (<= 2 x)
-           (<= x 10))))
-
-(defun scorep (x)
-  (declare (xargs :guard t))
-  (case x
-    ((BUST NATURAL-BLACKJACK) t)
-    (t (and (natp x)
-            (<= x 21)))))
-
-(defun rank-listp (x)
-  (declare (xargs :guard t))
-  (if (atom x)
-      (null x)
-      (and (rankp (car x))
-           (rank-listp (cdr x)))))
-
-(defthm rank-listp-to-true-listp
-  (implies (rank-listp x)
-           (true-listp x))
-  :rule-classes :forward-chaining)
+(in-package "ACL2")
 
-(defun filter-natp (x)
-  (declare (xargs :guard (true-listp x)))
-  (cond ((endp x) nil)
-        ((natp (car x))
-         (cons (car x) (filter-natp (cdr x))))
-        (t (filter-natp (cdr x)))))
+(include-book "standard-52-card-deck/standard-52-card-deck")
 
 (defun sum (x)
   (declare (xargs :guard (nat-listp x)))
   (cond ((endp x) 0)
         (t (+ (car x) (sum (cdr x))))))
 
-(defun filter-facep (x)
-  (declare (xargs :guard (true-listp x)))
+(defun rank-natp-filter (x)
+  (declare (xargs :guard (rank-listp x)))
+  (cond ((endp x) nil)
+        ((natp (car x))
+         (cons (car x) (rank-natp-filter (cdr x))))
+        (t (rank-natp-filter (cdr x)))))
+
+(defun rank-facep-filter (x)
   (cond ((endp x) nil)
-        ((facep (car x))
-         (cons (car x) (filter-facep (cdr x))))
-        (t (filter-facep (cdr x)))))
-
-(defun face-listp (x)
-  (declare (xargs :guard t))
-  (cond ((consp x)
-         (and (facep (car x))
-              (face-listp (cdr x))))
-        (t (null x))))
-
-(defun face-list-to-score (x)
-  (declare (xargs :guard (face-listp x)))
-  (* 10 (length x)))
-
-(defun score-without-aces (rl)
-  (declare (xargs :guard (rank-listp rl)))
-  (+ (sum (filter-natp rl))
-     (face-list-to-score (filter-facep rl))))
+        ((rank-facep (car x))
+         (cons (car x) (rank-facep-filter (cdr x))))
+        (t (rank-facep-filter (cdr x)))))
+
+(defmacro rank-face-list-to-score (x)
+  `(* 10 (len ,x)))
+
+(defmacro score-without-aces (x)
+  `(+ (sum (rank-natp-filter ,x))
+      (rank-face-list-to-score (rank-facep-filter ,x))))
 
 (defthm natp-score-without-aces
-  (implies (rank-listp x)
-           (natp (score-without-aces x))))
+  (let ((s (score-without-aces x)))
+    (and (integerp s)
+         (<= 0 s))))
 
 (defun ace-count (x)
-  (declare (xargs :guard (true-listp x)))
+  (declare (xargs :guard (rank-listp x)))
   (cond ((endp x) 0)
-        ((acep (car x)) (+ 1 (ace-count (cdr x))))
+        ((rank-acep (car x)) (+ 1 (ace-count (cdr x))))
         (t (ace-count (cdr x)))))
 
 (defthm natp-ace-count
-  (implies (rank-listp x)
-           (natp (ace-count x))))
+  (and (integerp (ace-count x))
+       (<= 0 (ace-count x))))
 
-(defun add-ace-scores (s ac)
-  (declare (xargs :guard (and (natp s)
-                              (natp ac))))
-  (cond
-   ((zip ac) s)
-   ((<= (+ s 11) 21) (+ s 11 (- ac 1)))
-   (t (+ s 1 (- ac 1)))))
+(defmacro add-ace-scores (s ac)
+  `(cond
+     ((equal ,ac 0) ,s)
+     ((< (+ ,s 10) 21) (+ ,s 11 (- ,ac 1)))
+     (t (+ ,s 1 (- ,ac 1)))))
 
 (defthm natp-add-ace-scores
-  (implies (and (natp x) (natp y))
-           (natp (add-ace-scores x y))))
-
-(defun nat-score (rl)
-  (declare (xargs :guard (rank-listp rl)))
-  (add-ace-scores (score-without-aces rl)
-                  (ace-count rl)))
-
-(defthm natp-nat-score-1
-  (implies (rank-listp rl)
-           (natp (+ (sum (filter-natp rl))
-                    (* 10 (len (filter-facep rl)))))))
+  (implies (and (integerp x)
+                (<= 0 x)
+                (integerp y)
+                (<= 0 y))
+           (let ((s (add-ace-scores x y)))
+             (and (integerp s)
+                  (<= 0 s)))))
+
+(defmacro nat-score (x)
+  `(add-ace-scores (score-without-aces ,x)
+                   (ace-count ,x)))
 
 (defthm natp-nat-score
-  (implies (rank-listp rl)
-           (natp (nat-score rl))))
-
-(defun score (rl)
-  (declare (xargs :guard (rank-listp rl)))
-  (let ((s (nat-score rl)))
-    (cond
-     ((and (< 21 s)) 'BUST)
-     ((and (= (len rl) 2) (= s 21))
+  (implies (rank-listp x)
+           (and (integerp (nat-score x))
+                (<= 0 (nat-score x))))
+  :rule-classes (:rewrite :forward-chaining))
+
+(defmacro score (x)
+  `(cond
+     ((and (< 21 (nat-score ,x))) 'BUST)
+     ((and (equal (len ,x) 2) (equal (nat-score ,x) 21))
       'NATURAL-BLACKJACK)
-     (t s))))
-
-(defthm scorep-score-1
+     (t (nat-score ,x))))
+
+(defmacro scorep (x)
+  `(or (equal ,x 'bust)
+       (equal ,x 'natural-blackjack)
+       (if (integerp ,x)
+           (if (< ,x 0)
+               nil
+               (< ,x 22))
+           nil)))
+
+(defthm natp-sum
+  (implies (nat-listp x)
+           (and (integerp (sum x))
+                (<= 0 (sum x))))
+  :rule-classes (:rewrite :forward-chaining))
+
+(defthm nat-listp-rank-natp-filter
   (implies (rank-listp x)
-           (natp (+ (sum (filter-natp x))
-                    (* 10 (len (filter-facep x)))))))
+           (rank-nat-listp (rank-natp-filter x)))
+  :rule-classes (:rewrite :forward-chaining))
 
 (defthm scorep-score
   (implies (rank-listp x)
-           (scorep (score x)))
-  :hints (("Goal" :hands-off (add-ace-scores))))
-
-(defun score-judge (player dealer)
-  (declare (xargs :guard (and (scorep player)
-                              (scorep dealer))))
-  (cond
-    ((and (equal player 'NATURAL-BLACKJACK)
-          (equal dealer 'NATURAL-BLACKJACK))
-     'PUSH)
-    ((equal player 'NATURAL-BLACKJACK) 'WIN)
-    ((equal dealer 'NATURAL-BLACKJACK) 'LOSE)
-    ((equal player 'BUST) 'LOSE)
-    ((equal dealer 'BUST) 'WIN)
-    ((< player dealer) 'LOSE)
-    ((> player dealer) 'WIN)
-    (t 'PUSH)))
-
-(defun judge (player dealer)
-  (declare (xargs :guard (and (rank-listp player)
-                              (rank-listp dealer))
-                  :guard-hints (("Goal"
-                                 :hands-off (score)
-                                 :use (scorep-score)))))
-  (score-judge (score player)
-               (score dealer)))
-
-(defthm bust-and-lose
+           (scorep (score x))))
+
+(defmacro score-judge (player dealer)
+  `(cond
+     ((and (equal ,player 'NATURAL-BLACKJACK)
+           (equal ,dealer 'NATURAL-BLACKJACK))
+      'PUSH)
+     ((equal ,player 'NATURAL-BLACKJACK) 'WIN)
+     ((equal ,dealer 'NATURAL-BLACKJACK) 'LOSE)
+     ((equal ,player 'BUST) 'LOSE)
+     ((equal ,dealer 'BUST) 'WIN)
+     ((< ,player ,dealer) 'LOSE)
+     ((> ,player ,dealer) 'WIN)
+     (t 'PUSH)))
+
+(defmacro judge (player dealer)
+  `(score-judge (score (card-list-to-rank-list ,player))
+                (score (card-list-to-rank-list ,dealer))))
+
+(defmacro judgementp (x)
+  `(or (equal ,x 'NATURAL-BLACKJACK)
+       (equal ,x 'BUST)
+       (equal ,x 'LOSE)
+       (equal ,x 'WIN)
+       (equal ,x 'PUSH)))
+
+(defthm judgementp-score-judge
+  (judgementp (score-judge p d)))
+
+(defthm if-bust-then-lose
   (equal (score-judge 'BUST x) 'LOSE))
 
-(defthm draw-a-face-and-blackjack
-  (implies (facep r)
-           (equal (score (list 'A r))
+(defthm if-draw-a-face-card-and-have-a-ace-card-only-then-natural-blackjack
+  (implies (and (rank-facep face)
+                (rank-acep ace))
+           (equal (score (list ace face))
                   'NATURAL-BLACKJACK)))
 
-(defthm bust-12
-  (let ((rs '(K 2))
-        (new 'J))
-    (and (= (nat-score rs) 12)
-         (equal (score (cons new rs)) 'BUST))))
+(defun no-rank-acep (x)
+  (if (endp x)
+      t
+      (and (not (rank-acep (car x)))
+           (no-rank-acep (cdr x)))))
+
+(defthm if-draw-a-face-when-12-then-bust
+  (implies (and (rank-listp rs)
+                (no-rank-acep rs)
+                (rank-facep face)
+                (equal (nat-score rs) 12))
+           (equal (score (cons face rs)) 'BUST)))
 
-(defthm safe-hit
+(defthm safe-to-hit
   (implies (and (rank-listp rs)
                 (rankp new)
                 (<= (nat-score rs) 11))
-- 
cgit v1.2.3