(load "~/git/minlog/init.scm")
(set! COMMENT-FLAG #f)
(load "~/uni/const-ana/vortrag/completeness.scm")
(set! COMMENT-FLAG #t)

(add-var-name "ys" (py "nat=>rea"))

;; RealNNegLim (adapted version)
(set-goal "all xs,M,x,L (
    all n (Real (xs n))
->  Real x
->  all n (x seq n = (xs n) seq ((xs n) mod (NatToPos n)) )
->  all p (L p = (M (p + 1)) max (p+2)) 
->  all p (x mod p = L p)
->  (all n (RealNNeg (xs n)))
->  RealNNeg x)")
(assume "xs" "M" "x" "L" "xsReal" "xReal" "xSeqDef" "LDef" "xModDef" "xsNNeg")

(intro 0)

(use "xReal")

(assume "p")
(simp "RatPlusComm")
(use "RatLePlusR")

(use "RatLeTrans" (pt "~(1#2**(L p))"))
	(ng #t)
	(use "NatLeMonTwoExp")
	(simp "LDef")
	(use "NatLeTrans" (pt "PosToNat (p+2)"))
		(simp "PosToNatLe")
		(use "Truth")
		(use "NatMaxUB2")

	(use "RatLeTrans" (pt "~(1#2**L p) + 0"))
		(use "Truth")

	(use "RatLePlusRInv")
	(simp "xSeqDef" (pt "x mod p"))
	(simp "xModDef" (pt "p"))
	(simp "RatPlusComm")

	(cut "(1#2**L p) = (1#2**NatToPos(L p))")
	(assume "NatToPosConversion")
	(simp "NatToPosConversion")
	(drop "NatToPosConversion")

	(use "RealNNegElim1" (pt "xs (L p)") (pt "NatToPos (L p)") )
	(use "xsNNeg")

	;; Left to show "(1#2**L p) = (1#2**NatToPos(L p))", surprisingly nontrivial:
	(simp "PosToNatToPosId")
		(use "Truth")
	(use "NatLtLeTrans" (pt "PosToNat 1"))
		(use "Truth")
	(simp "LDef")
	(use "NatLeTrans" (pt "PosToNat (p+2)"))
	(simp "PosToNatLe")
	(use "Truth")
	(use "NatMaxUB2")
(cdp)
(save "RealNNegLim")


;; SERIES

;; (PartialSum n xs m) denotes the sum of the entries n through (n+m) of the sequence xs
(add-program-constant "PartialSum" (py "nat => (nat => rea) => nat => rea"))
(add-computation-rule (pt "PartialSum n xs Zero") (pt "xs n"))
(add-computation-rule (pt "PartialSum n xs (Succ m)") (pt "(PartialSum n xs m) + (xs (n + Succ m))"))

;; Test example 
(add-program-constant "ID" (py "nat => rea"))
(add-computation-rule (pt "ID n") (pt "n"))
(pp (nt (pt "ID Zero")))
(pp (nt (pt "ID 5")))
(pp (nt (pt "PartialSum Zero ID Zero")))
(pp (nt (pt "PartialSum Zero ID 5")))
(pp (nt (pt "PartialSum 1 ID 3")))

;; Proof totality of PartialSum
(set-totality-goal "PartialSum")
(use "AllTotalElim")
(assume "n")
(assume "xs^")
(assume "TotalHyp")
(use "AllTotalElim")
(assume "n0")

(ind (pt "n0"))
	(ng)
	(use "TotalHyp")
	(use "NatTotalVar")

	(assume "n1" "IH")
	(ng)
	(use "RealPlusTotal")
	(use "IH")
	(use "TotalHyp")
	(use "NatTotalVar")
(save-totality)

;; Proof realness of PartialSum
(set-goal "all n,xs,m (all n (Real (xs n)) -> Real (PartialSum n xs m))")
(assume "n" "xs" "m" "RealHyp")

(ind (pt "m"))
	(ng #t)
	(use "RealHyp")

	(assume "n0" "IndHyp")
	(ng #t)
	(use "RealPlusReal")
	(use "IndHyp")
	(use "RealHyp")
(save "PartialSumReal")

;; some computation rules
(aga "PartialSumDif" "all xs,n,m (m < n -> PartialSum Zero xs n-PartialSum Zero xs m===PartialSum(m+1)xs(n--m--1))")
(aga "PartialSumSplitFirst" "all n,ys,n0 (PartialSum n ys(Succ n0)===ys n+PartialSum(n+1)ys n0)")
(aga "PartialSumNNeg" "all n,xs,m(all n (RealNNeg (xs n)) -> RealNNeg (PartialSum n xs m))")

;; Define convergence of series
(add-ids (list (list "RealSeriesConv" (make-arity (py "nat=>rea") (py "rea") (py "pos=>nat"))))
	'("all xs,x,M (RealConv (PartialSum Zero xs) x M -> RealSeriesConv xs x M)" 
	"RealSeriesConvIntro"))

;; Define Cauchy property of series
(add-ids (list (list "RealSeriesCauchy"
		     (make-arity (py "nat=>rea") (py "pos=>nat"))))
	'("all xs,M(
			all p,n,m(
				M p<=m
				-> m<n
				-> RealLe (abs((PartialSum Zero xs) n-(PartialSum Zero xs) m)) (1/2 ** p)) 
				-> RealSeriesCauchy xs M)"
	"RealSeriesCauchyIntro"))

;; RealSeriesConvElim
(set-goal "all xs,x,M (RealSeriesConv xs x M -> RealConv (PartialSum Zero xs) x M)")
(assume "xs" "x" "M")
(elim)
(search)
(save "RealSeriesConvElim")

;; RealSeriesCauchyElim
(set-goal "all xs,M (RealSeriesCauchy xs M ->
	all p,n,m (
		M p <= m
		-> m < n
		-> RealLe (abs((PartialSum Zero xs) n-(PartialSum Zero xs) m)) (1/2 ** p))
	)")
(assume "xs" "M")
(elim)
(search)
(save "RealSeriesCauchyElim")

(aga "RealConvCauchy" "all xs,x,M (RealConv xs x M -> RealCauchy xs ([p] M (p+1)))")

;; Convergence -> Cauchy for real series
(set-goal "all xs,x,M (RealSeriesConv xs x M -> RealSeriesCauchy xs ([p] M (p+1)))")
(assume "xs" "x" "M" "ConvHyp")
(intro 0)
(assume "p" "n" "m" "mBig" "nBig")

(inst-with-to "RealSeriesConvElim" (pt "xs") (pt "x") (pt "M") "ConvHyp" "SeqConvHyp")
(inst-with-to "RealConvCauchy" (pt "PartialSum Zero xs") (pt "x") (pt "M") "SeqConvHyp" "CauchyHyp")

(use "RealCauchyElim3" (pt "[p] M (p+1)"))
	(use "CauchyHyp")

	(ng #t)
	(use "NatLeTrans" (pt "m"))
		(search)

		(use "NatLtToLe")
		(search)
	(search)
(save "RealSeriesConvToCauchy")

;; Opposite implication
(aga "RealSeriesCauchyToConv" "all xs,M (RealSeriesCauchy xs M -> exnc x (RealSeriesConv xs x M))")

;; Null sequence criterion
(set-goal "all xs,M 
	(all n (Real (xs n)) 
	-> RealSeriesCauchy xs M 
	-> all p,n (
		(M p) <= n 
		-> abs(xs (n + 1)) <<= 1/2**p))")
(assume "xs" "M" "xsReal" "xsCauchy" "p" "n" "nBig")

(assert "Real (xs n)")
	(use "xsReal")
(assume "xnReal")

(assert "Real(xs (Succ n))")
	(use "xsReal")
(assume "RealHyp2")

(assert "Real(PartialSum Zero xs n)")
	(use "PartialSumReal")
	(use "xsReal")
(assume "RealHyp3")

(ng #t)
(use "RealLeTrans" (pt "abs(PartialSum Zero xs n+xs(Succ n)+ ~(PartialSum Zero xs n))"))
	(simpreal "<-" "RealAbsCompat" (pt "PartialSum Zero xs n+xs(Succ n)+ ~(PartialSum Zero xs n)"))
		(use "RealLeRefl")
		(autoreal)

		(simpreal "<-" "RealPlusComm")
		(simpreal "RealPlusAssoc")

		(assert "~(PartialSum Zero xs n)+PartialSum Zero xs n === 0")
			(simpreal "<-" "RealPlusComm")
			(use "RealPlusMinusZero")
			(autoreal)

		(assume "Eq")
		(simpreal "Eq")
		(use "RealZeroPlus")
		(autoreal)

	(inst-with-to "RealSeriesCauchyElim" (pt "xs") (pt "M") "xsCauchy" "CauchyDef")
	(inst-with-to "CauchyDef" (pt "p") (pt "n+1") (pt "n") "CauchyInst")
	(use "CauchyInst")
	(search)
	(search)
(cdp)
(save "NullSeqCrit")

;; Leibniz criterion
(set-goal "all xs,M,ys(
	all n (Real (xs n))
	-> all n (Real (ys n))
	-> all n (RealNNeg (xs n)) 
	-> all n (0 <<= xs n - xs (n+1))
	-> RealConv xs 0 M
	-> all n (xs n === ((~1)**n) * (ys n))
	-> RealSeriesCauchy ys M)")
(assume "xs" "M" "ys" "xsReal" "ysReal" "NNegHyp" "MonHyp" "ConvHyp" "xyEqHyp")

(assert "all m,n (0 <<= ((~1)**n) * (PartialSum n ys m) andi ((~1)**n) * (PartialSum n ys m) <<= (xs n))")
	(admit)
(assume "Ineq")

(intro 0)
(assume "p" "n" "m" "mBig" "nBig")

(simpreal "PartialSumDif")
(inst-with-to "Ineq" (pt "n--m--1") (pt "m+1") "IneqInst")

(assert "abs(PartialSum(m+1) ys (n--m--1)) === ~1**(m+1)*(PartialSum(m+1) ys (n--m--1))")
	(admit)
(assume "AbsEq")

(elim "IneqInst")
(assume "IneqInst1")
(assume "IneqInst2")

(simpreal "AbsEq")
(use "RealLeTrans" (pt "xs(m+1)"))
(use "IneqInst2")

(inst-with-to "RealConvElim4" (pt "xs") (pt "RealConstr ([n] 0) ([p] Zero)") (pt "M") "ConvHyp" "ConvDef")

(use "RealLeTrans" (pt "abs(xs(m+1))"))
(use "RealLeAbsId")
(autoreal)

(inst-with-to "ConvDef" (pt "p") (pt "Succ m") "Aux")
(ng #t "Aux")

(assert "M p <= Succ m")
	(use "NatLeTrans" (pt "m"))
	(use "mBig")
	(search)

(assert "abs(xs(Succ m)) === abs(xs(Succ m)+0)")
	(use "RealAbsCompat")
	(assert "Real (xs (Succ m))")
		(use "xsReal")
	(assume "RealHyp")
	(simpreal "RealPlusZero")
	(use "RealEqRefl")
	(autoreal)

(assume "Eq2")
(assume "SuccmBig")
(simpreal "Eq2")
(use "Aux")

(use "SuccmBig")
(use "nBig")

;; works sometimes
(cdp)


;; ComparisonTest (leichte modifizierte Version mit xs nicht-negativ, erspart Verwendung von Beträgen)
(set-goal "all ys,M,xs
	(all n (Real (ys n))
	-> all n (Real (xs n))
	-> all n (RealNNeg (ys n))
	-> all n (RealNNeg (xs n))
	-> all n (xs n <<= ys n)
	-> RealSeriesCauchy ys M
	-> RealSeriesCauchy xs M)")
(assume "ys" "M" "xs" "ysReal" "xsReal" "ysNNeg" "xsNNeg" "xsBound" "CauchyHyp")
(intro 0)
(assume "p" "n" "m" "mBig" "nBig")

(use "RealLeTrans" (pt "abs((PartialSum Zero ys n)+ ~(PartialSum Zero ys m))"))
	(get 6)
		(use "RealSeriesCauchyElim" (pt "M"))
		(use "CauchyHyp")
		(use "mBig")
		(use "nBig")

	(use "RealLeCompat" (pt "(PartialSum Zero xs n)+ ~(PartialSum Zero xs m)")
		(pt "(PartialSum Zero ys n) + ~(PartialSum Zero ys m)"))

		(use "RealEqSym")
		(use "RealEqAbs")
		(simpreal "PartialSumDif")
		(use "PartialSumNNeg")
		(use "xsNNeg")
		(use "nBig")

		(use "RealEqSym")
		(use "RealEqAbs")
		(simpreal "PartialSumDif")
		(use "PartialSumNNeg")
		(use "ysNNeg")
		(use "nBig")

	(use "RealLeCompat" (pt "PartialSum(Succ m)xs(Pred(n--m))") 
		(pt "PartialSum(Succ m)ys(Pred(n--m))")  )	

		(use "RealEqSym")
		(use "PartialSumDif")
		(use "nBig")

		(use "RealEqSym")
		(use "PartialSumDif")
		(use "nBig")

	(ind (pt "Pred(n--m)"))
		(ng #t)
		(use "xsBound")

		(assume "n0" "IH")
		(ng #t "IH")
		(use "RealLeMonPlus")
		(use "IH")
		(use "xsBound")
(cdp)
(save "ComparisonTest")