(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "list.scm")
(libload "pos.scm")
(libload "int.scm")
(libload "rat.scm")
(set! COMMENT-FLAG #t)

(load "rea.scm")

;;;; Helpful commands
;; (use …), in particular. (use "Truth")
;; (assume …)

;; (assert B)
; Replaces Goal A by the two goals B -> A and B

;; (pp …)
; Display a theorem

;; (intro i …)
; Use the i-th introduction-axiom with arguments …

;; (assert B)
; Replaces Goal A by the two goals B -> A and B

;; (ng #t)
; This command tries to normalize all terms in the goal as
; much as possible [note that it will not always do what you want]

;; (simp …), (simp "<-" …)
; Simp accepts the name of a theorem or a variable(*),
; which expresses an equality (i.e., the corresponding formula should
; be of the form "… eqd …" or "… = …") and applies
; this equality to the goal.
; The theorem or variable can also express a formula of the Form A → B → … → x=y.
; In that case x=y is used on the goal and A,B,… are added as additional goals.
; Sometimes
; If the string "<-" is passed as the first argument, the replacement
; is done from right to left instead of left to right.
; Regarding (*): Simp also accepts formulas directly, i.e., one can write
; (simp (pf "n+m=m+n"));
; "n+m=m+n" will be added as an additional goal.
; Furthermore, simp can replace computably true formulas with truth.
; For example, if a:l<n is in the context, then
; (simp a) performs the replacement.

;; (simprat …), (simpreal …)
; Works just like (simp …) but with equalities on rationals/reals (written with ==/===)

;; (realproof) 
; Proof goal of form "Real (x+y)" from context using assumptions like "Real x", "Real y". 

;; (autoreal)
; Apply (realproof) multiple times.

;;; Helpful definitions
(display-alg "rea")
(display-alg "rat")
(display-alg "int")
(display-alg "pos")
(display-alg "nat")

(display-idpc "Real")
(display-idpc "Mon")
(display-idpc "Cauchy")

;;;; (a)
;;; Useful theorems
(pp "RatLePlusR")
(pp "RatPlusComm")
(pp "RatLeTrans")
(pp "Truth")
(pp "CauchyElim")
(pp "RealConstrToCauchy")

;;; Useful commands
;; assume
;; use
;; simp

;; ApproxSplitAux1
(set-goal "all as,M(Real(RealConstr as M) -> 
 all p,n,m(M p<=n -> M p<=m -> as n<=as m+(1#2**p)))")
;; TODO
(save "ApproxSplitAux1")

;; ApproxSplitAux2
(set-goal "all as,M(Real(RealConstr as M) ->
 all p,n,m(M p<=n -> M p<=m -> as n+ ~(1#2**p)<=as m))")
(assume "as" "M" "RasM" "p" "n" "m" "nBd" "mBd")
(use "RatLeTrans" (pt "as m+(1#2**p)+ ~(1#2**p)"))
(use "RatLeMonPlus")
(use "RatLePlusR")
(simp "RatPlusComm")
(use "RatLeTrans" (pt "abs(as n+ ~(as m))"))
(use "Truth")
(use "CauchyElim" (pt "M"))
(use "RealConstrToCauchy")
(use "RasM")
(use "nBd")
(use "mBd")
(use "Truth")
(simprat "RatEqvPlusMinusRev")
(use "Truth")
;; Proof finished.
;; (cp)
(save "ApproxSplitAux2")

;; ApproxSplitAux3
(set-goal "all a,b (a+b)*(1#2)+(b+ ~a)*(1#4)==b+ ~((b+ ~a)*(1#4))")
(assume "a" "b")
(use "RatEqvTimesCancelR" (pt "(4#1)"))
(use "Truth")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(ng #t)
(simprat "RatTimesPlusDistrLeft")
(ng #t)

(simp "<-" "RatTimesAssoc")
(simp "<-" "RatTimesAssoc")
(simp "<-" "RatTimesAssoc")
(simp "<-" "RatTimesAssoc")
(ng #t)

(assert "all a a*2==a+a")
(assume "c")
(simp (pf "2=(1#1)+1"))
(simprat "RatTimesPlusDistr")
(use "Truth")
(use "Truth")
;; Auxiliary assertion proved.
(assume "Aux1")

(assert "all a a*4==a*2+a*2")
(assume "c")
(simp (pf "4=(2#1)+2"))
(simprat "RatTimesPlusDistr")
(use "Truth")
(use "Truth")
;; Auxiliary assertion proved.
(assume "Aux2")

(simprat "Aux2")
(simprat "Aux1")
(simp "RatPlusComm")
(ng #t)
(simp "<-" (pf "0+ ~a+a+a+b*2+b= ~a+a+a+b*2+b"))
(simprat "RatEqvPlusMinusPlus")
(ng #t)
(simp (pf "b*2+b*2+ ~b+a=a+(b*2+b*2+ ~b)"))
(ng #t)
(simp (pf "a+b*2+b*2+ ~b=a+b*2+(b*2+ ~b)"))
(use "RatPlusCompat")
(use "Truth")
(simprat "Aux1")
(use "RatEqvSym")
(use "RatEqvPlusMinusRev")
(use "Truth")
(use "RatPlusComm")
(use "Truth")
;; Proof finished.
;; (cp)
(save "ApproxSplitAux3")

;;  ApproxSplitAux4
(set-goal "all a,b a+(b+ ~a)*(1#4)==(a+b)*(1#2)+ ~((b+ ~a)*(1#4))")
(assume "a" "b")
(assert "~((b+ ~a)*(1#4))=(a+ ~b)*(1#4)")
(simp "<-" "RatTimes4RewRule")
(ng #t)
(simp "RatPlusComm")
(use "Truth")
;; Auxiliary assertion proved.
(assume "Assertion")

(simp "Assertion")
(simp (pf "(b+ ~a)*(1#4)= ~ ~((b+ ~a)*(1#4))"))
(simp "Assertion")
(simp (pf "a+b=b+a"))
;; ?^13:a+ ~((a+ ~b)*(1#4))==(b+a)*(1#2)+(a+ ~b)*(1#4)
(simprat "ApproxSplitAux3")
(use "Truth")
(use "RatPlusComm")
(use "Truth")
;; Proof finished.
;; (cp)
(save "ApproxSplitAux4")

;;;; (b)

;;; Useful theorems
(pp "RealLeChar2")

(pp "RatLeTrans")
(pp "RatLeMonTimes")
(pp "RatLe7RewRule")
(pp "RatLeMonPlus")
(pp "RatTimesComm")

(pp "NatMaxUB2")
(pp "NatMaxUB2")
(pp "NatMaxUB1")

(pp "PosSSucc")
(pp "Truth")

(pp "ApproxSplitAux1")
(pp "ApproxSplitAux2")
(pp "ApproxSplitAux3")

;;; Useful commands
;; ng
;; assume
;; use
;; simp
;; simprat
;; intro

;; ApproxSplitPos
(set-goal "all x,y,z,p(Real x -> Real y -> Real z -> RealPos(y+ ~x)p ->
                       z<<=y oru x<<=z)")
(assume "x" "y" "z" "p" "Rx" "Ry" "Rz")
(cases (pt "x"))
(assume "as" "M" "xDef")
(cases (pt "y"))
(assume "bs" "N" "yDef")
(cases (pt "z"))
(assume "cs" "K" "zDef")
(ng #t)
(def "n" "N(PosS(PosS p))max M(PosS(PosS p))")
(simp "<-" "nDef")
(assume "x<y")
(def "m" "n max K(PosS(PosS p))")
(cases (pt "cs m<=(1#2)*(as n+(bs n))"))

;; TODO

;; Left case completed
;; 27
(assume "Right")
(intro 1)
;; ?^87:RealConstr as M<<=RealConstr cs K
(use "RealLeChar2")
(simp "<-" "xDef")
(use "Rx")
(simp "<-" "zDef")
(use "Rz")
;; ?^90:all p exnc n all n0(n<=n0 -> as n0<=cs n0+(1#2**p))
(assume "q")
(intro 0 (pt "m"))
(assume "l" "m<=l")
(use "RatLeTrans" (pt "cs l"))
;; 96,97
;; ?^96:as l<=cs l
(use "RatLeTrans" (pt "as n+(1#2**(PosS(PosS p)))"))
;; 98,99
;; ?^98:as l<=as n+(1#2**PosS(PosS p))
(use "ApproxSplitAux1" (pt "M"))
(simp "<-" "xDef")
(use "Rx")
(use "NatLeTrans" (pt "m"))
(simp "mDef")
(use "NatLeTrans" (pt "n"))
(simp "nDef")
(use "NatMaxUB2")
(use "NatMaxUB1")
(use "m<=l")
(simp "nDef")
(use "NatMaxUB2")
;; ?^99:as n+(1#2**PosS(PosS p))<=cs l
(use "RatLeTrans" (pt "as n+(bs n+ ~(as n))*(1#4)"))
;; 111,112
;; ?^111:as n+(1#2**PosS(PosS p))<=as n+(bs n+ ~(as n))*(1#4)
(use "RatLeMonPlus")
(use "Truth")
(use "RatLeTrans" (pt "(1#2**p)*(1#4)"))
(ng #t)
;; ?^117:SZero(SZero(2**p))<=2**PosS(PosS p)
(simp "PosSSucc")
(simp "PosSSucc")
(use "Truth")
;; ?^116:(1#2**p)*(1#4)<=(bs n+ ~(as n))*(1#4)
(use "RatLeMonTimes")
(use "Truth")
(use "x<y")
;; ?^112:as n+(bs n+ ~(as n))*(1#4)<=cs l
(simprat "ApproxSplitAux4")
;; ?^122:(as n+bs n)*(1#2)+ ~((bs n+ ~(as n))*(1#4))<=cs l
(use "RatLeTrans" (pt "cs m+ ~(1#2**PosS(PosS p))"))
;; ?^123:(as n+bs n)*(1#2)+ ~((bs n+ ~(as n))*(1#4))<=cs m+ ~(1#2**PosS(PosS p))
(use "RatLeMonPlus")
;; 125,126
;; ?^125:(as n+bs n)*(1#2)<=cs m
(use "RatLtToLe")
(use "RatNotLeToLt")
(simp "RatTimesComm")
(use "Right")
;; ?^126:~((bs n+ ~(as n))*(1#4))<= ~(1#2**PosS(PosS p))
(simp "RatLe7RewRule")
;; ?^130:(1#2**PosS(PosS p))<=(bs n+ ~(as n))*(1#4) ;same goal as 68
(use "RatLeTrans" (pt "(1#2**p)*(1#4)"))
;; 131,132
;; ?^131:(1#2**PosS(PosS p))<=(1#2**p)*(1#4)
(simp "PosSSucc")
(simp "PosSSucc")
(use "Truth")
;; ?^132:(1#2**p)*(1#4)<=(bs n+ ~(as n))*(1#4)
(use "RatLeMonTimes")
(use "Truth")
(use "x<y")
;; ?^124:cs m+ ~(1#2**PosS(PosS p))<=cs l
(use "ApproxSplitAux2" (pt "K"))
(simp "<-" "zDef")
(use "Rz")
(simp "mDef")
(use "NatMaxUB2")
(use "NatLeTrans" (pt "m"))
(simp "mDef")
(use "NatMaxUB2")
(use "m<=l")
(use "Truth")
;; Proof finished.
;; (cp)
(save "ApproxSplitPos")