(load-file "elms-defs.ath")

(load-file "parse.ath")

;; Transitivity of the subset relation:

(define subset-trans "ALL s1 s2 s3 | (s1 subset s2) & (s2 subset s3) ==> s1 subset s3")

(!pf subset-trans [subset-axiom])

;; A useful set-theory lemma: 
   
(define union-lemma-1 "ALL s1 s2 s | (s1 subset s) & (s2 subset s) ==> (s1 union s2) subset s")

(!pf union-lemma-1 [subset-axiom union-axiom])


(define dot-theorem
  (pick-any s1 s2 R
     (assume-let ((hyp1 "s1 subset s2"))
       (dlet ((goal "ALL t | t in s1.R ==> t in s2.R")
	      (P (structure-cases goal
                   ((cons y unit) 
                      (assume-let ((hyp2 "[y] in s1.R"))
                        (!pf "[y] in s2.R" [hyp2 hyp1 subset-axiom sbdot-axiom]))))))
         (!pf "s1.R subset s2.R" [P subset-axiom])))))

(define cons-axiom
  (forall* [?S ?R ?t] 
   (if (in ?t (sbdot ?S ?R)) 
       (exists ?y (= ?t (cons ?y unit))))))

(define dt
  (pick-any s1 s2 R
     (assume-let ((hyp1 "s1 subset s2"))
       (dlet ((goal "ALL t | t in s1.R ==> t in s2.R"))
         (pick-any t
           (assume-let ((hyp2 "t in s1.R"))
              (!pf "t in s2.R" [hyp1 hyp2 sbdot-axiom id-axiom cons-axiom subset-axiom])))))))

(define dt'
  (pick-any s1 s2 R
     (assume-let ((hyp1 "s1 subset s2"))
        (!pf "s1.R subset s2.R" [hyp1 sbdot-axiom id-axiom cons-axiom subset-axiom]))))

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

(define scalar-lemma "ALL x y R | [y] in {[x]}.R <==> [x y] in R")

(!pf scalar-lemma [sbdot-axiom singleton-axiom cons-injectivity id-axiom])

;A useful lemma for power:

(define psl "ALL x y z R k1 k2 | [x y] in R^k1 & [y z] in R^k2 ==> [x z] in R^(k1+k2)")

(define (goal k)
  (forall* [?x ?y ?z ?R ?k2]
    (if (and (holds (pow ?R k) [?x ?y]) 
             (holds (pow ?R ?k2)  [?y ?z]))
        (holds (pow ?R (+ k ?k2)) [?x ?z]))))

(define (all-props) (fetch-all (function (P) true)))

(define power-sum-lemma
  (by-induction-on ?k1 (goal ?k1)
    (zero (!pf (goal zero) [plus-axiom-1 pow-axiom-1 id-axiom]))
    ((succ k) (dlet ((ind-hyp (goal k)))
                (!pf (goal (succ k)) [plus-axiom-2 pow-axiom-2 ind-hyp id-axiom])))))

(define comp-monotonicity "ALL n m R | [m] in {[n]}.R* ==> {[m]}.R* subset {[n]}.R*")

