(load-file "equal.ath")
(load-file "tuple.ath")

(domain (Set-Of T))

(declare in ((T) -> (T (Set-Of T)) Boolean))

(declare empty ((T) -> ((Set-Of T)) Boolean))

(declare null ((T) (Set-Of T)))

(define null-def (forall ?x (not (in ?x null))))

(define empty-def
  (forall ?s
    (iff (empty ?s)
      (forall ?x (not (in ?x ?s))))))


(assert empty-def)


(declare singl ((T) -> (T) (Set-Of T)))

(define singleton-def
  (forall ?x
    (forall ?y 
      (iff (in ?x (singl ?y))
	   (= ?x ?y)))))

(define singleton-def-1
  (forall ?x (in ?x (singl ?x))))

(assert singleton-def singleton-def-1)

(define singleton-hc-1 
  (forall* [?x ?y]
   (if (= ?x ?y)
       (in ?x (singl ?y)))))

(assert singleton-hc-1)

(declare is-singleton ((T) -> ((Set-Of T)) Boolean))

(define is-singleton-def
  (forall ?s
    (iff (is-singleton ?s)
	 (exists ?x (= ?s (singl ?x))))))

(assert is-singleton-def)            

(declare subset ((T) -> ((Set-Of T) (Set-Of T)) Boolean))

(define subset-def 
  (forall ?s1
    (forall ?s2
      (iff (subset ?s1 ?s2)
           (forall ?x
             (if (in ?x ?s1)
                 (in ?x ?s2)))))))

(assert subset-def)

(define set-ext
  (forall ?s1
    (forall ?s2
      (iff (= ?s1 ?s2)
	   (forall ?x
	     (iff (in ?x ?s1)
		  (in ?x ?s2)))))))

(assert set-ext)

(define set-equality
  (forall ?s1 ?s2
    (iff (= ?s1 ?s2)
	 (and (subset ?s1 ?s2) (subset ?s2 ?s1)))))

(define prove pf)

(!prove set-equality [set-ext subset-def])

(declare union ((T) -> ((Set-Of T) (Set-Of T)) (Set-Of T)))

(declare intersection ((T) -> ((Set-Of T) (Set-Of T)) (Set-Of T)))

(define union-def
  (forall ?s1 
    (forall ?s2
      (forall ?x
        (iff (in ?x (union ?s1 ?s2))
             (or (in ?x ?s1)
                 (in ?x ?s2)))))))

(assert union-def)

(define union-hc-1
  (forall* [?s1 ?s2 ?x]
    (if (in ?x ?s1)
	(in ?x (union ?s1 ?s2)))))

(define union-hc-2
  (forall* [?s1 ?s2 ?x]
    (if (in ?x ?s2)
	(in ?x (union ?s1 ?s2)))))

(assert union-hc-1 union-hc-2)

;(structure (Pair-Of S T)
;  (cons S T))

;(structure Unit
;  unit)

;(define cons-injectivity (!constructor-injectivity cons))

(define (tup terms)
  (match terms
    ([x] x)
    ([x y] (pair x y))
    ([x y z] (triple x y z))))

;; (define (tup terms)
;;   (match terms
;;     ([] unit)
;;     ((list-of t rest) (cons t (tup rest)))))

;; (define (tup1 x) (tup [x]))
;; (define (tup2 x y) (tup [x y]))
;; (define (tup3 x y z) (tup [x y z]))

(define (holds R args)
  (in (tup args) R))

(define (scalar n)
  (singl (tup [n])))

(define (binary-relations? s1 s2)
  (let ((v (fresh-var)))
    (match (sort-of-var v (in v (union s1 s2)))
      ((split "(Pair-Of " _) true)
      (_ false))))

(define (prove-subsets s1 s2 hyps) 
  (dlet ((v (fresh-var))
	 (P (forall v (if (in v s1) (in v s2)))))
    (dmatch (binary-relations? s1 s2)
      (true (dlet ((inclusion (structure-cases P
	                        ((pair y1 y2) (!prove (if (in (tup [y1 y2]) s1) (in (tup [y1 y2]) s2)) hyps)))))
              (!prove (subset s1 s2) [inclusion subset-def])))
      (_ (dlet ((inclusion (pick-any v (!prove (if (in v s1) (in v s2)) hyps))))
           (!prove (subset s1 s2) [inclusion subset-def]))))))

