;; 2025-06-15.  solcoigfpiter.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)

;;;; 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 …

;;;; Helpful theorems 
(pp "RealEqRefl")
(pp "RealEqToReal0")

;;;; Used predicates
(display-idpc "CoI")
(display-idpc "OrD")

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

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