Developing a function (cart-prod a b) to compute the cartesian product of two lists a and b and proving it sound and complete.

cartesian-product.lisp

;; Note: This is a work in progress
;;
;; A function (cart-prod a b) is developed here that computes the cartesian
;; product of two lists.
;;
;; For example:
;;
;; (cart-prod '(1 2 3) '(a b)) => ((1 a) (1 b) (2 a) (2 b) (3 a) (3 b))
;;
;; The function cart-prod is proven sound and complete by the theorems
;; cart-prod-complete and cart-prod-sound respectively.
;;
;; These are stated below as follows:
;;
;; (defthm cart-prod-complete
;;   (implies (and
;;             (member-equal x a)
;;             (member-equal y b))
;;            (member-equal (list x y)
;;                          (cart-prod a b))))
;;
;; (defthm cart-prod-sound
;;   (all-pairs-can-be-explained
;;    (cart-prod a b)
;;    a
;;    b))

;; Note for myself
;; I invoked
;; (set-ld-redefinition-action '(:doit . :overwrite) state)
;; to enable redefinitions

(progn
  (defun comb (x l)
    "Combine X with all elts of L."
    (if (endp l)
        nil
      (cons (list x (car l))
            (comb x (cdr l)))))
  (defun cart-prod (a b)
    (declare (ignorable a b))
    (if (endp a)
        nil
      (append
       ;; (list (list 1 2)) ;make it unsound :-D
       (comb (car a) b)
       (cart-prod (cdr a) b))))
  (defthm about-comb
    (implies (member-equal y b)
             (member-equal (list x y)
                           (comb x b))))
  (defthm member-append
    (iff (member-equal x (append a b))
         (or (member-equal x a)
             (member-equal x b))))
  ;; complete
  (defthm help1
    (implies (and
              ;; (member x a)
              (member-equal y b)
              (equal x (car a))
              ;; (equal y (car b))
              (consp a)
              ;; (consp b)
              )
             (member-equal (list x y)
                           (cart-prod a b))))
  (defthm help2
    (implies (and
              ;; (member x a)
              (member-equal x a)
              (equal y (car b))
              ;; (equal y (car b))
              ;; (consp a)
              (consp b)
              )
             (member-equal (list x y)
                           (cart-prod a b))))
  (defthm cart-prod-complete
    (implies (and
              (member-equal x a)
              (member-equal y b))
             (member-equal (list x y)
                           (cart-prod a b))))
  )

(progn
  (defun all-pairs-can-be-explained (pairs a b)
    (if (endp pairs)
        t
      (let ((pair (car pairs)))
        (case-match
         pair
         ((x y)
          (and (member-equal x a)
               (member-equal y b)
               (all-pairs-can-be-explained (cdr pairs) a b)))))))
  (thm
   (and
    (all-pairs-can-be-explained
     '((1 2) (3 4) (5 6))
     '(1 3 5)
     '(2 4 6))
    (not
     (all-pairs-can-be-explained
      '((1 2) (3 4) (x y) (5 6))
      '(1 3 5)
      '(2 4 6)))))
  (defthm cart-prod-sound
    (all-pairs-can-be-explained
     (cart-prod a b)
     a
     b)))