(load-file defs)

(domain Set)

(declare member (-> (Set Set) Boolean))

(define (subset ?x ?y)
  (forall ?w
    (if (member ?w ?x)
        (member ?w ?y))))

(define (is-empty ?x)
  (forall ?w (not (member ?w ?x))))

(define EXTENSIONALITY-AXIOM
  (forall ?x 
    (forall ?y
      (iff (equal ?x ?y)
           (and (subset ?x ?y)
                (subset ?y ?x))))))

(assert EXTENSIONALITY-AXIOM)

(define (subsets=>equal set1 set2)
  (!mp (!right-iff (!uspec-list EXTENSIONALITY-AXIOM [set1 set2]))
       (!both (subset set1 set2) (subset set2 set1))))


(define (equal=>subsets set1 set2)
  (!left-and (!mp (!left-iff (!uspec-list EXTENSIONALITY-AXIOM [set1 set2]))
                  (equal set1 set2))))

                                             
(define (subsets=>equal2 set1 set2)
  (dbegin (!subset-intro set1 set2)
          (!subset-intro set2 set1)
          (!subsets=>equal set1 set2)))


(define null-is-unique
  (pick-any x
    (pick-any y
      (assume-let ((both-empty (and (is-empty x) 
                                    (is-empty y))))
        (dlet ((x-is-empty (!left-and both-empty))
               (y-is-empty (!right-and both-empty))
               (x-subset-y (pick-any w
                             (dlet ((p (assume (not (member w y))
                                         (!uspec (!is-empty-elim x) w))))
                               (!contra2 p))))
               (y-subset-x (pick-any w
                             (dlet ((p (assume (not (member w x))
                                         (!uspec (!is-empty-elim y) w))))
                               (!contra2 p)))))
        (!subsets=>equal2 x y))))))

(define NULL-AXIOM
  (exists ?x (is-empty ?x)))

(assert NULL-AXIOM)

(define exists-unique-empty-set
  (pick-witness NULL-AXIOM null
     (!egen-unique (exists-unique ?s (is-empty ?s)) null)))
    
(define-symbol null-set
  (the ?x (is-empty ?x)))

(define (is-pair-of ?x ?y ?z)
  (forall ?w 
    (iff (member ?w ?z)
         (or (equal ?w ?x)
             (equal ?w ?y)))))

(define PAIRING-AXIOM
  (forall ?x 
    (forall ?y
      (exists ?z
        (is-pair-of ?x ?y ?z)))))

(assert PAIRING-AXIOM)

(define at-most-one-pair
  (method (x y)
    (pick-any z1 
      (pick-any z2
        (assume-let ((both-are-xy-pairs (and (is-pair-of x y z1)
                                             (is-pair-of x y z2))))
          (dlet ((z1-is-xy-pair (!left-and both-are-xy-pairs))
                 (z2-is-xy-pair (!right-and both-are-xy-pairs))
                 (pair-cond-z1  (!is-pair-of-elim x y z1))
                 (pair-cond-z2  (!is-pair-of-elim x y z2))
                 (z1-subset-z2  (pick-any w
                                  (assume-let ((w-in-z1 (member w z1)))
                                     (dlet ((w=x\/w=y (!mp (!left-iff (!uspec pair-cond-z1 w)) w-in-z1))
                                            (w-in-z2 (!mp (!right-iff (!uspec pair-cond-z2 w)) w=x\/w=y)))
                                       $w-in-z2))))
                 (z2-subset-z1  (pick-any w
                                  (assume-let ((w-in-z2 (member w z2)))
                                   (dlet ((w=x\/w=y (!mp (!left-iff (!uspec pair-cond-z2 w)) w-in-z2))
                                          (w-in-z1 (!mp (!right-iff (!uspec pair-cond-z1 w)) w=x\/w=y)))
                                     $w-in-z1)))))
            (!subsets=>equal2 z1 z2)))))))

(define pair-uniqueness
  (pick-any x
    (pick-any y
      (pick-witness (!uspec-list PAIRING-AXIOM [x y]) z
        (dlet ((uniqueness (!at-most-one-pair x y)))
          (!egen-unique (exists-unique z (is-pair-of x y z)) z))))))


(define (pair-of ?x ?y)
  (the ?z (is-pair-of ?x ?y ?z)))

