; PR-003: No circle of dependence.  Independent cross-check in Z3.
; Z3 cannot state "circles of every length" in one formula, so it checks
; circles of length 2, 3, 4 and 5.  The general result for every length is
; the Rocq proof.  Z3 assumes a non-empty domain; each check names its own
; things, so that assumption does no work.  No time appears.

(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool)    ; (Gives y x): y gives existence to x
(declare-fun Through (Thing Thing) Bool)  ; (Through x y): x has its existence through y

(define-fun MP001 () Bool   ; what lacks a thing cannot give it
  (forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))
(define-fun MP002 () Bool   ; the receiver has its existence through the giver
  (forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))
(define-fun MP003 () Bool   ; existence through is inherited
  (forall ((x Thing) (y Thing) (z Thing))
    (=> (and (Through x y) (Through y z)) (Through x z))))

(declare-const a Thing)
(declare-const b Thing)
(declare-const c Thing)
(declare-const d Thing)
(declare-const e Thing)

; Circles: a depends on b, b on c, ..., last on a.
(define-fun circle2 () Bool (and (Gives b a) (Gives a b)))
(define-fun circle3 () Bool (and (Gives b a) (Gives c b) (Gives a c)))
(define-fun circle4 () Bool (and (Gives b a) (Gives c b) (Gives d c) (Gives a d)))
(define-fun circle5 () Bool (and (Gives b a) (Gives c b) (Gives d c) (Gives e d) (Gives a e)))

(echo "check 1: MP-001..003 + circle of 2 (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert circle2) (check-sat) (pop)
(echo "check 2: MP-001..003 + circle of 3 (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert circle3) (check-sat) (pop)
(echo "check 3: MP-001..003 + circle of 4 (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert circle4) (check-sat) (pop)
(echo "check 4: MP-001..003 + circle of 5 (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert circle5) (check-sat) (pop)

(echo "check 5: circle of 3 without MP-003 (expect sat: MP-003 is needed)")
(push) (assert MP001) (assert MP002) (assert circle3) (check-sat) (pop)
(echo "check 6: circle of 3 without MP-001 (expect sat: MP-001 is needed)")
(push) (assert MP002) (assert MP003) (assert circle3) (check-sat) (pop)
(echo "check 7: circle of 3 without MP-002 (expect sat: MP-002 is needed)")
(push) (assert MP001) (assert MP003) (assert circle3) (check-sat) (pop)

(echo "check 8: MP-001..003 + straight chain c gives b gives a (expect sat: postulates allow chains)")
(push) (assert MP001) (assert MP002) (assert MP003)
  (assert (and (Gives b a) (Gives c b) (distinct a b c))) (check-sat) (pop)