;;; list-monad.lisp
;;; ACL2 でリストモナドがモナド則を満たしていることを示す
(in-package "ACL2")

;; ACL2 では第一級の関数は使えないため、値としての関数は連想リストで表現する
;; ACL2 には apply$ という限定的な高階関数を実現する機能があるがよく分かってい
;; ないので今回は使用しない
;; https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____APPLY_42?path=3463/6113/3222/31/23
(defmacro apply-function (f x)
  `(cdr (assoc-equal ,x ,f)))

;;; リストモナドの定義
(defmacro unit (x)
  `(list ,x))

(defun bind (x f)
  (cond
    ((endp x) nil)
    (t
     (append (apply-function f (car x))
             (bind (cdr x) f)))))

;;; モナド則を証明するのに必要な関数と定理
;; リストを返す関数かどうかを確認する
(defun to-list-function-p (x)
  (if (endp x)
      t
      (and (true-listp (cdar x))
           (to-list-function-p (cdr x)))))

;; 定義域 s で unit ととして振舞う関数を作成する
(defun make-unit-function (s)
  (cond
    ((endp s) nil)
    (t (acons (car s)
              (unit (car s))
              (make-unit-function (cdr s))))))

;; make-unit-function が定義域 s で
;; unit ととして振舞うことを示す定理
(defthm theorem-of-make-unit-function
  (implies (member e s)
           (equal (apply-function (make-unit-function s) e)
                  (unit e))))

;; append したものを bind するのと
;; bind したものを append するのは同値
(defthm bind-append
  (implies (to-list-function-p g)
           (equal (bind (append x y) g)
                  (append (bind x g)
                          (bind y g)))))

;; 定義域 s で
;; (lambda (x) (bind (apply-function g x) h))
;; を表現する関数
(defun make-apply-and-bind-function (s g h)
  (if (endp s)
      nil
      (acons (car s)
             (bind (apply-function g (car s)) h)
             (make-apply-and-bind-function (cdr s) g h))))

;; 定義域 s で
;; (lambda (x) (bind (apply-function g x) h))
;; ととして振舞うことを示す定理
(defthm theorem-of-make-apply-and-bind-function
  (implies (and (member x s)
                (to-list-function-p g)
                (to-list-function-p h))
           (equal (apply-function (make-apply-and-bind-function s g h) x)
                  (bind (apply-function g x) h))))

;; associativity-of-bind の補助定理
(defthm associativity-of-bind-lemma
  (implies (and (to-list-function-p g)
                (to-list-function-p h)
                (member e s))
           (equal (cdr (assoc-equal e (make-apply-and-bind-function s g h)))
                  (bind (cdr (assoc-equal e g)) h))))

;;; モナド則
;;  unit x >>= f ≡ f x
(defthm left-identity
  (implies (to-list-function-p f)
           (equal (bind (unit x) f)
                  (apply-function f x))))

;;  m >>= unit ≡ m
(defthm right-identity
  (implies (and (true-listp m)
                (subsetp m s))
           (equal (bind m (make-unit-function s))
                  m)))

;; m >>= (\x -> g x >>= h) ≡ (m >>= g) >>= h
(defthm associativity-of-bind
  (implies (and (true-listp m)
                (to-list-function-p g)
                (to-list-function-p h)
                (subsetp m s))
           (equal (bind m (make-apply-and-bind-function s g h))
                  (bind (bind m g) h))))