(define (prove-subsets' S1 S2 hyps)
  (dlet ((P (pick-any x
              (assume (in x S1)
                (!prove (in x S2) (add (in x S1) hyps))))))
    (!prove (subset S1 S2) [P subset-def])))

(define (prove-set-equality S1 S2 hyps)
  (dlet ((P1 (!prove-subsets S1 S2 hyps))
         (P2 (!prove-subsets S2 S1 hyps)))
    (!prove (= S1 S2) [P1 P2 set-equality])))

(define (prove-set-equality' S1 S2 hyps)
  (dlet ((P1 (!prove-subsets' S1 S2 hyps))
         (P2 (!prove-subsets' S2 S1 hyps)))
    (!prove (= S1 S2) [P1 P2 set-equality])))




(declare left-set ((S T) -> ((Set-Of (Pair-Of S T))) (Set-Of S)))

(define left-set-def
  (forall ?r 
    (forall ?x 
         (iff (in ?x (left-set ?r))
              (exists ?y
                 (in (pair ?x ?y) ?r))))))

(assert left-set-def)

(declare is-fun ((S T) -> ((Set-Of (Pair-Of S T))) Boolean))

(define is-fun-def
  (forall ?R
    (iff (is-fun ?R)
         (forall ?x ?y1 ?y2
           (if (and (in (pair ?x ?y1) ?R)
                    (in (pair ?x ?y2) ?R))
               (= ?y1 ?y2))))))

(assert is-fun-def)

(declare is-total-fun ((S T) -> ((Set-Of S) (Set-Of (Pair-Of S T))) Boolean))

(define is-total-fun-def
  (forall ?S
    (forall ?f
      (iff (is-total-fun ?S ?f)
           (and (is-fun ?f)
                (forall ?x 
                  (if (in ?x ?S)
                      (exists ?y
                        (in (pair ?x ?y) ?f)))))))))

(assert is-total-fun-def)

(declare tran ((S) -> ((Set-Of (Pair-Of S S))) Boolean))

(define tran-def
  (forall ?R
    (iff (tran ?R)
         (forall ?x 
            (forall ?y
              (forall ?z
                 (if (and (in (tup [?x ?y]) ?R)
                          (in (tup [?y ?z]) ?R))
                     (in (tup [?x ?z]) ?R))))))))

(assert tran-def)

(structure Nat
  zero
  (succ Nat))

(define one (succ zero))

(declare + (-> (Nat Nat) Nat))

(define plus-def-1 
  (forall ?x 
    (= (+ zero ?x) ?x)))

(define plus-def-2
  (forall ?x 
    (forall ?y
      (= (+ (succ ?x) ?y) (succ (+ ?x ?y))))))

(assert plus-def-1 plus-def-2)

(declare tc ((S) -> ((Set-Of (Pair-Of S S))) 
                    (Set-Of (Pair-Of S S))))

(declare pow ((S) -> ((Set-Of (Pair-Of S S)) Nat)
                      (Set-Of (Pair-Of S S))))

(define pow-def
  (and
    (forall ?R ?x ?y
      (iff (in (tup [?x ?y]) (pow ?R zero))
           (= ?x ?y)))
    (forall ?R ?k ?x ?y
      (iff (in (tup [?x ?y]) (pow ?R (succ ?k)))
           (exists ?z
             (and (in (tup [?x ?z]) ?R)
                  (in (tup [?z ?y]) (pow ?R ?k))))))))

(define pow-def-1
  (forall ?R 
    (forall ?x
      (forall ?y
        (iff (in (tup [?x ?y]) (pow ?R zero))
             (= ?x ?y))))))

(define pow-def-hc1
  (forall ?R 
    (forall ?x
      (forall ?y
        (if (= ?x ?y)
	    (in (tup [?x ?y]) (pow ?R zero)))))))

(define pow-def-2
  (forall ?R
    (forall ?k
      (forall ?x
        (forall ?y
          (iff (in (tup [?x ?y]) (pow ?R (succ ?k)))
               (exists ?z
                 (and (holds ?R [?x ?z])
                      (holds (pow ?R ?k) [?z ?y])))))))))

(define pow-def-hc2
  (forall* [?R ?k ?x ?y ?z]
    (if (and (holds ?R [?x ?z])
             (holds (pow ?R ?k) [?z ?y]))
        (in (tup [?x ?y]) (pow ?R (succ ?k))))))

(define pow-def-hc3
  (forall ?R
    (forall ?k
      (forall ?x
        (forall ?y
          (if (in (tup [?x ?y]) (pow ?R (succ ?k)))
              (exists ?z
                (and (holds ?R [?x ?z])
                     (holds (pow ?R ?k) [?z ?y])))))))))

(assert pow-def-1 pow-def-2 pow-def-hc1 pow-def-hc2 pow-def-hc3)
 
(define tc-def
  (forall ?R
    (forall ?x
      (forall ?y
        (iff (holds (tc ?R) [?x ?y])
             (exists ?k
               (holds (pow ?R (succ ?k)) [?x ?y])))))))

(assert tc-def)

(define tc-def-hc
  (forall ?R
    (forall ?x
      (forall ?y
        (forall ?k
          (if (holds (pow ?R (succ ?k)) [?x ?y])
              (holds (tc ?R) [?x ?y])))))))

(assert tc-def-hc)

(declare rtc ((S) -> ((Set-Of (Pair-Of S S))) 
                      (Set-Of (Pair-Of S S))))

(define rtc-def
  (forall ?R
    (forall ?x
      (forall ?y
        (iff (holds (rtc ?R) [?x ?y])
             (exists ?k
               (holds (pow ?R ?k) [?x ?y])))))))


(assert rtc-def)

(define rtc-def-hc
  (forall ?R
    (forall ?x
      (forall ?y
	(forall ?k
          (if (holds (pow ?R ?k) [?x ?y])
              (holds (rtc ?R) [?x ?y])))))))

(assert rtc-def-hc)

;; (define (forall* var-list P)
;;   (match var-list
;;     ([] P)
;;     ((list-of avar rest) (forall avar (forall* rest P)))))

;; (define (exists* var-list P)
;;   (match var-list
;;     ([] P)
;;     ((list-of avar rest) (exists avar (exists* rest P)))))


;; (declare dot ((T1 T2 T3) -> ((Set-Of (Pair-Of T1 (Pair-Of T2 Unit))) 
;; 			     (Set-Of (Pair-Of T2 (Pair-Of T3 Unit))))
;; 			     (Set-Of (Pair-Of T1 (Pair-Of T3 Unit)))))

(declare inv ((T1 T2) -> ((Set-Of (Pair-Of T1 T2)))
			  (Set-Of (Pair-Of T2 T1))))

;; Darko: explanining composition operators to Lev
;;      r1.r2
;; r1: T1 x T2 x ... x Tn-1 x U
;; r2: U x S2 x ... x Sm
;; r1.r2: T1 x T2 x ... x Tn-1 x S2 x ... x Sm

;; <t1 ... tn-1, s2, ..., sm> \in r1.r2 <=>
;; exists u | <t1 ... tn-1, u> \in r1 /\ <u, s2, ..., sm> \in r2

;; sbdot = comp-1-2
(declare sbdot ((S T) -> ((Set-Of S) (Set-Of (Pair-Of S T)))
                          (Set-Of T)))
(define sbdot-ax
  (forall ?y ?S ?R
    (iff (in ?y (sbdot ?S ?R))
         (exists ?x
           (and (in ?x ?S)
                (in (pair ?x ?y) ?R))))))
(assert sbdot-ax)

(declare bbdot ((S T U) -> ((Set-Of (Pair-Of S T)) (Set-Of (Pair-Of T U)))
                            (Set-Of (Pair-Of S U))))
(define bbdot-ax
  (forall ?y ?z ?S ?R
    (iff (in (pair ?y ?z) (bbdot ?S ?R))
         (exists ?x
           (and (in (pair ?y ?x) ?S)
                (in (pair ?x ?z) ?R))))))
(assert bbdot-ax)

(declare comp-1-3 ((S T R) -> ((Set-Of S) (Set-Of (Triple-Of S T R)))
                               (Set-Of (Pair-Of T R))))
(define comp-1-3-ax
  (forall* [?y ?z ?S ?R]
    (iff (in (pair ?y ?z) (comp-1-3 ?S ?R))
         (exists ?x
           (and (in ?x ?S)
                (in (triple ?x ?y ?z) ?R))))))
(assert comp-1-3-ax)

(define inv-def
  (forall ?R ?x ?y
    (iff (in (tup [?x ?y]) (inv ?R))
	 (in (tup [?y ?x]) ?R))))

(assert inv-def)

(define sbdot-def
  (forall ?R
    (forall ?scalars
      (forall ?y
        (iff (in (tup [?y]) (sbdot ?scalars ?R))
             (exists ?x 
               (and (in (tup [?x]) ?scalars)
                    (in (tup [?x ?y]) ?R))))))))

(assert sbdot-def)

(define id-axiom (forall ?x (= ?x ?x)))

(assert id-axiom)