;;
;; The following method takes any three terms w, x, and y, and 
;; outputs the theorem (iff (member w (pair-of x y)) 
;;                          (or (equal w x) (equal w y)))                
;;

(define pair-membership
  (method (w x y)
    (dlet ((_ (!pair-of-definition x y))
           (pair-cond (!is-pair-of-elim x y (pair-of x y))))
      (!uspec pair-cond w))))

;;
;; Thus we can now derive the general (universally quantified) theorem
;; (forall ?w ?x ?y
;;   (iff (member ?w (pair-of ?x ?y))
;;        (or (equal ?w ?x) (equal ?w ?y))))
;;  
;; simply by applying the preceding method to arbitrarily-picked w, x, and y!! 
;; Observe how simple and intuitive it is:

(define pair-characterization
  (pick-any w
    (pick-any x
      (pick-any y
        (!pair-membership w x y)))))

;;
;; Next, the following method derives either (1) (or (equal w x) (equal w y))
;; from the assumption that (member w (pair-of x y))
;; or (2) (member w (pair-of x y)) from the assumption 
;; (or (equal w x) (equal w y))
;;

(define get-from-pair-definition 
  (method (P)
    (dmatch P 
      ((or (equal w x) (equal w y))
         (dlet ((conditional (!left-iff (!pair-membership w x y))))
           (!mp conditional (member w (pair-of x y)))))
      ((member w (pair-of x y))
         (dlet ((conditional (!right-iff (!pair-membership w x y))))
           (!mp conditional (or (equal w x) (equal w y))))))))

;;
;; The next method takes any two terms x and y and outpus the
;; theorem (subset (pair-of x y) (pair-of y x))
;;

(define pair-subset
  (method (x y)
    (dbegin (pick-any w 
              (assume (member w (pair-of x y))
                (dlet ((w=x\/w=y (!get-from-pair-definition (or (equal w x) 
                                                                (equal w y))))
                       (w=y\/w=x (!swap-disjunction w=x\/w=y))) 
                  (!get-from-pair-definition (member w (pair-of y x))))))
            (!subset-intro (pair-of x y) (pair-of y x))))) 

;; The next method takes any two terms x and y and outputs
;; the commutativity theorem (equal (pair-of x y) (pair-of y x))
;;

(define show-pair-commutativity
  (method (x y)
    (dbegin (!pair-subset x y)
            (!pair-subset y x)
            (!subsets=>equal (pair-of x y) (pair-of y x)))))

;; We can now establish the general commutativity of pairing, expressed
;; as a universally quantified proposition, in a very straightforward manner:
;;

(define pairing-is-commutative
  (pick-any x 
    (pick-any y
      (!show-pair-commutativity x y))))


(define (singleton ?x)
  (pair-of ?x ?x))


;; The following method takes an element x and two sets s1, s2
;; and, on the assumptions that (member x s1) and (subset s1 s2) 
;; it derives the theorem (member x s2)

(define (subsets-member x s1 s2)
  (!mp (!uspec (!subset-elim s1 s2) x)
       (member x s1)))


;; The following method takes any two terms w and x 
;; and outputs the theorem (if (member w (singleton x))
;;                             (equal w x))

(define (singleton-membership w x)
  (assume (member w (singleton x))
    (dbegin (!singleton-definition x)
            (!equal=>subsets (singleton x) (pair-of x x))
            (!subsets-member w (singleton x) (pair-of x x))
            (!get-from-pair-definition (or (equal w x) (equal w x)))
            (!simplify-or (equal w x)))))


(define (singleton-membership2 w x)
  (assume (member w (singleton x))
    (dbegin (!beta-reduce (singleton x) (member w (singleton x)))
            (!get-from-pair-definition (or (equal w x) (equal w x)))
            (!simplify-or (equal w x)))))


;; Now we easily derive the theorem (forall ?w (if (member ?w (singleton ?x))
;;                                                 (equal ?w ?x))):

(pick-any w 
  (pick-any x
    (!singleton-membership w x)))


(define (tuple ?x ?y)
  (pair-of ?x (pair-of ?x ?y)))


(define (plus ?x ?y)
 (match ?x
   (zero ?y)
   ((succ ?n) (succ (plus ?n ?y)))))



