aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2021-08-22 18:03:09 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2021-08-22 18:03:09 +0900
commit2e3d30de9209a9affd6225cba5f60a9b6ac935e4 (patch)
treea72ca1fa526f44876f86d40383b9a939350e6444
parentbde2eff4a1062f3e8d16bf60c448d20c6f0993f8 (diff)
Update.
-rw-r--r--blackjack.lisp259
1 files 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))