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

(load-file "parse.ath")

; The following method takes two sets s1, s2 such that
;; (s1 subset s2) and an element x in s1 and proves x in s2:

(primitive-method (pf P props) (match (prove-from P props)
                                 (true P)
				 (_ (print ("\nOtter failed.")))))

(define (os p) (print (head (make-otter-prop-string [p]))))


(define (subset-method s1 s2 x)
  (!fire (!fire subset-axiom [s1 s2]) [x]))


;; Transitivity of the subset relation:

(define subset-trans
  (forall* [?s1 ?s2 ?s3]
    (if (and (subset ?s1 ?s2) (subset ?s2 ?s3))
        (subset ?s1 ?s3))))

(!prove-from subset-trans [subset-axiom])


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

(!prove-from subset-trans-1 [subset-axiom])

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

(define union-theorem-1 
  (forall* [?s1 ?s2 ?s]
    (if (and (subset ?s1 ?s)
	     (subset ?s2 ?s))
	(subset (union ?s1 ?s2) ?s))))

(define union-th-1 "ALL s1 s2 s | (s1 subset s) & (s2 subset s) ==> (s1 union s2) subset s")

(!prove-from union-th-1 [subset-axiom union-axiom])


;; Another useful result: ALL s1, s2, R | s1 subset s2 ==> (s1 . R) subset (s2 . R)

(define dot-th' 
  (pick-any s1 s2 R
        (assume-let ((hyp1 (subset s1 s2)))
     	  (dlet ((goal (forall ?t (if (in ?t (sbdot s1 R)) (in ?t (sbdot s2 R)))))
	         (P (structure-cases goal
		      ((cons y unit) 
                         (assume-let ((hyp2 (in (tup [y]) (sbdot s1 R))))
                           (!pf (in (tup [y]) (sbdot s2 R)) [hyp2 hyp1 subset-axiom sbdot-axiom]))))))
            (!pf (subset (sbdot s1 R) (sbdot s2 R)) [P subset-axiom])))))


(define pf prove-from)

(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 (gp s) (match (and s s) ((and p p) p)))
                      
(define dot-th
  (pick-any s1 
    (pick-any s2
      (pick-any R
  	(assume-let ((hyp1 (subset s1 s2)))
  	  (dlet ((goal (if (in ?t (sbdot s1 R)) (in ?t (sbdot s2 R))))
		 (P (by-induction-on ?t goal
		      ((cons y unit) 
                         (assume-let ((hyp2 (in (tup [y]) (sbdot s1 R))))
   			   (dlet ((P1 (!fire sbdot-axiom [R s1 y])))
                             (pick-witness w P1 
                               (dlet ((inst-P1 (replace-var (qvar-of P1) w (body-of P1)))
        			      (P2 (!left-and inst-P1)) (P3 (!right-and inst-P1))	
   				      (P4 ((in (tup [w]) s2) BY (!subset-method s1 s2 (tup [w]))))
				      (P5 (!both P4 P3))
				      (P6 (!egen (exists ?x (replace-var w ?x P5)) w)))
                                 (!fire sbdot-axiom [R s2 y])))))))))
	    (!fire subset-axiom [(sbdot s1 R) (sbdot s2 R)])))))))
                   

;; Proves x = y from the assumption [x] in {[y]}

(define (eq-tup-parts premise)
  (dmatch premise 
    ((in (cons x unit) (singl (cons y unit)))
       (dlet ((P1 ((= (tup [x]) (tup [y])) BY (!fire singleton-axiom [(tup [x]) (tup [y])]))))
         (!left-and (!mp (!uspec* (!constructor-injectivity cons) [x unit y unit]) P1))))))

(define (eq-tup-parts1 premise)
  (dmatch premise 
    ((in (cons x unit) (singl (cons y unit)))
       (!pf (= x y) [premise (!constructor-injectivity cons) singleton-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 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])))))

; Another lemma: 
; ALL n, m | m in n.next* ==> m.next* subset n.next*

(define comp-monotonicity
  (forall* [?n ?m ?R]
    (if (in (tup [?m]) (sbdot (scalar ?n) (rtc ?R)))
	(subset (sbdot (scalar ?m) (rtc ?R))
		(sbdot (scalar ?n) (rtc ?R))))))

(define cm "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 ((P1 (!pf (exists ?ka (in (tup [n m]) (pow R ?ka))) [hyp scalar-lemma rtc-axiom]))
            (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*"))
                                    (dlet ((P3 (!pf (exists ?kb (in (tup [m y]) (pow R ?kb))) [hyp' scalar-lemma rtc-axiom]))
	   			           (P4 (!pf (exists ?k (in (tup [n y]) (pow R ?k))) [power-sum-lemma P1 P3])))
                                      (!pf "[y] in {[n]}.R*" [P4 rtc-axiom scalar-lemma])))))))
        (!pf "{[m]}.R* subset {[n]}.R*" [inc subset-axiom]))))


(pick-any n m R
  (assume-let ((hyp "[m] in {[n]}.R*"))
     (dlet ((P1 (!pf (exists ?ka (in (tup [n m]) (pow R ?ka))) [hyp scalar-lemma rtc-axiom]))
            (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' power-sum-lemma P1 rtc-axiom scalar-lemma]))))))
        (!pf "{[m]}.R* subset {[n]}.R*" [inc subset-axiom]))))


(pick-any n m R
  (assume-let ((hyp "[m] in {[n]}.R*"))
     (dlet ((P1 (!pf "SOME a | [n m] in R^a" [hyp scalar-lemma rtc-axiom]))
            (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*"))
                                    (dlet ((P3 (!pf "SOME b | [m y] in R^b" [hyp' scalar-lemma rtc-axiom]))
	   			           (P4 (!pf "SOME k | [n y] in R^k" [power-sum-lemma P1 P3])))
                                      (!pf "[y] in {[n]}.R*" [P4 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
 (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])))))))
          
; Prove: ALL n, R | {(n)} subset n.R*

(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")
;