;; 2025-06-22.  solcoi.scm

(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "list.scm")
(set-goal "all n(NatEven n -> NatEven(Succ n) -> F)")
(use "NatEvenToOddSucc")
(save "NatEvenSucc")
(libload "pos.scm")
(libload "int.scm")
(libload "rat.scm")
(libload "rea.scm")
(load "digits.scm")
(load "sdcode1.scm")
(set! COMMENT-FLAG #t)

(pp "RealEqToReal0")
;; all x,y(x===y -> Real x)

;; CoIGfpIter
(set-goal
 "allnc x(
     (Pvar rea)x -> 
     exr d,x0(
      Sd d andi
      Real x0 andi abs x0<<=1 andi (Pvar rea)x0 andi x===(1#2)*(x0+d))) -> 
    allnc x((Pvar rea)x -> CoI x)")
;; allnc x(
;;      (Pvar rea)x -> 
;;      exr d,x0(
;;       Sd d andd 
;;       Real x0 andr abs x0<<=1 andr (Pvar rea)x0 andl x===(1#2)*(x0+d))) -> 
;;     allnc x((Pvar rea)x -> CoI x)

;; Note that proper decorations (andd andr andl) are inserted
;; automatically.  They are determined by the cr/nc-status of the
;; formulas involved.  Recall that "and" is right-associative.

(assume "Hyp" "x" "Px")
(coind "Px")
(assume "x0" "Px0")
(inst-with-to "Hyp" (pt "x0") "Px0" "Inst")
(drop "Hyp")
(by-assume "Inst" "d" "dProp")
(by-assume "dProp" "y" "dyProp")
(intro 0 (pt "d"))
(intro 0 (pt "y"))
(intro 0 (pt "x0"))
(split)
(use "dyProp")
(split)
(use "dyProp")
(split)
(use "dyProp")
(split)
(intro 1)
(use "dyProp")
(split)
(use "dyProp")
(use "RealEqRefl")
(use "RealEqToReal0" (pt "(1#2)*(y+d)"))
(use "dyProp")
;; Proof finished.
;; (cp)
(save "CoIGfpIter")

;; To see the greatest-fixed-point (or coinduction) axiom CoI^+ apply
;; (proof-to-expr-with-formulas) after (coind "Px").  This gives

;; Gfp: allnc x(
;;  (Pvar rea)x -> 
;;  allnc x0(
;;   (Pvar rea)x0 -> 
;;   exr d,x1,y(
;;    Sd d andd 
;;    Real x1 andr 
;;    abs x1<<=1 andr 
;;    (CoI x1 ord (Pvar rea)x1) andl y===(1#2)*(x1+d) andnc x0===y)) -> 
;;  CoI x)



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

;; (coind), (coind (pt "…"))
; Applies coinduction axiom

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

;; (pp …)
; Display a theorem

;; (split)
; Splits a goal of the Form A ∧ B into subgoals A,B

;; (inst-with-to "Hyp" … "Inst")
; Supply variables and assumptions to the hypothesis "Hyp"
; and extract the result to "Inst".
(set-goal "all m ((all n(n = Succ m -> n = 0 -> bot)) -> (all n(n = Succ m -> n = 0 -> bot)))")
(assume "m" "V" "n" "n=m+1" "n=0")
(inst-with-to "V" (pt "n") "n=m+1" "n=0" "W")
(use "W")

;; (by-assume "∃ₓA" "x" "A")
; Splits an hypothesis from the context ∃ₓA into a variable x and a formula A with free x
; and adds them to the context.

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

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

;; (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.

;; (simpreal …)
; Works just like (simp …) but with equalities on 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.

;;; Tips
;; To obtain a better understanding of Real and Sd you might find following helpful
(display-idpc "Real")
(display-idpc "Cauchy")
(display-idpc "Mon")
(display-alg "rea") ; the type of variables x,y
(display-alg "rat")
(display-alg "int")
(display-alg "pos")
(display-alg "nat")

;;;; (a)
;;; Helpful Theorems
(pp "RealUMinusRealInv")
(pp "CoIToReal")
(pp "CoIToBd")
(pp "CoIClosure")
(pp "SdUMinus")
(pp "RealUMinusPlusRat")
(pp "RealTimesIdUMinus")
(pp "RealUMinusInj")
(pp "RealEqRefl")
(pp "RealAbsUMinus")
(pp "RealUMinusUMinus")

;; You might find further helpful theorems by using e.g.
(search-about "RealEq")
(search-about "Real")
(search-about "CoI")

;; CoIUMinus
(set-goal "allnc x(CoI(~x) -> CoI x)")
(assume "x" "CoI-x")
(coind "CoI-x")
;; TODO
(save "CoIUMinus")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (ppc neterm)

;; [u](CoRec ai=>ai)u
;;  ([u0]
;;    cSdUMinus clft(cCoIClosure u0)pair InR(cCoICompat crht(cCoIClosure u0)))

(add-sound "CoIUMinus")
(deanimate "CoIUMinus")

(display-idpc "CoI")

;;;; (b)
;;; Helpful theorems
(pp "CoIClauseInv")
(pp "CoIToBd")
(pp "RealEqRefl")

;; CoIClosureInv
(set-goal "allnc d,x(Sd d -> CoI x -> CoI((1#2)*(x+d)))")
;; TODO
(save "CoIClosureInv")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (ppc neterm)
;; [s,u]cCoIClauseInv(s pair u)

(add-sound "CoIClosureInv")

;; (define eterm (proof-to-extracted-term))
;; (define neterm (rename-variables (nt eterm)))
;; (ppc neterm)
;; [s,u](CoRec sd yprod ai=>ai)(s pair u)([su]clft su pair InL crht su)

(deanimate "CoIClosureInv")