(pick-any n m R
  (assume-let ((hyp "[m] in {[n]}.R*"))
     (dlet ((goal "ALL x | x in {[m]}.R* ==> x in {[n]}.R*")
            (inc (structure-cases goal
                   ((cons y unit) (assume-let ((hyp' "[y] in {[m]}.R*"))
                                    (!pf "[y] in {[n]}.R*" [hyp hyp' power-sum-lemma rtc-axiom scalar-lemma]))))))
        (!pf "{[m]}.R* subset {[n]}.R*" [inc subset-axiom]))))

(!claim comp-monotonicity)			           

; Lemma: ALL n, R | (n,n) in R^0

(define rtc-zero-lemma
  (pick-any n
    (pick-any R
      (dlet ((P1 (!eq-reflex n)))
	((in (tup [n n]) (pow R zero)) BY (!fire pow-axiom-1 [R n n]))))))

(!pf rtc-zero-lemma [pow-axiom-1 id-axiom])

; Lemma: ALL n, R | (n,n) in R*

(define reflex-clos-lemma  "ALL n R | [n n] in R*")

(!pf reflex-clos-lemma [pow-axiom-1 rtc-axiom id-axiom])

;; Another simple lemma: ALL x, y, R | (x,y) in R ==> (x,y) in R^1

(define first-power-lemma 
  (forall* [?x ?y ?R] (if (in (tup [?x ?y]) ?R)
                          (in (tup [?x ?y]) (pow ?R (succ zero))))))

(!pf first-power-lemma [rtc-zero-lemma id-axiom pow-axiom-2])
                     
;; And a similar one: ALL x, y, R | (x,y) in R ==> (x,y) in R^*

(define first-power-lemma-1 "ALL x, y, R | (x,y) in R ==> (x,y) in R*"

(define first-power-lemma-1
 (pick-any x 
  (pick-any y
    (pick-any R
      (assume-let ((hyp (holds R [x y])))
        (dlet ((P1 ((holds (pow R (succ zero)) [x y]) BY (!fire first-power-lemma [x y R])))
	       (P2 (!egen (exists ?k (holds (pow R ?k) [x y])) (succ zero))))
          (!fire rtc-axiom [R x y])))))))

(!pf first-power-lemma-1 [first-power-lemma rtc-axiom])
          
; Prove: ALL n, R | {(n)} subset n.R*

(define subset-ref-lemma "ALL n R | {[n]} subset {[n]}.R*")

(!pf subset-ref-lemma [reflex-clos-lemma cons-injectivity scalar-lemma subset-axiom id-axiom])

(define subset-ref-lemma
  (pick-any n
    (pick-any R
      (dlet ((P (by-induction-on ?x (if (in ?x (scalar n)) (in ?x (sbdot (scalar n) (rtc R))))
	  	  ((cons x unit) 
		     (assume (in (tup [x]) (scalar n))
                       (dlet ((P1 ((= n x) BY (!eq-symmetry2 (!eq-tup-parts (in (tup [x]) (scalar n))))))
			      (P2 ((in (tup [n n]) (rtc R)) BY (!uspec* reflex-clos-lemma [n R])))
			      (P3 ((in (tup [n]) (sbdot (scalar n) (rtc R))) 
				    BY (!fire scalar-lemma [n n (rtc R)]))))
                         (!rec-rel-cong P3 (in (tup [x]) (sbdot (scalar n) (rtc R))))))))))
        (!fire subset-axiom [(scalar n) (sbdot (scalar n) (rtc R))])))))

            

(define lemma-L1
  (pick-any n
    (dlet ((P1 (!uspec* subset-ref-lemma [n next]))
	   (P2 (!fire dot-th [(scalar n) (sbdot (scalar n) (rtc next)) data])))
      $P2)))


(define (exp1 n)
  (sbdot (scalar n) (rtc next)))

(define (exp2 n)
  (sbdot (exp1 n) data))

(define (ind-goal n)
  (subset (elms n) (exp2 n)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define base-step
  (pick-any n
    (assume-let ((hyp (not (exists ?m (holds next [n ?m])))))
      (dlet ((P1 ((= (elms n) (sbdot (scalar n) data)) 
                  BY (!mp (!left-and (!uspec elms-semantics n)) hyp)))
	     (P2 (!uspec lemma-L1 n)))
        (!rec-rel-cong P2 (subset (elms n) (sbdot (sbdot (scalar n) (rtc next)) data)))))))


(define ind-step
  (pick-any n 
    (pick-any m
      (assume-let ((hyp (holds next [n m]))
                   (ihyp (ind-goal m)))
        (dlet ((P1 ((= (elms n) (union (sbdot (scalar n) data) (elms m))) 
	  	    BY (!mp (!uspec (!right-and (!uspec elms-semantics n)) m) hyp)))
               (P2 ((holds (rtc next) [n m]) BY (!fire first-power-lemma-1 [n m next])))
	       (P3 ((in (tup [m]) (sbdot (scalar n) (rtc next))) BY (!fire scalar-lemma [n m (rtc next)])))
	       (P4 ((subset (exp1 m) (exp1 n)) BY (!fire comp-monotonicity [n m next])))
	       (P5 ((subset (exp2 m) (exp2 n)) BY (!fire dot-th [(exp1 m) (exp1 n) data])))
	       (P6 ((subset (elms m) (exp2 n)) BY (!fire subset-trans [(elms m) (exp2 m) (exp2 n)])))
	       (P7 ((subset (sbdot (scalar n) data) (exp2 n)) BY (!uspec lemma-L1 n)))
               (P8 ((subset (union (sbdot (scalar n) data) (elms m)) (exp2 n)) 
		    BY (!fire union-theorem-1 [(sbdot (scalar n) data) (elms m) (exp2 n)]))))
         (!rec-rel-cong P8 (subset (elms n) (exp2 n))))))))
             

(assert acyclicity)

(define inductive-proof
  (!list-induction ind-goal))
    
	  
      
         

; (load-file "elms2.ath")
; (load-file "elm-lemmas.ath") 
; (load-file "elms-proofs.ath")
;