Created
January 5, 2024 13:28
-
-
Save kisp/39cf758f14f99bd365e0abcfbd596c39 to your computer and use it in GitHub Desktop.
Developing a function (cart-prod a b) to compute the cartesian product of two lists a and b and proving it sound and complete.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; 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))) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment