#|
(load "~/git/minlog/init.scm")
(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "list.scm")
(libload "pos.scm")
(libload "int.scm")
(libload "rat.scm")
;; (set! COMMENT-FLAG #t)
|#

(if (not (assoc "nat" ALGEBRAS))
    (myerror "First execute (libload \"nat.scm\")")
    (if (not (assoc "pos" ALGEBRAS))
	(myerror "First execute (libload \"pos.scm\")")
	(if (not (assoc "int" ALGEBRAS))
	    (myerror "First execute (libload \"int.scm\")")
	    (if (not (assoc "rat" ALGEBRAS))
		(myerror "First execute (libload \"rat.scm\")")))))

(display "loading rea.scm ...") (newline)

;; 1.  Real numbers
;; ================

;; We introduce the reals.  A real is a pair of a Cauchy sequence of
;; rationals and a modulus.  We view real as a data type (i.e., no
;; properties), and within this data type inductively define the
;; predicate Real x, meaning that x is a (proper) real.

(add-var-name "as" "bs" "cs" "ds" (py "nat=>rat"))
(add-var-name "M" "N" "K" (py "pos=>nat"))

(add-alg "rea" (list "RealConstr" "(nat=>rat)=>(pos=>nat)=>rea"))
(add-var-name "x" "y" "z" (py "rea"))

(add-eqp "rea")

;; (pp "EqPReaRealConstr")

;; allnc as^,as^0(
;;  allnc n^,n^0(EqPNat n^ n^0 -> EqPRat(as^ n^)(as^0 n^0)) -> 
;;  allnc M^,M^0(
;;   allnc p^,p^0(EqPPos p^ p^0 -> EqPNat(M^ p^)(M^0 p^0)) -> 
;;   EqPRea(RealConstr as^ M^)(RealConstr as^0 M^0)))

(add-eqpnc "rea")

;; We prefer to work with a simple direct definition of TotalRea and
;; then show its equivalence to the general definition x eqp x.

(add-ids
 (list (list "TotalRea" (make-arity (py "rea")) "rea"))
 '("allnc as^(allnc n^(TotalNat n^ -> TotalRat(as^ n^)) ->
    allnc M^(allnc p^(TotalPos p^ -> TotalNat(M^ p^)) ->
    TotalRea(RealConstr as^ M^)))"
   "TotalReaRealConstr"))

(add-ids
 (list (list "TotalReaNc" (make-arity (py "rea"))))
 '("allnc as^(allnc n^(TotalNatNc n^ -> TotalRatNc(as^ n^)) ->
    allnc M^(allnc p^(TotalPosNc p^ -> TotalNatNc(M^ p^)) ->
    TotalReaNc(RealConstr as^ M^)))"
   "TotalReaNcRealConstr"))

;; EqPTotalNatToRatLeft
(set-goal "allnc as^1,as^2(
     allnc n^1,n^2(EqPNat n^1 n^2 -> EqPRat(as^1 n^1)(as^2 n^2)) -> 
     allnc n^(TotalNat n^ -> TotalRat(as^1 n^)))")
(assume "as^1" "as^2" "EqPas1as2" "n^" "Tn")
(use "EqPRatToTotalLeft" (pt "as^2 n^"))
(use "EqPas1as2")
(use "EqPNatRefl")
(use "Tn")
;; Proof finished.
;; (cp)
(save "EqPTotalNatToRatLeft")

;; EqPTotalNatToRatRight
(set-goal "allnc as^1,as^2(
     allnc n^1,n^2(EqPNat n^1 n^2 -> EqPRat(as^1 n^1)(as^2 n^2)) -> 
     allnc n^(TotalNat n^ -> TotalRat(as^2 n^)))")
(assume "as^1" "as^2" "EqPas1as2" "n^" "Tn")
(use "EqPRatToTotalRight" (pt "as^1 n^"))
(use "EqPas1as2")
(use "EqPNatRefl")
(use "Tn")
;; Proof finished.
;; (cp)
(save "EqPTotalNatToRatRight")

;; EqPTotalPosToNatLeft
(set-goal "allnc M^1,M^2(
     allnc p^,p^0(EqPPos p^ p^0 -> EqPNat(M^1 p^)(M^2 p^0)) -> 
     allnc p^(TotalPos p^ -> TotalNat(M^1 p^)))")
(assume "M^1" "M^2" "EqPM1M2" "p^" "Tp")
(use "EqPNatToTotalLeft" (pt "M^2 p^"))
(use "EqPM1M2")
(use "EqPPosRefl")
(use "Tp")
;; Proof finished.
;; (cp)
(save "EqPTotalPosToNatLeft")

;; EqPTotalPosToNatRight
(set-goal "allnc M^1,M^2(
     allnc p^,p^0(EqPPos p^ p^0 -> EqPNat(M^1 p^)(M^2 p^0)) -> 
     allnc p^(TotalPos p^ -> TotalNat(M^2 p^)))")
(assume "M^1" "M^2" "EqPM1M2" "p^" "Tp")
(use "EqPNatToTotalRight" (pt "M^1 p^"))
(use "EqPM1M2")
(use "EqPPosRefl")
(use "Tp")
;; Proof finished.
;; (cp)
(save "EqPTotalPosToNatRight")

;; EqPReaToTotalLeft
(set-goal "allnc x^,y^(EqPRea x^ y^ -> TotalRea x^)")
(assume "x^" "y^" "EqPxy")
(elim "EqPxy")
(assume "as^1" "as^2" "EqPas1as2" "M^1" "M^2" "EqPM1M2")
(use "TotalReaRealConstr")
(use "EqPTotalNatToRatLeft" (pt "as^2"))
(use "EqPas1as2")
(use "EqPTotalPosToNatLeft" (pt "M^2"))
(use "EqPM1M2")
;; Proof finished.
;; (cp)
(save "EqPReaToTotalLeft")

;; EqPReaToTotalRight
(set-goal "allnc x^,y^(EqPRea x^ y^ -> TotalRea y^)")
(assume "x^" "y^" "EqPxy")
(elim "EqPxy")
(assume "as^1" "as^2" "EqPas1as2" "M^1" "M^2" "EqPM1M2")
(use "TotalReaRealConstr")
(use "EqPTotalNatToRatRight" (pt "as^1"))
(use "EqPas1as2")
(use "EqPTotalPosToNatRight" (pt "M^1"))
(use "EqPM1M2")
;; Proof finished.
;; (cp)
(save "EqPReaToTotalRight")

;; EqPReaRefl
(set-goal "allnc x^(TotalRea x^ -> EqPRea x^ x^)")
(assume "x^" "Tx")
(elim "Tx")
(assume "as^" "Tas" "M^" "TM")
(use "EqPReaRealConstr")
;; 5,6
(assume "n^1" "n^2" "EqPn1n2")
(simp "<-" (pf "n^1 eqd n^2"))
;; 8,9
(use "EqPRatRefl")
(use "Tas")
(use "EqPNatToTotalLeft" (pt "n^2"))
(use "EqPn1n2")
;; 9
(use "EqPNatNcToEqD")
(use "EqPn1n2")
;; 6
(assume "p^1" "p^2" "EqPp1p2")
(simp "<-" (pf "p^1 eqd p^2"))
;; 15,16
(use "EqPNatRefl")
(use "TM")
(use "EqPPosToTotalLeft" (pt "p^2"))
(use "EqPp1p2")
;; 16
(use "EqPPosToEqD")
(use "EqPp1p2")
;; Proof finished.
;; (cp)
(save "EqPReaRefl")

;; End of proof of the equivalence of the simple direct definition of
;; TotalRea with the general definition x eqp x.

;; ReaTotalVar
(set-goal "all x TotalRea x")
(cases)
(assume "as" "M")
(use "TotalReaRealConstr")
(use "AllTotalElim")
(assume "n")
(use "RatTotalVar")
(use "AllTotalElim")
(assume "p")
(use "NatTotalVar")
;; Proof finished.
;; (cp)
(save "ReaTotalVar")

;; To conveniently access the two fields of a real, we provide seq and
;; mod as informative names to be used (postfix) in display strings.

(add-program-constant "RealSeq" (py "rea=>nat=>rat") t-deg-zero 'const 1)

(add-token
 "seq"
 'postfix-op
 (lambda (x)
   (mk-term-in-app-form
    (make-term-in-const-form (pconst-name-to-pconst "RealSeq"))
    x)))

(add-display
 (py "nat=>rat")
 (lambda (x)
   (let ((op (term-in-app-form-to-final-op x))
	 (args (term-in-app-form-to-args x)))
     (if (and (term-in-const-form? op)
	      (string=? "RealSeq"
			(const-to-name (term-in-const-form-to-const op)))
	      (= 1 (length args)))
	 (let ((arg (car args)))
	   (list
	    'postfix-op "seq"
	    (term-to-token-tree arg)))
	 #f))))

(add-computation-rules
 "(RealConstr as M)seq" "as")

(set-totality-goal "RealSeq")
(fold-alltotal)
(cases)
(assume "as" "M")
(fold-alltotal)
(assume "n")
(use "RatTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

(add-program-constant "RealMod" (py "rea=>pos=>nat") t-deg-zero 'const 1)

(add-token
 "mod"
 'postfix-op
 (lambda (x)
   (mk-term-in-app-form
    (make-term-in-const-form (pconst-name-to-pconst "RealMod"))
    x)))

(add-display
 (py "pos=>nat")
 (lambda (x)
   (let ((op (term-in-app-form-to-final-op x))
	 (args (term-in-app-form-to-args x)))
     (if (and (term-in-const-form? op)
	      (string=? "RealMod"
			(const-to-name (term-in-const-form-to-const op)))
	      (= 1 (length args)))
	 (let ((arg (car args)))
	   (list
	    'postfix-op "mod"
	    (term-to-token-tree arg)))
	 #f))))

(add-computation-rules
 "(RealConstr as M)mod" "M")

;; RealModTotal
(set-totality-goal "RealMod")
(fold-alltotal)
(cases)
(assume "as" "M")
(fold-alltotal)
(assume "p")
(use "NatTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; (pp (pt "x seq n"))
;; (pp (pt "x mod p"))

;; 2. Parsing and display for arithmetical operations
;; ==================================================

(add-item-to-algebra-edge-to-embed-term-alist
 "rat" "rea"
 (let ((var (make-var (make-alg "rat") -1 t-deg-one ""))
       (n (make-var (make-alg "nat") -1 t-deg-one ""))
       (l (make-var (make-alg "nat") -1 t-deg-one "")))
   (make-term-in-abst-form
    var (mk-term-in-app-form
         (make-term-in-const-form
          (constr-name-to-constr "RealConstr"))
         (make-term-in-abst-form ;constant Cauchy sequence
          n (make-term-in-var-form var))
         (make-term-in-abst-form ;Zero modulus
          l (make-term-in-const-form
             (constr-name-to-constr "Zero")))))))

;; (alg-le? (make-alg "rat") (make-alg "rea"))

(add-program-constant "RealPlus" (py "rea=>rea=>rea"))
(add-program-constant "RealUMinus" (py "rea=>rea"))
(add-program-constant "RealMinus" (py "rea=>rea=>rea"))
(add-program-constant "RealTimes" (py "rea=>rea=>rea"))
(add-program-constant "RealUDiv" (py "rea=>pos=>rea"))
(add-program-constant "RealDiv" (py "rea=>rea=>rea"))
(add-program-constant "RealAbs" (py "rea=>rea"))
(add-program-constant "RealExp" (py "rea=>nat=>rea"))
(add-program-constant "RealMax" (py "rea=>rea=>rea"))
(add-program-constant "RealMin" (py "rea=>rea=>rea"))

(add-token-and-type-to-name "+" (py "rea") "RealPlus")
(add-token-and-type-to-name "~" (py "rea") "RealUMinus")
(add-token-and-type-to-name "-" (py "rea") "RealMinus")
(add-token-and-type-to-name "*" (py "rea") "RealTimes")
(add-token-and-type-to-name "/" (py "rea") "RealDiv")
(add-token-and-type-to-name "abs" (py "rea") "RealAbs")

(add-token-and-types-to-name "**" (list (py "rea") (py "pos")) "RealExp")
(add-token-and-types-to-name "**" (list (py "rea") (py "nat")) "RealExp")

(add-token-and-type-to-name "max" (py "rea") "RealMax")
(add-token-and-type-to-name "min" (py "rea") "RealMin")

(add-display (py "rea") (make-display-creator "RealPlus" "+" 'add-op))
(add-display (py "rea") (make-display-creator1 "RealUMinus" "~" 'prefix-op))
(add-display (py "rea") (make-display-creator "RealMinus" "-" 'add-op))
(add-display (py "rea") (make-display-creator "RealTimes" "*" 'mul-op))
(add-display (py "rea") (make-display-creator "RealDiv" "/" 'mul-op))
(add-display (py "rea") (make-display-creator1 "RealAbs" "abs" 'prefix-op))
(add-display (py "rea") (make-display-creator "RealExp" "**" 'exp-op))
(add-display (py "rea") (make-display-creator "RealMax" "max" 'mul-op))
(add-display (py "rea") (make-display-creator "RealMin" "min" 'mul-op))

(add-display
 (py "rea")
 (lambda (x)
   (let ((op (term-in-app-form-to-final-op x))
	 (args (term-in-app-form-to-args x)))
     (if (and (term-in-const-form? op)
	      (string=? "RealConstr"
			(const-to-name (term-in-const-form-to-const op)))
	      (= 2 (length args))
	      (term-in-abst-form? (car args))
	      (not (member (term-in-abst-form-to-var (car args))
			   (term-to-free
			    (term-in-abst-form-to-kernel (car args))))))
	 (term-to-token-tree (term-to-original
			      (term-in-abst-form-to-kernel (car args))))
	 #f))))

;; (pp (pt "(IntN p#q)+RealConstr([n]1)([p]7)"))
;; (IntN p#q)+1

;; 3.  Arithmetic
;; ==============

;; RealPos is a decidable property and hence can be considered as a
;; program constant.

(add-program-constant "RealPos" (py "rea=>pos=>boole"))

(add-display
 (make-alg "boole")
 (lambda (x)
   (let ((op (term-in-app-form-to-final-op x))
	 (args (term-in-app-form-to-args x)))
     (if (and (term-in-const-form? op)
	      (string=? "RealPos"
			(const-to-name (term-in-const-form-to-const op)))
	      (= 2 (length args)))
	 (let ((arg1 (car args))
	       (arg2 (cadr args)))
	   (list
	    'appterm ""
	    (list
	     'appterm ""
	     (list 'const "RealPos")
	     (term-to-token-tree (term-to-original arg1)))
	    (term-to-token-tree (term-to-original arg2))))
	 #f))))

(add-computation-rules "RealPos(RealConstr as M)p" "(1#2**p)<=as(M(PosS p))")

;; EqPReaAux reduces a goal allnc x^,y^(EqPRea x^ y^ -> (Pvar rea rea)x^ y^)
;; to another one with x^, y^ in RealConstr form.  This can be done since
;; rea has one constructor only.

;; EqPReaAux
(set-goal "allnc as^,M^,bs^,N^(
 EqPRea(RealConstr as^ M^)(RealConstr bs^ N^) ->
 (Pvar rea rea)(RealConstr as^ M^)(RealConstr bs^ N^)) -> 
 allnc x^,y^(EqPRea x^ y^ -> (Pvar rea rea)x^ y^)")
(assume "Hyp" "x^" "y^" "EqPxy")
(elim "EqPxy")
(assume "as^1" "as^2" "EqPas1as2" "M^1" "M^2" "EqPM1M2")
(use "Hyp")
(use "EqPReaRealConstr")
(use "EqPas1as2")
(use "EqPM1M2")
;; Proof finished.
;; (cp)
(save "EqPReaAux")

;; 2020-07-13.  Changed because of pure unfolding of the premise.
;; EqPReaElimLeft
(set-goal "allnc x^,y^(EqP x^ y^ -> EqP(x^ seq)(y^ seq))")
(assume "x^" "y^" "EqPxy")
(elim "EqPxy")
(assume "as^1" "as^2" "EqPas1as2" "M^1" "M^2" "EqPM1M2")
(ng #t)
(assume "n^1" "n^2" "n1=n2")
(use "EqPas1as2")
(use "n1=n2")
;; Proof finished.
;; (cp)
(save "EqPReaElimLeft")

;; 2020-07-13.  Changed because of pure unfolding of the premise.
;; EqPReaElimRight
(set-goal "allnc x^,y^(EqP x^ y^ -> EqP(x^ mod)(y^ mod))")
(assume "x^" "y^" "EqPxy")
(elim "EqPxy")
(assume "as^1" "as^2" "EqPas1as2" "M^1" "M^2" "EqPM1M2")
(ng #t)
(assume "p^1"  "p^2" "p1=p2")
(use "EqPM1M2")
(use "p1=p2")
;; Proof finished.
;; (cp)
(save "EqPReaElimRight")

;; EqPReaElimLeftRealConstr
(set-goal "allnc as^,M^,bs^,N^(
 EqPRea(RealConstr as^ M^)(RealConstr bs^ N^) ->
 allnc n^,m^(EqPNat n^ m^ -> EqPRat(as^ n^)(bs^ m^)))")
(assume "as^" "M^" "bs^" "N^" "EqPxy")
;; (use "AllEqPNatElim")
(use-with "EqPReaElimLeft"
	  (pt "(RealConstr as^ M^)") (pt "(RealConstr bs^ N^)")
	  "EqPxy")
;; Proof finished.
;; (cp)
(save "EqPReaElimLeftRealConstr")

;; EqPReaElimRightRealConstr
(set-goal "allnc as^,M^,bs^,N^(
 EqPRea(RealConstr as^ M^)(RealConstr bs^ N^) ->
 allnc p^,q^(EqPPos p^ q^ -> EqPNat(M^ p^)(N^ q^)))")
(assume "as^" "M^" "bs^" "N^" "EqPxy")
;; (use "AllEqPPosElim")
(use-with "EqPReaElimRight"
	  (pt "(RealConstr as^ M^)") (pt "(RealConstr bs^ N^)")
	  "EqPxy")
;; Proof finished.
;; (cp)
(save "EqPReaElimRightRealConstr")

;; RealPosTotal
(set-totality-goal "RealPos")
(fold-alltotal)
(cases)
(assume "as" "M")
(fold-alltotal)
(assume "p")
(use "BooleTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; RealLt is a decidable property and hence can be considered as a
;; program constant.

(add-program-constant "RealLt" (py "rea=>rea=>pos=>boole"))

(add-display
 (make-alg "boole")
 (lambda (x)
   (let ((op (term-in-app-form-to-final-op x))
	 (args (term-in-app-form-to-args x)))
     (if (and (term-in-const-form? op)
	      (string=? "RealLt"
			(const-to-name (term-in-const-form-to-const op)))
	      (= 3 (length args)))
	 (let ((arg1 (car args))
	       (arg2 (cadr args))
	       (arg3 (caddr args)))
	   (list
	    'appterm ""
	    (list
	     'appterm ""
	     (list
	      'appterm ""
	      (list 'const "RealLt")
	      (term-to-token-tree (term-to-original arg1)))
	     (term-to-token-tree (term-to-original arg2)))
	    (term-to-token-tree (term-to-original arg3))))
	 #f))))

(add-computation-rules
 "RealLt(RealConstr as M)(RealConstr bs N)p"
 "RealPos(RealConstr bs N+ ~(RealConstr as M))p")

;; Rules for RealUMinus

(add-computation-rules
 "~(RealConstr as M)" "RealConstr([n]~(as n))M")

;; RealUMinusTotal
(set-totality-goal "RealUMinus")
(fold-alltotal)
(cases)
(assume "as" "M")
(use "ReaTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; Rules for RealPlus

(add-computation-rules
 "RealConstr as M+RealConstr bs N"
 "RealConstr([n]as n+bs n)([p]M(PosS p)max N(PosS p))")

;; RealPlusTotal
(set-totality-goal "RealPlus")
(fold-alltotal)
(cases)
(assume "as" "M")
(fold-alltotal)
(cases)
(assume "bs" "N")
(use "ReaTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; RealLtTotal

(set-totality-goal "RealLt")
(fold-alltotal)
(cases)
(assume "as" "M")
(fold-alltotal)
(cases)
(assume "bs" "N")
(fold-alltotal)
(assume "p")
(ng #t)
(use "BooleTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; Rules for RealMinus

(add-computation-rules
 "x-y" "x+ ~y")

(set-totality-goal "RealMinus")
(fold-alltotal)
(cases)
(assume "as" "M")
(fold-alltotal)
(cases)
(assume "bs" "N")
(use "ReaTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; Rules for RealUDiv
(add-computation-rules
 "RealUDiv(RealConstr as M)q" "RealConstr([n]RatUDiv(as n))([p]M(2*PosS q+p))")

;; RealUDivTotal
(set-totality-goal "RealUDiv")
(fold-alltotal)
(cases)
(assume "as" "M")
(fold-alltotal)
(assume "p")
(use "ReaTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; Rules for RealAbs

(add-computation-rules
 "abs(RealConstr as M)" "RealConstr([n]abs(as n))M")

;; RealAbsTotal
(set-totality-goal "RealAbs")
(fold-alltotal)
(cases)
(assume "as" "M")
(use "ReaTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; Rules for RealTimes are postponed.
;; They require the Archimedian property, in the form of a pconst
;; RealBd.  We will define an auxiliary function ListNatMax, then
;; RealBd and finally the computation rule for RealTimes.  Its
;; properties require the predicate Cauchy.

;; Rules for RealMax : rea=>rea=>rea

(add-computation-rules
 "RealConstr as M max RealConstr bs N"
 "RealConstr([n]as n max bs n)([p]M p max N p)")

;; RealMaxTotal
(set-totality-goal "RealMax")
(fold-alltotal)
(cases)
(assume "as1" "M1")
(fold-alltotal)
(cases)
(assume "as2" "M2")
(use "ReaTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; Rules for RealMin : rea=>rea=>rea

(add-computation-rules
 "RealConstr as M min RealConstr bs N"
 "RealConstr([n]as n min bs n)([p]M p max N p)")

;; RealMinTotal
(set-totality-goal "RealMin")
(fold-alltotal)
(cases)
(assume "as1" "M1")
(fold-alltotal)
(cases)
(assume "as2" "M2")
(use "ReaTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; 4.  Inductive predicates Cauchy, Mon, Real
;; ==========================================

;; To work with reals, we use a predicate constant Cauchy which takes
;; two arguments, a sequence of rationals and a modulus.

;; We introduce Cauchy as an inductively defined predicate (which may
;; in this case also be called a record).

(add-ids
 (list (list "Cauchy" (make-arity (py "nat=>rat") (py "pos=>nat"))))
 '("allnc as,M(
    allnc p,n,m(M p<=n -> M p<=m -> abs(as n+ ~(as m))<=(1#2**p)) ->
    Cauchy as M)" "CauchyIntro"))

;; Similarly, we introduce a predicate constant Mon, taking a sequence
;; of positive numbers as argument, to express monotonicity.

(add-ids (list (list "Mon" (make-arity (py "pos=>nat"))))
	 '("allnc M(allnc p,q(p<=q -> M p<=M q) -> Mon M)" "MonIntro"))

;; CauchyElim
(set-goal
 "allnc as,M(Cauchy as M ->
             allnc p,n,m(M p<=n -> M p<=m -> abs(as n+ ~(as m))<=(1#2**p)))")
(assume "as" "M")
(elim)
(search)
;; Proof finished.
;; (cp)
(save "CauchyElim")

;; MonElim
(set-goal "allnc M(Mon M -> allnc p,q(p<=q -> M p<=M q))")
(assume "M")
(elim)
(search)
;; Proof finished.
;; (cp)
(save "MonElim")

;; EfCauchy
(set-goal "F -> allnc as,M Cauchy as M")
(assume "Absurd" "as" "M")
(intro 0)
(strip)
(use "EfAtom")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfCauchy")

;; EfMon
(set-goal "F -> allnc M Mon M")
(assume "Absurd" "M")
(intro 0)
(strip)
(use "EfAtom")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfMon")

;; CauchyChar1
(set-goal "all as,M(Cauchy as M ->
 all p,n,m(M p<=n -> M p<=m -> as n<=as m+(1#2**p)))")
(assume "as" "M" "CasM" "p" "n" "m" "nBd" "mBd")
(use "RatLePlusR")
(simp "RatPlusComm")
(use "RatLeTrans" (pt "abs(as n+ ~(as m))"))
(use "Truth")
(use "CauchyElim" (pt "M"))
(use "CasM")
(use "nBd")
(use "mBd")
;; Proof finished.
;; (cp)
(save "CauchyChar1")

;; CauchyChar2
(set-goal "all as,M(all p,n,m(M p<=n -> M p<=m -> as n<=as m+(1#2**p)) ->
 Cauchy as M)")
(assume "as" "M" "AllHyp")
(use "CauchyIntro")
(assume "p" "n" "m" "nBd" "mBd")
(use "RatLeAbs")
;; 5,6
(simp "RatPlusComm")
(use "RatLePlusRInv")
(use "AllHyp")
(use "nBd")
(use "mBd")
;; 6
(ng #t)
(use "RatLePlusRInv")
(use "AllHyp")
(use "mBd")
(use "nBd")
;; Proof finished.
;; (cp)
(save "CauchyChar2")

;; We introduce Real as an inductively defined predicate (which in this
;; case may also be called a record).  Then we can prove theorems:

;; RealIntro: allnc x(Cauchy(x seq)(x mod) -> Mon(x mod) -> Real x)
;; RealToCauchySeq: allnc as,M(Real(RealConstr as M) -> Cauchy as M)
;; RealToMonMod: allnc as,M(Real(RealConstr as M) -> Mon M)

;; Alternative formulation (worse, since usability is restricted)
;; RealIntro: allnc as,M(Cauchy as M -> Mon M -> Real RealConstr as M) 
;; RealToCauchySeq: allnc x(Real x -> Cauchy(x seq)(x mod))
;; RealToMonMod: allnc x(Real x -> Mon(x mod))

(add-ids
 (list (list "Real" (make-arity (py "rea"))))
 '("all x(Cauchy(x seq)(x mod) -> Mon(x mod) -> Real x)" "RealIntro"))

;; RealToCauchy
(set-goal "all x(Real x -> Cauchy(x seq)(x mod))")
(assume "x")
(elim)
(auto)
;; Proof finished.
;; (cp)
(save "RealToCauchy")

;; RealToMon
(set-goal "all x(Real x -> Mon(x mod))")
(assume "x")
(elim)
(auto)
;; Proof finished.
;; (cp)
(save "RealToMon")

;; The following variants will be more useful, because their heads will
;; be more often of the form of a given goal.

;; RealConstrToCauchy
(set-goal "all as,M(Real(RealConstr as M) -> Cauchy as M)")
(strip)
(use-with "RealToCauchy" (pt "RealConstr as M") 1)
;; Proof finished.
;; (cp)
(save "RealConstrToCauchy")

;; RealConstrToMon
(set-goal "all as,M(Real(RealConstr as M) -> Mon M)")
(strip)
(use-with "RealToMon" (pt "RealConstr as M") 1)
;; Proof finished.
;; (cp)
(save "RealConstrToMon")

;; EfReal
(set-goal "F -> all x Real x")
(assume "Absurd")
(cases)
(assume "as" "M")
(intro 0)
(ng)
(use "EfCauchy")
(use "Absurd")
(ng)
(use "EfMon")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "EfReal")

;; RealRat
(set-goal "allnc a Real a")
(assume "a")
(use "RealIntro")
(use "CauchyIntro")
(assume "p" "n" "m" "Useless1" "Useless2")
(ng #t)
(simprat (pf "a+ ~a==0"))
(use "Truth")
(use "Truth")
(use "MonIntro")
(assume "p" "q" "p<=q")
(ng)
(use "Truth")
;; Proof finished.
;; (cp)
(save "RealRat")

;; Computation rules for RealTimes.  

;; We first define an auxiliary function ListNatMax, then RealBd and
;; finally the computation rule for RealTimes.

(add-var-name "nl" "ml" (py "list nat"))
(add-program-constant "ListNatMax" (py "list nat=>nat") t-deg-zero)

(add-computation-rules
 "ListNatMax(Nil nat)" "Zero"
 "ListNatMax(n:)" "n"
 "ListNatMax(n::m::nl)" "n max ListNatMax(m::nl)")

;; (pp (nt (pt "ListNatMax(2::6::1::3::4:)")))
;; Succ(Succ(Succ(Succ(Succ(Succ Zero)))))

(set-totality-goal "ListNatMax")
(fold-alltotal)
(ind)
;; 3,4
(use "NatTotalVar")
;; 4
(assume "n")
(cases)
;; 6,7
(assume "Useless")
(use "NatTotalVar")
;; 7
(assume "m" "nl" "IH")
(ng #t)
(use "NatMaxTotal")
(use "NatTotalVar")
(use "IH")
;; Proof finished.
;; (cp)
(save-totality)

;; ListNatMaxEqP
(set-goal "allnc nl^1,nl^2(EqP nl^1 nl^2 ->
 EqP(ListNatMax nl^1)(ListNatMax nl^2))")
(assume "nl^1" "nl^2" "EqPnl1nl2")
(elim "EqPnl1nl2")
;; 3,4
(ng #t)
(use "EqPNatZero")
;; 4
(assume "n^1" "n^2" "EqPn1n2" "nl^3" "nl^4" "EqPnl3nl4")
(elim "EqPnl3nl4")
;; 7,8
(assume "Useless")
(ng #t)
(use "EqPn1n2")
;; 8
(assume "n^3" "n^4" "EqPn3n4" "nl^5" "nl^6" "EqPnl5nl6" "Hyp1" "Hyp2")
(ng #t)
(use "NatMaxEqP")
(use "EqPn1n2")
(use "Hyp2")
;; Proof finished.
;; (cp)
(save "ListNatMaxEqP")

;; (display-pconst "ListNatMax")

;; ListNatMaxUB
(set-goal "all ml,n(n<Lh ml -> ListNatProj n ml<=ListNatMax ml)")
(ind)
;; 2,3
(ng)
(assume "n" "Absurd")
(use "EfAtom")
(use "Absurd")
;; 3
(assume "m")
(cases)
;; 8,9
(assume "Useless")
(cases)
;; 11,12
(ng)
(strip)
(use "Truth")
;; 12
(ng)
(assume "n" "Absurd")
(use "EfAtom")
(use "Absurd")
;; 9
(assume "m1" "ml" "IH")
(cases)
;; 19,20
(assume "Useless")
(ng)
(use "NatMaxUB1")
;; 20
(ng)
(assume "n1" "n1Prop")
(use "NatLeTrans" (pt "ListNatMax(m1::ml)"))
(use "IH")
(use "n1Prop")
(use "NatMaxUB2")
;; Proof finished.
;; (cp)
(save "ListNatMaxUB")

;; ListNatMaxFBar
(set-goal "all nat=>nat,n,l(n<l -> (nat=>nat)n<=ListNatMax((nat=>nat)fbar l))")
(assume "nat=>nat" "n" "l" "n<l")
(inst-with-to "ListNatProjFBar" (pt "l") (pt "n") (pt "nat=>nat") "n<l" "Inst")
(simp "<-" "Inst")
(drop "Inst")
(use "ListNatMaxUB")
(use "n<l")
;; Proof finished.
;; (cp)
(save "ListNatMaxFBar")

;; We need some more auxiliary concepts.

(animate "RatLeBound")
(animate "RatLeAbsBound")
;; (display-pconst "cRatLeAbsBound")

;; cRatLeAbsBoundTotal
(set-totality-goal "cRatLeAbsBound")
(fold-alltotal)
(assume "a")
(ng)
(use "RatIfTotal")
(use "RatTotalVar")
(assume "k^" "p^" "Tk" "Tp")
(use "IntIfTotal")
(use "Tk")
(use "NatTotalVar")
;; 10
(use "AllTotalElim")
(assume "p1")
(use "NatMinusTotal")
(use "NatTotalVar")
(use "PosLogTotal")
(use "Tp")
;; 11
(use "AllTotalElim")
(assume "p1")
(use "NatMinusTotal")
(use "NatTotalVar")
(use "PosLogTotal")
(use "Tp")
;; Proof finished.
;; (cp)
(save-totality)

(deanimate "RatLeBound")
(deanimate "RatLeAbsBound")

(set-totality-goal "cRatLeBound")
(fold-alltotal)
(assume "p")
(fold-alltotal)
(assume "q")
(use "NatTotalVar")
;; Proof finished.
;; (cp)
(save "cRatLeBoundTotal")

;; Every real has an upper bound, that is the reals are Archimedian ordered.

;; 2021-10-15.  NatPos NatPosExfree cNatPosTotal moved to lib/pos.scm
;; ;; Use cNatPos instead of the pconst NatToPos to block unwanted unfoldings

;; ;; NatPos
;; (set-goal "all n exl p p=NatToPos n")
;; (assume "n")
;; (intro 0 (pt "NatToPos n"))
;; (use "Truth")
;; ;; Proof finished.
;; ;; (cp)
;; (save "NatPos")

;; (animate "NatPos")

;; ;; NatPosExFree
;; (set-goal "all n cNatPos n=NatToPos n")
;; (assume "n")
;; (use "Truth")
;; ;; Proof finished.
;; ;; (cp)
;; (save "NatPosExFree")

;; (deanimate "NatPos")

;; (set-totality-goal "cNatPos")
;; (fold-alltotal)
;; (assume "n")
;; (use "PosTotalVar")
;; ;; Proof finished.
;; ;; (cp)
;; (save "cNatPosTotal")

;; 2021-02-05.  
;; Use cRBd instead of the pconst RealBd to block unwanted unfoldings

(add-program-constant "RealBd" (py "(nat=>rat)=>(pos=>nat)=>nat") t-deg-zero)

;; It might be more uniform to take rea=>nat as type.  Postponed, but
;; some preliminary code is in temp/librseq8.scm, for RealBound

(add-computation-rules
 "RealBd as M"
 "Succ(ListNatMax(cRatLeAbsBound map as fbar Succ(M 1)))")

(set-totality-goal "RealBd")
(fold-alltotal)
(assume "as")
(fold-alltotal)
(assume "M")
(ng #t)
(use "NatTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; RBd
(set-goal "all as,M(Cauchy as M -> exl n n=RealBd as M)")
(assume "as" "M" "CasM")
(intro 0 (pt "RealBd as M"))
(use "Truth")
;; Proof finished.
;; (cp)
(save "RBd")

(animate "RBd")

;; RBdExFree
(set-goal "all as,M(Cauchy as M -> cRBd as M=RealBd as M)")
(assume "as" "M" "CasM")
(use "Truth")
;; Proof finished.
;; (cp)
(save "RBdExFree")

(deanimate "RBd")

(set-totality-goal "cRBd")
(fold-alltotal)
(assume "as")
(fold-alltotal)
(assume "M")
(use "NatTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; Now we can use cRBd where we had used RealBd before.

;; (add-program-constant "RealTimes" (py "rea=>rea=>rea"))

(add-computation-rules
 "(RealConstr as M)*(RealConstr bs N)"
 "RealConstr([n]as n*bs n)
            ([p]M(PosS(p+cNatPos(cRBd bs N)))max
                N(PosS(p+cNatPos(cRBd as M))))")

(animate "RBd")

;; RealBdProp
(set-goal "all as,M(Cauchy as M -> all n abs(as n)<=2**cRBd as M)")
(assume "as" "M" "CasM" "n")
(ng #t)
(simp "SZeroPosPlus")
(cases (pt "n<=M 1"))
;; 5,6
(assume "n<=M 1")
(use "RatLeTrans"
     (pt "(2**ListNatMax(([n0]cRatLeAbsBound(as n0))fbar Succ(M 1)))#1"))
;; 8,9
;; ?^8:abs(as n)<=2**ListNatMax(([n0]cRatLeAbsBound(as n0))fbar Succ(M 1))
(use "RatLeTrans" (pt "(2**cRatLeAbsBound(as n))#1"))
;; 10,11
(use "RatLeAbsBoundExFree")
;;   as  M  CasM:Cauchy as M
;;   n  n<=M 1:n<=M 1
;; -----------------------------------------------------------------------------
;; ?^11:RatLe(2**cRatLeAbsBound(as n))
;;      (2**ListNatMax(([n0]cRatLeAbsBound(as n0))fbar Succ(M 1)))
(use "NatLeMonTwoExp")
;;   as  M  CasM:Cauchy as M
;;   n  n<=M 1:n<=M 1
;; -----------------------------------------------------------------------------
;; ?^12:cRatLeAbsBound(as n)<=
;;      ListNatMax
;;      (cRatLeAbsBound(as Zero)::([n0]cRatLeAbsBound(as(Succ n0)))fbar M 1)
(simp (pf "(cRatLeAbsBound(as Zero)::([n0]cRatLeAbsBound(as(Succ n0)))fbar M 1)
           eqd(([n0]cRatLeAbsBound(as n0))fbar Succ(M 1)) "))
(use-with "ListNatMaxFBar"
	  (pt "[n0]cRatLeAbsBound(as n0)") (pt "n") (pt "Succ(M 1)") "?")
(use "NatLeToLtSucc")
(use "n<=M 1")
(use "InitEqD")
;; 9
(simp (pf "(cRatLeAbsBound(as Zero)::([n0]cRatLeAbsBound(as(Succ n0)))fbar M 1)
           eqd(([n0]cRatLeAbsBound(as n0))fbar Succ(M 1)) "))
(use "Truth")
(use "InitEqD")
;; 6
(assume "n<=M 1 -> F")
(simp (pf "(cRatLeAbsBound(as Zero)::([n0]cRatLeAbsBound(as(Succ n0)))fbar M 1)
           eqd(([n0]cRatLeAbsBound(as n0))fbar Succ(M 1)) "))
(use "RatLeTrans" (pt "abs(as(M 1))+(abs(as n)+ ~(abs(as(M 1))))"))
(assert "all b,c b<=c+(b+ ~c)")
 (assume "b" "c")
 (simp "RatPlusComm")
 (simp "<-" "RatPlusAssoc")
 (simprat (pf "~c+c==0"))
 (use "Truth")
 (use "Truth") 
(assume "Assertion")
(use "Assertion")
(use "RatLeTrans"
     (pt "((2**ListNatMax(([n0]cRatLeAbsBound(as n0))fbar Succ(M 1)))#1)+
          (1#2**1)"))
(use "RatLeMonPlus")
;; 34,35
;; ?^34:abs(as(M 1))<=2**ListNatMax(([n]cRatLeAbsBound(as n))fbar Succ(M 1))
(use "RatLeTrans" (pt "(2**cRatLeAbsBound(as(M 1)))#1"))
(use "RatLeAbsBoundExFree")
(use "NatLeMonTwoExp")
(simp (pf "(cRatLeAbsBound(as Zero)::([n0]cRatLeAbsBound(as(Succ n0)))fbar M 1)
           eqd(([n0]cRatLeAbsBound(as n0))fbar Succ(M 1)) "))
(use-with "ListNatMaxFBar"
	  (pt "[n0]cRatLeAbsBound(as n0)") (pt "M 1") (pt "Succ(M 1)") "?")
(use "Truth")
(use "InitEqD")
;; ?^35:abs(as n)+ ~abs(as(M 1))<=(1#2**1)
(use "RatLeTrans" (pt "abs(abs(as n)+ ~abs(as(M 1)))"))
(use "Truth")
(use "RatLeTrans" (pt "abs(as n+ ~(as(M 1)))"))
(use "RatLeAbsMinusAbs")
;; ?^45:abs(as n+ ~(as(M 1)))<=(1#2**1)
(use "CauchyElim" (pt "M"))
(use "CasM")
(use "NatNotLtToLe")
(assume "n<M 1")
(use "n<=M 1 -> F")
(use "NatLtToLe")
(use "n<M 1")
(use "Truth")
;; ?^33:2**ListNatMax(([n]cRatLeAbsBound(as n))fbar Succ(M 1))+(1#2**1)<=
;;      2**ListNatMax(([n]cRatLeAbsBound(as n))fbar Succ(M 1))+
;;      2**ListNatMax(([n]cRatLeAbsBound(as n))fbar Succ(M 1))
(use "Truth")
;; 21
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "RealBdProp")

;; RealBdPos
(set-goal "all as,M Zero<cRBd as M")
(assume "as" "M")
(use "Truth")
;; Proof finished.
;; (cp)
(save "RealBdPos")

(deanimate "RBd")

;; Totality proofs for RealTimes and RealExp

;; RealTimesTotal
(set-totality-goal "RealTimes")
(fold-alltotal)
(cases)
(assume "as" "M")
(fold-alltotal)
(cases)
(assume "bs" "N")
(use "ReaTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; Rules for RealExp : rea=>nat=>rea

(add-computation-rules
 "x**Zero" "RealConstr([n](RatConstr(IntPos One)One))([p]Zero)"
 "x**Succ n" "x**n*x")

;; RealExpTotal
(set-totality-goal "RealExp")
(fold-alltotal)
(assume "x")
(fold-alltotal)
(ind)
;; Base
(ng #t)
(use "ReaTotalVar")
;; Step
(assume "n" "IH")
(ng #t)
(use "RealTimesTotal")
(use "IH")
(use "ReaTotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; 5.  Comparisen and equality
;; ===========================

;; We introduce an inductively defined predicate RealLe x y

(add-ids
 (list (list "RealLe" (make-arity (py "rea") (py "rea"))))
 '("all x,y(Real x -> Real y ->
    all p x seq(x mod(PosS p))<=y seq(y mod(PosS p))+(1#2**p) ->
    RealLe x y)" "RealLeIntro"))

;; Notice that we cannot take <= and use overloading, because the token
;; <= has token type rel-op and hence produces a term, not a predicate.

(add-token
 "<<="
 'pred-infix
 (lambda (x y)
   (make-predicate-formula (make-idpredconst "RealLe" '() '()) x y)))

(add-idpredconst-display "RealLe" 'pred-infix "<<=")

;; We introduce an inductively defined predicate RealLeS x y
;; expressing pointwise <= for the Cauchy sequences.

(add-ids
 (list (list "RealLeS" (make-arity (py "rea") (py "rea"))))
 '("all x,y(all n x seq n<=y seq n -> RealLeS x y)" "RealLeSIntro"))

;; predicate creator

(define (make-predicate-creator token min-type-string)
  (lambda (x y)
    (let* ((type1 (term-to-type x))
	   (type2 (term-to-type y))
	   (min-type (py min-type-string))
	   (type (types-lub type1 type2 min-type))
	   (internal-name (token-and-types-to-name token (list type))))
      (make-predicate-formula (make-idpredconst internal-name '() '()) x y))))

(add-token "<+=" 'pred-infix (make-predicate-creator "<+=" "rea"))

(add-token-and-type-to-name "<+=" (py "rea") "RealLeS")

(add-idpredconst-display "RealLeS" 'pred-infix "<+=")

;; We introduce an inductively defined predicate RealEq x y

(add-ids
 (list (list "RealEq" (make-arity (py "rea") (py "rea"))))
 '("all x,y(x<<=y -> y<<=x -> RealEq x y)" "RealEqIntro"))

;; Notice that we cannot take = and use overloading, because the token
;; = has token type rel-op and hence produces a term, not a predicate.

(add-token "===" 'pred-infix (make-predicate-creator "===" "rea"))

(add-token-and-type-to-name "===" (py "rea") "RealEq")

(add-idpredconst-display "RealEq" 'pred-infix "===")

;; RealLeAntiSym ;same as RealEqIntro
(set-goal "all x,y(x<<=y -> y<<=x -> RealEq x y)")
(use "RealEqIntro")
;; Proof finished.
;; (cp)
(save "RealLeAntiSym")

;; We introduce an inductively defined predicate RealEqS x y
;; expressing extensional equality of the Cauchy sequences.

(add-ids
 (list (list "RealEqS" (make-arity (py "rea") (py "rea"))))
 '("all x,y(all n x seq n==y seq n -> RealEqS x y)" "RealEqSIntro"))

(add-token "=+=" 'pred-infix (make-predicate-creator "=+=" "rea"))

(add-token-and-type-to-name "=+=" (py "rea") "RealEqS")

(add-idpredconst-display "RealEqS" 'pred-infix "=+=")

;; Non-negative reals are defined inductively

(add-ids
 (list (list "RealNNeg" (make-arity (py "rea"))))
 '("all x(Real x -> all p 0<=x seq(x mod p)+(1#2**p) -> RealNNeg x)"
 "RealNNegIntro"))

;; We introduce an inductively defined predicate RealNNegS x
;; expressing the pointwise NNeg-property of the Cauchy sequence.

(add-ids
 (list (list "RealNNegS" (make-arity (py "rea"))))
 '("all x(all n 0<=x seq n -> RealNNegS x)" "RealNNegSIntro"))

;; Properties of RealLe RealLeS RealEq RealEqS RealNNeg RealNNegS

;; RealLeElim0
(set-goal "all x,y(x<<=y -> Real x)")
(assume "x" "y" "x<=y")
(elim "x<=y")
(search)
;; Proof finished.
;; (cp)
(save "RealLeElim0")

;; RealLeElim1
(set-goal "all x,y(x<<=y -> Real y)")
(assume "x" "y" "x<=y")
(elim "x<=y")
(search)
;; Proof finished.
;; (cp)
(save "RealLeElim1")

;; RealLeElim2
(set-goal "all x,y(x<<=y ->
  all p x seq(x mod(PosS p))<=y seq(y mod(PosS p))+(1#2**p))")
(assume "x" "y" "x<=y")
(elim "x<=y")
(search)
;; Proof finished.
;; (cp)
(save "RealLeElim2")

;; RealConstrLeElim2
(set-goal
 "all as,M,bs,N(RealConstr as M<<=RealConstr bs N ->
                all p as(M(PosS p))<=bs(N(PosS p))+(1#2**p))")
(assume "as" "M" "bs" "N" "LeHyp" "p")
(use-with "RealLeElim2"
	  (pt "RealConstr as M") (pt "RealConstr bs N") "LeHyp" (pt "p"))
;; Proof finished.
;; (cp)
(save "RealConstrLeElim2")

;; RealEqElim0
(set-goal "all x,y(x===y -> x<<=y)")
(assume "x" "y" "x=y")
(elim "x=y")
(search)
;; Proof finished.
(save "RealEqElim0")

;; RealEqElim1
(set-goal "all x,y(x===y -> y<<=x)")
(assume "x" "y" "x=y")
(elim "x=y")
(search)
;; Proof finished.
(save "RealEqElim1")

;; RealEqToReal0
(set-goal "all x,y(x===y -> Real x)")
(assume "x" "y" "x=y")
(use "RealLeElim0" (pt "y"))
(use "RealEqElim0")
(use "x=y")
;; Proof finished.
;; (cp)
(save "RealEqToReal0")

;; RealEqToReal1
(set-goal "all x,y(x===y -> Real y)")
(assume "x" "y" "x=y")
(use "RealLeElim1" (pt "x"))
(use "RealEqElim0")
(use "x=y")
;; Proof finished.
;; (cp)
(save "RealEqToReal1")

;; RealEqSElim
(set-goal "all x,y(x=+=y -> all n x seq n==y seq n)")
(assume "x" "y" "x=y")
(elim "x=y")
(search)
;; Proof finished.
;; (cp)
(save "RealEqSElim")

;; RealConstrEqSElim
(set-goal
 "all as,M,bs,N(RealConstr as M=+=RealConstr bs N -> all n as n==bs n)")
(assume "as" "M" "bs" "N" "EqSHyp" "n")
(use-with "RealEqSElim"
	  (pt "RealConstr as M") (pt "RealConstr bs N") "EqSHyp" (pt "n"))
;; Proof finished.
;; (cp)
(save "RealConstrEqSElim")

;; TotalReaToEqD
(set-goal "allnc x^(TotalReaNc x^ -> x^ eqd RealConstr x^ seq x^ mod)")
(assume "x^")
(elim)
(ng)
(strip)
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "TotalReaToEqD")

;; RealNNegElim0
(set-goal "all x(RealNNeg x -> Real x)")
(assume "x" "NNegx")
(elim "NNegx")
(search)
;; Proof finished.
(save "RealNNegElim0")

;; RealNNegElim1
(set-goal "all x(RealNNeg x -> all p 0<=x seq(x mod p)+(1#2**p))")
(assume "x" "NNegx")
(elim "NNegx")
(search)
;; Proof finished.
(save "RealNNegElim1")

;; The following variants will be useful, because their heads will be
;; more often of the form of a given goal.

;; RealConstrNNegElim0
(set-goal
 "all as,M(RealNNeg(RealConstr as M) -> Real(RealConstr as M))")
(assume "as" "M" "NNegHyp")
(use "RealNNegElim0")
(use "NNegHyp")
;; Proof finished.
(save "RealConstrNNegElim0")

;; RealConstrNNegElim1
(set-goal
 "all as,M(RealNNeg(RealConstr as M) -> all p 0<=as(M p)+(1#2**p))")
(assume "as" "M" "NNegHyp" "p")
(use-with "RealNNegElim1" (pt "RealConstr as M") "NNegHyp" (pt "p"))
;; Proof finished.
(save "RealConstrNNegElim1")

;; We now prove further properties of RealLe RealNNeg

;; EfRealLe
(set-goal "F -> all x,y x<<=y")
(assume "Absurd" "x" "y")
(intro 0)
(use "EfReal")
(use "Absurd")
(use "EfReal")
(use "Absurd")
(ng)
(strip)
(use "EfAtom")
(use "Absurd")
;; Proof finished.
(save "EfRealLe")

;; RealLeRefl
(set-goal "all x(Real x -> x<<=x)")
(cases)
(assume "as" "M" "Rx")
(use "RealLeIntro")
;; 4-6
(use "Rx")
(use "Rx")
(assume "p")
(use "Truth")
;; Proof finished.
(save "RealLeRefl")

;; EfRealEq
(set-goal "F -> all x,y x===y")
(assume "Absurd" "x" "y")
(intro 0)
(use "EfRealLe")
(use "Absurd")
(use "EfRealLe")
(use "Absurd")
;; Proof finished.
(save "EfRealEq")

;; EfRealEq$
(set-goal "F -> all x,y x=+=y")
(assume "Absurd" "x" "y")
(intro 0)
(assume "n")
(use "EfAtom")
(use "Absurd")
;; Proof finished.
(save "EfRealEqS")

;; EfRealNNeg
(set-goal "F -> all x RealNNeg x")
(assume "Absurd" "x")
(intro 0)
(use "EfReal")
(use "Absurd")
(assume "p")
(use "EfAtom")
(use "Absurd")
;; Proof finished.
(save "EfRealNNeg")

;; To prove transitivity of RealLe we need a characterization

;; RealLeChar1
(set-goal "allnc as,M,bs,N(RealConstr as M<<=RealConstr bs N -> 
      allnc p exnc n1 allnc n(n1<=n -> as n<=bs n+(1#2**p)))")
(assume "as" "M" "bs" "N" "x<=y" "p")
(intro 0 (pt "M(PosS(PosS p))max N(PosS(PosS p))"))
(assume "n" "BdHyp")
(use "RatLePlusR")
(simp "RatPlusComm")
;; ?^6:as n+ ~(bs n)<=(1#2**p)
(use "RatLeTrans"
     (pt "(1#2**(PosS(PosS p)))+(1#2**(PosS p))+(1#2**(PosS(PosS p)))"))
;; 7,8
(use "RatLeTrans" (pt "(as n+ ~(as(M(PosS(PosS p)))))+
                       (as(M(PosS(PosS p)))+ ~(bs(N(PosS(PosS p)))))+
                       (bs(N(PosS(PosS p)))+ ~(bs n))"))
;; 9,10
(ng #t)
(simprat "RatEqvPlusMinus")
(simprat "RatEqvPlusMinus")
(use "Truth")
;; 10
(assert
 "all a1,a2,b1,b2,c1,c2(a1<=a2 -> b1<=b2 -> c1<=c2 -> a1+b1+c1<=a2+b2+c2)")
 (assume "a1" "a2" "b1" "b2" "c1" "c2" "a1<=a2" "b1<=b2" "c1<=c2")
 (use "RatLeMonPlus")
 (use "RatLeMonPlus")
 (use "a1<=a2")
 (use "b1<=b2")
 (use "c1<=c2")
;; Assertion proved
(assume "RatLeMonPlus3")
(use "RatLeMonPlus3")
;; 22-24
(use "RatLeTrans" (pt "abs(as n+ ~(as(M(PosS(PosS p)))))"))
(use "Truth")
(use "CauchyElim" (pt "M"))
(use "RealConstrToCauchy")
(autoreal)
(use "NatLeTrans" (pt "(M(PosS(PosS p)))max(N(PosS(PosS p)))"))
(use "NatMaxUB1")
(use "BdHyp")
(use "Truth")
;; 23
(simp "RatPlusComm")
(use "RatLePlusRInv")
(use "RealConstrLeElim2")
(use "x<=y")
;; 24
(use "RatLeTrans" (pt "abs(bs(N(PosS(PosS p)))+ ~(bs n))"))
(use "Truth")
(use "CauchyElim" (pt "N"))
(use "RealConstrToCauchy")
(autoreal)
(use "Truth")
(use "NatLeTrans" (pt "(M(PosS(PosS p)))max(N(PosS(PosS p)))"))
(use "NatMaxUB2")
(use "BdHyp")
;; ?^8:(1#2**PosS(PosS p))+(1#2**PosS p)+(1#2**PosS(PosS p))<=(1#2**p)
;; Use RatPlusHalfExpPosS :
;; all p (1#2**PosS p)+(1#2**PosS p)==(1#2**p)
(assert "(1#2**PosS(PosS p))+(1#2**PosS p)=(1#2**PosS p)+(1#2**PosS(PosS p))")
 (use "RatPlusComm")
(assume "Assertion")
(simp "Assertion")
(drop "Assertion")
(simp "<-" "RatPlusAssoc")
(simprat "RatPlusHalfExpPosS")
(simprat "RatPlusHalfExpPosS")
(use "Truth")
;; Proof finished.
;; (cp)
(save "RealLeChar1")

;; RealLeChar1RealConstrFree
(set-goal "all x,y(x<<=y ->
 all p exnc n0 all n(n0<=n -> x seq n<=y seq n+(1#2**p)))")
(cases)
(assume "as" "M")
(cases)
(assume "bs" "N")
(use "RealLeChar1")
;; Proof finished.
;; (cp)
(save "RealLeChar1RealConstrFree")

;; RealLeChar2
(set-goal "all as,M,bs,N(Real(RealConstr as M) -> Real(RealConstr bs N) ->
           all p exnc n0 all n(n0<=n -> as n<=bs n+(1#2**p)) ->
           RealConstr as M<<=RealConstr bs N)")
(assume "as" "M" "bs" "N" "Rx" "Ry" "Est")
(intro 0)
(autoreal)
(assume "p")
(ng #t)
;; ?^7:as(M(PosS p))<=bs(N(PosS p))+(1#2**p)
(use "RatLePlusR")
(simp "RatPlusComm")
;; ?^9:as(M(PosS p))+ ~(bs(N(PosS p)))<=(1#2**p)
(use "RatLeAllPlusToLe")
(assume "q")
;; ?^11:as(M(PosS p))+ ~(bs(N(PosS p)))<=(1#2**p)+(1#2**q)
(inst-with-to "Est" (pt "q") "InstEst")
(drop "Est")
(by-assume "InstEst" "n0" "n0Prop")
;; We now want to use n as an abbreviation for the complex term
;; ((M(PosS p))max(N(PosS p)))max n0.
(defnc "n" "((M(PosS p))max(N(PosS p)))max n0")
(use "RatLeTrans"
     (pt "(as(M(PosS p))+ ~(as n))+
          (as n+ ~(bs n))+
          (bs n+ ~(bs(N(PosS p))))"))
;; 25,26
(ng #t)
(simprat "RatEqvPlusMinus")
(simprat "RatEqvPlusMinus")
(use "Truth")
;; ?^26:as(M(PosS p))+ ~(as n)+(as n+ ~(bs n))+(bs n+ ~(bs(N(PosS p))))<=
;;      (1#2**p)+(1#2**q)
(use "RatLeTrans" (pt "(1#2**(PosS p))+(1#2**q)+(1#2**(PosS p))"))
(assert
 "all a1,a2,b1,b2,c1,c2(a1<=a2 -> b1<=b2 -> c1<=c2 -> a1+b1+c1<=a2+b2+c2)")
 (assume "a1" "a2" "b1" "b2" "c1" "c2" "a1<=a2" "b1<=b2" "c1<=c2")
 (use "RatLeMonPlus")
 (use "RatLeMonPlus")
 (use "a1<=a2")
 (use "b1<=b2")
 (use "c1<=c2")
;; Assertion proved
(assume "RatLeMonPlus3")
(use "RatLeMonPlus3")
;; 40-42
(drop "RatLeMonPlus3")
(use "RatLeTrans" (pt "abs(as(M(PosS p))+ ~(as n))"))
(use "Truth")
(use "CauchyElim" (pt "M"))
(use "RealConstrToCauchy")
(use "Rx")
(use "Truth")
(simp "nDef")
(use "NatLeTrans" (pt "M(PosS p)max N(PosS p)"))
(use "NatMaxUB1")
(use "NatMaxUB1")
;; 41
(drop "RatLeMonPlus3")
(simp "RatPlusComm")
(use "RatLePlusRInv")
(use "n0Prop")
(simp "nDef")
(use "NatMaxUB2")
;; 42
(drop "RatLeMonPlus3")
(use "RatLeTrans" (pt "abs(bs n+ ~(bs(N(PosS p))))"))
(use "Truth")
(use "CauchyElim" (pt "N"))
(use "RealConstrToCauchy")
(use "Ry")
(simp "nDef")
(use "NatLeTrans" (pt "M(PosS p)max N(PosS p)"))
(use "NatMaxUB2")
(use "NatMaxUB1")
(use "Truth")
;; ?^31:(1#2**PosS p)+(1#2**q)+(1#2**PosS p)<=(1#2**p)+(1#2**q)
(simp "RatPlusComm")
(simp "RatPlusAssoc")
(simprat "RatPlusHalfExpPosS")
(use "Truth")
;; Proof finished.
;; (cp)
(save "RealLeChar2")


;; 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)))")
(assume "as" "M" "RasM" "p" "n" "m" "nBd" "mBd")
(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")
;; Proof finished.
;; (cp)
(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")

;; 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))"))
;; 26,27
(ng #t)
(assume "Left")
(intro 0)
;; ?^30:RealConstr cs K<<=RealConstr bs N
(use "RealLeChar2")
(simp "<-" "zDef")
(use "Rz")
(simp "<-" "yDef")
(use "Ry")
;; ?^33:all p exnc n all n0(n<=n0 -> cs n0<=bs n0+(1#2**p))
(assume "q")
(intro 0 (pt "m"))
(assume "l" "m<=l")
(use "RatLeTrans" (pt "bs l"))
;; 39,40
(use "RatLeTrans" (pt "cs m+(1#2**(PosS(PosS p)))"))
;; 41,42
;; ?^41:cs l<=cs m+(1#2**PosS(PosS p))
(use "ApproxSplitAux1" (pt "K"))
(simp "<-" "zDef")
(use "Rz")
(use "NatLeTrans" (pt "m"))
(simp "mDef")
(use "NatMaxUB2")
(use "m<=l")
(simp "mDef")
(use "NatMaxUB2")
;; ?^42:cs m+(1#2**PosS(PosS p))<=bs l
(use "RatLeTrans" (pt "(as n+bs n)*(1#2)+(bs n+ ~(as n))*(1#4)"))
(use "RatLeMonPlus")
(simp "RatTimesComm")
(use "Left")
(use "RatLeTrans" (pt "(1#2**p)*(1#4)"))
(ng #t)
;; ?^58:SZero(SZero(2**p))<=2**PosS(PosS p)
(simp "PosSSucc")
(simp "PosSSucc")
(use "Truth")
;; ?^57:(1#2**p)*(1#4)<=(bs n+ ~(as n))*(1#4)
(use "RatLeMonTimes")
(use "Truth")
(use "x<y")
;; ?^52:(as n+bs n)*(1#2)+(bs n+ ~(as n))*(1#4)<=bs l
(simprat "ApproxSplitAux3")
;; ?^63:bs n+ ~((bs n+ ~(as n))*(1#4))<=bs l
(use "RatLeTrans" (pt "bs n+ ~(1#2**PosS(PosS p))"))
(use "RatLeMonPlus")
(use "Truth")
(simp "RatLe7RewRule")
;; ?^68:(1#2**PosS(PosS p))<=(bs n+ ~(as n))*(1#4)
(use "RatLeTrans" (pt "(1#2**p)*(1#4)"))
;; 69,70
;; ?^69:(1#2**PosS(PosS p))<=(1#2**p)*(1#4)
(simp "PosSSucc")
(simp "PosSSucc")
(use "Truth")
;; ?^70:(1#2**p)*(1#4)<=(bs n+ ~(as n))*(1#4)
(use "RatLeMonTimes")
(use "Truth")
(use "x<y")
;; ?^65:bs n+ ~(1#2**PosS(PosS p))<=bs l
(use "ApproxSplitAux2" (pt "N"))
(simp "<-" "yDef")
(use "Ry")
(simp "nDef")
(use "NatMaxUB1")
(use "NatLeTrans" (pt "m"))
(simp "mDef")
(use "NatLeTrans" (pt "n"))
(simp "nDef")
(use "NatMaxUB1")
(use "NatMaxUB1")
(use "m<=l")
(use "Truth")
;; 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")